Imperial College London

ProfessorNobukoYoshida

Faculty of EngineeringDepartment of Computing

Academic Visitor
 
 
 
//

Contact

 

+44 (0)20 7594 8240n.yoshida Website

 
 
//

Location

 

556Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Publication Type
Year
to

373 results found

Yoshida N, 2024, Programming Language Implementations with Multiparty Session Types, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Pages: 147-165

Session types provide a typing discipline for communication systems, and a number of programming languages are integrated with session types. This paper provides a survey of programming language implementations which use the structuring mechanism from multiparty session types (MPST). The theory of MPST guarantees that processes following a predefined communication protocol (a multiparty session) are free from communication errors and deadlocks. We discuss the top-down, bottom-up and hybrid MPST frameworks, and compare their positive and negative aspects, through a Rust MPST implementation framework, Rumpsteak. We also survey MPST implementations with dynamic (runtime) verification which target active object programming languages.

Book chapter

Barbanera F, Dezani-Ciancaglini M, Gheri L, Yoshida Net al., 2023, Multicompatibility for Multiparty-Session Composition

Modular methodologies for the development and verification of concurrent/distributed systems are increasingly relevant nowadays. We investigate the simultaneous composition of multiple systems in a multiparty-session-type setting, working on suitable notions of interfacing policy and multicompatibility. The resulting method is conservative (it makes only the strictly needed changes), flexible (any system can be looked at as potentially open) and safe (relevant communication properties, e.g. lock-freedom, are preserved by composition). We obtain safety by proving preservation of typability. We also provide a sound and complete type inference algorithm.

Conference paper

Barwell A, Hou P, Yoshida N, Zhou Fet al., 2023, Designing asynchronous multiparty protocols with crash-stop failures, European Conference on Object-Oriented Programming (ECOOP 2023), Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, Pages: 1:1-1:30, ISSN: 1868-8969

Session types provide a typing discipline for message-passing systems. However, most session type approaches assume an ideal world: one in which everything is reliable and without failures. Yet this is in stark contrast with distributed systems in the real world. To address this limitation, we introduce Teatrino, a code generation toolchain that utilises asynchronous multiparty session types(MPST) with crash-stop semantics to support failure handling protocols. We augment asynchronous MPST and processes with crash handling branches. Our approach requires no user-level syntax extensions for global types and features a formalisation of global semantics, which captures complex behaviours induced by crashed/crash handling processes. The sound and complete correspondence between global and local type semantics guarantees deadlock-freedom, protocol conformance, and liveness of typed processes in the presence of crashes. Our theory is implemented in the toolchain Teatrino, which provides correctness by construction. Teatrino extends the Scribble multiparty protocol language to generate protocol-conformingScala code, using the Effpi concurrent programming library. We extend both Scribble and Effpi to support crash-stop behaviour. We demonstrate the feasibility of our methodology and evaluate Teatrino with examples extended from both session type and distributed systems literature.

Conference paper

Castro-Perez D, Yoshida N, 2023, Dynamically Updatable Multiparty Session Protocols Generating Concurrent Go Code from Unbounded Protocols, ISSN: 1868-8969

Multiparty Session Types (MPST) are a typing disciplines that guarantee the absence of deadlocks and communication errors in concurrent and distributed systems. However, existing MPST frameworks do not support protocols with dynamic unbounded participants, and cannot express many common programming patterns that require the introduction of new participants into a protocol. This poses a barrier for the adoption of MPST in languages that favour the creation of new participants (processes, lightweight threads, etc) that communicate via message passing, such as Go or Erlang. This paper proposes Dynamically Updatable Multiparty Session Protocols, a new MPST theory (DMst) that supports protocols with an unbounded number of fresh participants, whose communication topologies are dynamically updatable. We prove that DMst guarantees deadlock-freedom and liveness. We implement a toolchain, GoScr (Go-Scribble), which generates Go implementations from DMst, ensuring by construction, that the different participants will only perform I/O actions that comply with a given protocol specification. We evaluate our toolchain by (1) implementing representative parallel and concurrent algorithms from existing benchmarks, textbooks and literature; (2) showing that GoScr does not introduce significant overheads compared to a naive implementation, for computationally expensive benchmarks; and (3) building three realistic protocols (dynamic task delegation, recursive Domain Name System, and a parallel Min-Max strategy) in GoScr that could not be represented with previous theories of session types.

Conference paper

Gheri L, Yoshida N, 2023, Hybrid Multiparty Session Types, PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, Vol: 7

Journal article

Mezzina CA, Tiezzi F, Yoshida N, 2023, Rollback Recovery in Session-Based Programming, Pages: 195-213, ISBN: 9783031353604

To react to unforeseen circumstances or amend abnormal situations in communication-centric systems, programmers are in charge of “undoing” the interactions which led to an undesired state. To assist this task, session-based languages can be endowed with reversibility mechanisms. In this paper we propose a language enriched with programming facilities to commit session interactions, to roll back the computation to a previous commit point, and to abort the session. Rollbacks in our language always bring the system to previous visited states and a rollback cannot bring the system back to a point prior to the last commit. Programmers are relieved from the burden of ensuring that a rollback never restores a checkpoint imposed by a session participant different from the rollback requester. Such undesired situations are prevented at design-time (statically) by relying on a decidable compliance check at the type level, implemented in MAUDE. We show that the language satisfies error-freedom and progress of a session.

Book chapter

Demangeon R, Yoshida N, 2023, Causal computational complexity of distributed processes, INFORMATION AND COMPUTATION, Vol: 290, ISSN: 0890-5401

Journal article

Vasconcelos VT, Martins F, Lopez H-A, Yoshida Net al., 2022, A Type Discipline for Message Passing Parallel Programs, ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, Vol: 44, ISSN: 0164-0925

Journal article

Li R, Ren X, Zhao X, He S, Stumm M, Yuan Det al., 2022, ctFS: Replacing File Indexing with Hardware Memory Translation through Contiguous File Allocation for Persistent Memory, ACM TRANSACTIONS ON STORAGE, Vol: 18, ISSN: 1553-3077

Journal article

Ellis S, Zhu S, Yoshida N, Song Let al., 2022, Generic go to go: dictionary-passing, monomorphisation, and hybrid, Proceedings of the ACM on Programming Languages, Vol: 6

Go is a popular statically-typed industrial programming language. To aid the type safe reuse of code, the recent Go release (Go 1.18) published early 2022 includes bounded parametric polymorphism via generic types. Go 1.18 implements generic types using a combination of monomorphisation and call-graph based dictionary-passing called hybrid. This hybrid approach can be viewed as an optimised form of monomorphisation that statically generates specialised methods and types based on possible instantiations. A monolithic dictionary supplements information lost during monomorphisation, and is structured according to the program's call graph. Unfortunately, the hybrid approach still suffers from code bloat, poor compilation speed, and limited code coverage. In this paper we propose and formalise a new non-specialising call-site based dictionary-passing translation. Our call-site based translation creates individual dictionaries for each type parameter, with dictionary construction occurring in place of instantiation, overcoming the limitations of hybrid. We prove it correct using a novel and general bisimulation up to technique. To better understand how different generics translation approaches work in practice, we benchmark five translators, Go 1.18, two existing monomorphisation translators, our dictionary-passing translator, and an erasure translator. Our findings reveal several suggestions for improvements for Go 1.18 - specifically how to overcome the expressiveness limitations of generic Go and improve compile time and compiled code size performance of Go 1.18.

Journal article

Peters K, Yoshida N, 2022, On the expressiveness of mixed choice sessions, EXPRESS/SOS 2022 : Combined 29th International Workshop on Expressiveness in Concurrency and 19th Workshop on Structural Operational Semantics, Publisher: Open Publishing Association, Pages: 113-130, ISSN: 2075-2180

Session types provide a flexible programming style for structuring interaction, and are used to guarantee a safe and consistent composition of distributed processes. Traditional session types include only one-directional input (external) and output (internal) guarded choices. This prevents the session-processes to explore the full expressive power of the pi-calculus where the mixed choices are proved more expressive than the (non-mixed) guarded choices. To account this issue, recently Casal, Mordido, and Vasconcelos proposed the binary session types with mixed choices (CMV+). This paper carries a surprising, unfortunate result on CMV+: in spite of an inclusion of unrestricted channels with mixed choice, CMV+'s mixed choice is rather separate and not mixed. We prove this negative result using two methodologies (using either the leader election problem or a synchronisation pattern as distinguishing feature), showing that there exists no good encoding from the pi-calculus into CMV+, preserving distribution. We then close their open problem on the encoding from CMV+ into CMV (without mixed choice), proving its soundness and thereby that the encoding is good up to coupled similarity.

Conference paper

Barwell A, Scalas A, Yoshida N, Zhou Fet al., 2022, Generalised multiparty session types with crash-stop failures, International Conference on Concurrency Theory (CONCUR), Publisher: Schloss Dagstuhl, Pages: 35:1-35:25, ISSN: 1868-8969

Session types enable the specification and verification of communicating systems. However, their theory often assumes that processes never fail. To address this limitation, we present a generalised multiparty session type (MPST) theory with crash-stop failures, where processes can crash arbitrarily.Our new theory validates more protocols and processes w.r.t. previous work. We apply minimal syntactic changes to standard session π-calculus and types: we model crashes and their handling semantically, with a generalised MPST typing system parametric on a behavioural safety property. We cover the spectrum between fully reliable and fully unreliable sessions, via optional reliability assumptions, and prove type safety and protocol conformance in the presence of crash-stop failures. Introducing crash-stop failures has non-trivial consequences: writing correct processes that handle all crash scenarios can be difficult. Yet, our generalised MPST theory allows us to tame this complexity, via model checkers, to validate whether a multiparty session satisfies desired behavioural properties, e.g. deadlock-freedom or liveness, even in presence of crashes. We implement our approach using the mCRL2 model checker, and evaluate it with examples extended from the literature

Conference paper

Peters K, Yoshida N, 2022, On the Expressiveness of Mixed Choice Sessions, Electronic Proceedings in Theoretical Computer Science, Vol: 368, Pages: 113-130

Journal article

Yoshida N, 2022, Introduction to the Special Issue on ESOP 2021, ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, Vol: 44, ISSN: 0164-0925

Journal article

Gheri L, Lanese I, Sayers N, Tuosto E, Yoshida Net al., 2022, Design-by-contract for flexible multiparty session protocols (Artifact), ECOOP 2022 (Artifacts Evaluation), Publisher: Schloss Dagstuhl, Leibniz-Zentrum, Pages: 1-5, ISSN: 2509-8195

We introduce CAScr, the first implementationof Scribble (http://www.scribble.org, https://nuscr.dev/) that relies on choreography automata,for deadlock-free distributed programming. CAScrsupports the main theoretical results and construc-tions in the related article. CAScr takes the populartop-down approach to system development, basedon choreographic models, following the originalmethodology of Scribble and multiparty sessiontypes. The top-down approach enables correctness-by-construction: a developer provides a global de-scription for the whole communication protocol;by projecting the global protocol, APIs are gen-erated from local CFSMs, which ensure the safeimplementation of each participant. The theoryof choreography automata in the related articleguarantees deadlock freedom for the distributedimplementation of flexible global protocols. Wetarget web development, supporting in particularthe TypeScript programming language.

Conference paper

Gheri L, Lanese I, Sayers N, Tuosto E, Yoshida Net al., 2022, Design-by-contract for flexible multiparty session protocols, European Conference on Object-Oriented Programming (ECOOP 2022), Publisher: Schloss Dagstuhl, Leibniz-Zentrum, Pages: 1-28, ISSN: 1868-8969

Choreographic models support a correctness-by-construction principle in distributed programming. Also, they enable the automatic generation of correct message-based communication patterns from a global specification of the desired system behaviour. In this paper we extend the theory ofchoreography automata, a choreographic model based on finite-state automata, with two key features. First, we allow participants to act only in some of the scenarios described by the choreography automaton. While this seems natural, many choreographic approaches in the literature, andchoreography automata in particular, forbid this behaviour. Second, we equip communications with assertions constraining the values that can be communicated, enabling a design-by-contract approach. We provide a toolchain allowing to exploit the theory above to generate APIs for TypeScript web programming. Programs communicating via the generated APIs follow, by construction, the prescribed communication pattern and are free from communication errors such as deadlocks

Conference paper

Lagaillardie N, Neykova R, Yoshida N, 2022, Stay safe under panic: affine rust programming with multiparty session types, European Conference on Object-Oriented Programming (ECOOP)'22), Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, Pages: 4:1-4:29, ISSN: 1868-8969

Communicating systems comprise diverse software components across networks. To ensure theirrobustness, modern programming languages such as Rust provide both strongly typed channels,whose usage is guaranteed to be affine (at most once), and cancellation operations over binarychannels. For coordinating components to correctly communicate and synchronize with eachother, we use the structuring mechanism from multiparty session types, extending it with affinecommunication channels and implicit/explicit cancellation mechanisms. This new typing discipline,affine multiparty session types (AMPST), ensures cancellation termination of multiple, independentlyrunning components and guarantees that communication will not get stuck due to error or abrupttermination. Guided by AMPST, we implemented an automated generation tool (MultiCrusty) ofRust APIs associated with cancellation termination algorithms, by which the Rust compiler autodetects unsafe programs. Our evaluation shows that MultiCrusty provides an efficient mechanismfor communication, synchronization and propagation of the notifications of cancellation for arbitraryprocesses. We have implemented several usecases, including popular application protocols (OAuth,SMTP), and protocols with exception handling patterns (circuit breaker, distributed logging).

Conference paper

Gheri L, Lanese I, Sayers N, Tuosto E, Yoshida Net al., 2022, Design-By-Contract for Flexible Multiparty Session Protocols, ECOOP 2022, ISSN: 1868-8969

Choreographic models support a correctness-by-construction principle in distributed programming. Also, they enable the automatic generation of correct message-based communication patterns from a global specification of the desired system behaviour. In this paper we extend the theory of choreography automata, a choreographic model based on finite-state automata, with two key features. First, we allow participants to act only in some of the scenarios described by the choreography automaton. While this seems natural, many choreographic approaches in the literature, and choreography automata in particular, forbid this behaviour. Second, we equip communications with assertions constraining the values that can be communicated, enabling a design-by-contract approach. We provide a toolchain allowing to exploit the theory above to generate APIs for TypeScript web programming. Programs communicating via the generated APIs follow, by construction, the prescribed communication pattern and are free from communication errors such as deadlocks.

Conference paper

Gheri L, Lanese I, Sayers N, Tuosto E, Yoshida Net al., 2022, Design-by-Contract for Flexible Multiparty Session Protocols - Choreography Automata for distributed TypeScript programming (Artifact), ECOOP 2022

Conference paper

Barwell AD, Ferreira F, Yoshida N, 2022, Book review, Journal of Logical and Algebraic Methods in Programming, Vol: 125, Pages: 100744-100744, ISSN: 2352-2208

Journal article

Graversen E, Phillips I, Yoshida N, 2022, Event structures for the reversible early internal π-calculus, Journal of Logical and Algebraic Methods in Programming, Vol: 124, Pages: 1-46, ISSN: 2352-2208

The 휋-calculus is a widely used process calculus, which models communications between processes and allows the passing of communication links. Various operationalsemantics of the 휋-calculus have been proposed, which can be classified according towhether transitions are unlabelled (so-called reductions) or labelled. With labelled transitions, we can distinguish early and late semantics. The early version allows a processto receive names it already knows from the environment, while the late semantics andreduction semantics do not. All existing reversible versions of the 휋-calculus use reduction or late semantics, despite the early semantics of the (forward-only) 휋-calculusbeing more widely used than the late. We introduce two reversible forms of the internal 휋-calculus; these are the first to use early semantics. The internal 휋-calculus is asubset of the 휋-calculus where every link sent by an output is private, yielding greatersymmetry between inputs and outputs. One of the new reversible calculi uses staticreversibility, where performing an action does not change the structure of the process,and the other uses dynamic reversibility, where performing an action moves it to a separate history. We show an operational correspondence between the two calculi. Forthe static calculus we define denotational event structure semantics, which generate anevent structure inductively on the structure on the process. For the dynamic calculus wedefine operational event structure semantics, which generate an event structure basedon a labelled asynchronous transition system. We describe a correspondence betweenthe resulting event structures.

Journal article

Cutner Z, Yoshida N, Vassor M, 2022, Deadlock-Free Asynchronous Message Reordering in Rust with Multiparty Session Types, 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), Publisher: ASSOC COMPUTING MACHINERY, Pages: 246-261

Conference paper

Aceto L, Bertrand N, Yoshida N, 2021, INTERVIEWS WITH THE 2021 CONCUR TEST-OF-TIME AWARD RECIPIENTS, BULLETIN OF THE EUROPEAN ASSOCIATION FOR THEORETICAL COMPUTER SCIENCE, ISSN: 0252-9742

Journal article

Yoshida N, Ferreira Ruiz F, Zhou F, 2021, Communicating Finite State Machines and an Extensible Toolchain for Multiparty Session Types, FCT 2021 - 23rd International Symposium on Fundamentals of Computation Theory, Publisher: Springer Verlag, ISSN: 0302-9743

Conference paper

Bertrand N, Alfaro LD, Glabbeek RV, Palamidessi C, Yoshida Net al., 2021, CONCUR Test-Of-Time Award 2021, CONCUR 2021, ISSN: 1868-8969

This short article announces the recipients of the CONCUR Test-of-Time Award 2021.

Conference paper

Medic D, Mezzina CA, Phillips I, Yoshida Net al., 2021, Towards a formal account for software transactional memory, Twelfth International Conference on Reversible Computation, Publisher: Springer Verlag, Pages: 255-263, ISSN: 0302-9743

Software transactional memory (STM) is a concurrency con-trol mechanism for shared memory systems. It is opposite to the lockbased mechanism, as it allows multiple processes to access the same setof variables in a concurrent way. Then according to the used policy, theeffect of accessing to shared variables can be committed (hence, madepermanent) or undone. In this paper, we define a formal framework fordescribing STMs and show how with a minor variation of the rules it ispossible to model two common policies for STM: reader preference andwriter preference.

Conference paper

Toninho B, Yoshida N, 2021, On polymorphic sessions and functions: A tale of two (fully abstract) encodings, ACM Transactions on Programming Languages and Systems, Vol: 43, Pages: 1-55, ISSN: 0164-0925

This work exploits the logical foundation of session types to determine what kind of type discipline for the𝜋-calculus can exactly capture, and is captured by, 𝜆-calculus behaviours. Leveraging the proof theoreticcontent of the soundness and completeness of sequent calculus and natural deduction presentations of linearlogic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processesencodings between a polymorphic session 𝜋-calculus and a linear formulation of System F. We are then ableto derive results of the session calculus from the theory of the 𝜆-calculus: (1) we obtain a characterisation ofinductive and coinductive session types via their algebraic representations in System F; and (2) we extend ourresults to account for value and process passing, entailing strong normalisation.

Journal article

Castro-Perez D, Ferreira Ruiz F, Gheri L, Yoshida Net al., 2021, Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes, PLDI 2021, Publisher: Association for Computing Machinery (ACM), Pages: 237-251

We design and implement Zooid, a domain specific language for certified multiparty communication, embedded in Coq and implemented atop our mechanisation frame work of asynchronous multiparty session types (the first of its kind). Zooid provides a fully mechanised metatheory for the semantics of global and local types, and a fully verified end-point process language that faithfully reflects the type-level behaviours and thus inherits the global types properties such as deadlock freedom, protocol compliance, and liveness guarantees.

Conference paper

Yoshida N, Cutner Z, 2021, Safe session-based asynchronous coordination in rust, Coordination 2021, Publisher: Springer Verlag, Pages: 80-89, ISSN: 0302-9743

Rust is a popular systems language focused on performance and reliability, with an emphasis on providing “fearless concurrency”. Message passing has become a widely-used pattern by Rust developers although the potential for communication errors leaves developing safe and concurrent applications an unsolved challenge. In this ongoing work, we use multiparty session types to provide safety guarantees such as deadlock-freedom by coordinating message-passing processes. In contrast to previous contributions [22,21,20], our implementation targets asynchronous applications using a sync/await code in Rust. Specifically, we incorporate a synchronous subtyping theory, which allows program optimisation through reordering input and output actions. We evaluate our ideas by developing several representative use cases from the literature and by taking microbenchmarks. We discuss our plans to support full API generation integrating asynchronous optimisations.

Conference paper

Graversen E, Phillips I, Yoshida N, 2021, Event structure semantics of (controlled) reversible CCS, Journal of Logical and Algebraic Methods in Programming, Vol: 121, ISSN: 2352-2208

CCSK is a reversible form of CCS which is causal, meaning that actions can be reversed if and only if each action caused by them has already been reversed; there is no control on whether or when a computation reverses. We propose an event structure semantics for CCSK. For this purpose we define a category of reversible bundle event structures, and use the causal subcategory to model CCSK. We then modify CCSK to control the reversibility with a rollback primitive, which reverses a specific action and all actions caused by it. To define the event structure semantics of rollback, we change our reversible bundle event structures by making the conflict relation asymmetric rather than symmetric, and we exploit their capacity for non-causal reversibility.

Journal article

This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.

Request URL: http://wlsprd.imperial.ac.uk:80/respub/WEB-INF/jsp/search-html.jsp Request URI: /respub/WEB-INF/jsp/search-html.jsp Query String: respub-action=search.html&id=00365177&limit=30&person=true