Publications
368 results found
Demangeon R, Yoshida N, 2023, Causal computational complexity of distributed processes, Information and Computation, Vol: 290, ISSN: 0890-5401
This article studies the complexity of π-calculus processes with respect to the quantity of transitions caused by an incoming message. First, we propose a typing system for integrating Bellantoni and Cook's characterisation of polytime computable functions into Deng and Sangiorgi's typing system for termination. We then define computational complexity of distributed messages based on Degano and Priami's causal semantics, which identifies the dependency between interleaved transitions. Next, we apply a necessary syntactic flow analysis to typable processes to ensure a computational bound on the number of distributed messages. We prove that our analysis is decidable; sound in the sense that it guarantees that the total number of messages causally dependent of an input request received from the outside is bounded by a polynomial of the content of this request; and complete, meaning that each polynomial recursive function can be computed by a typable process.
Vasconcelos VT, Martins F, Lopez H-A, et al., 2022, A Type Discipline for Message Passing Parallel Programs, ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, Vol: 44, ISSN: 0164-0925
Ellis S, Zhu S, Yoshida N, et al., 2022, Generic go to go: dictionary-passing, monomorphisation, and hybrid, Proceedings of the ACM on Programming Languages, Vol: 6, Pages: 1207-1235
<jats:p>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.</jats:p> <jats:p>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.</jats:p>
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.
Peters K, Yoshida N, 2022, On the Expressiveness of Mixed Choice Sessions, Electronic Proceedings in Theoretical Computer Science, Vol: 368, Pages: 113-130
Barwell AD, Scalas A, Yoshida N, et al., 2022, Generalised Multiparty Session Types with Crash-Stop Failures (Technical Report)
Session types enable the specification and verification of communicatingsystems. However, their theory often assumes that processes never fail. Toaddress 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 {\pi}-calculus andtypes: we model crashes and their handling semantically, with a generalisedMPST typing system parametric on a behavioural safety property. We cover thespectrum between fully reliable and fully unreliable sessions, via optionalreliability assumptions, and prove type safety and protocol conformance in thepresence of crash-stop failures. Introducing crash-stop failures has non-trivial consequences: writing correctprocesses that handle all crash scenarios can be difficult. Yet, ourgeneralised MPST theory allows us to tame this complexity, via model checking,to validate whether a multiparty session satisfies desired behaviouralproperties, e.g. deadlock-freedom or liveness, even in presence of crashes. Weimplement our approach using the mCRL2 model checker, and evaluate it withexamples extended from the literature.
Barwell A, Scalas A, Yoshida N, et al., 2022, Generalised multiparty session types with crash-stop failures, International Conference on Concurrency Theory (CONCUR), Publisher: Schloss Dagstuhl, 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
Gheri L, Lanese I, Sayers N, et 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.
Gheri L, Lanese I, Sayers N, et al., 2022, Design-by-Contract for Flexible Multiparty Session Protocols -- Extended Version
Choreographic models support a correctness-by-construction principle indistributed programming. Also, they enable the automatic generation of correctmessage-based communication patterns from a global specification of the desiredsystem 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 bythe choreography automaton. While this seems natural, many choreographicapproaches in the literature, and choreography automata in particular, forbidthis behaviour. Second, we equip communications with assertions constrainingthe values that can be communicated, enabling a design-by-contract approach. Weprovide a toolchain allowing to exploit the theory above to generate APIs forTypeScript web programming. Programs communicating via the generated APIsfollow, by construction, the prescribed communication pattern and are free fromcommunication errors such as deadlocks.
Gheri L, Lanese I, Sayers N, et al., 2022, Design-by-Contract for Flexible Multiparty Session Protocols - Choreography Automata for distributed TypeScript programming (Artifact), ECOOP 2022
Gheri L, Lanese I, Sayers N, et al., 2022, Design-by-contract for flexible multiparty session protocols - choreography automata for distributed TypeScript programming (Artifact), ECOOP 2022 (Artifacts Evaluation)
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.
Gheri L, Lanese I, Sayers N, et al., 2022, Design-by-contract for flexible multiparty session protocols - choreography automata for distributed typescript programming, European Conference on Object-Oriented Programming (ECOOP 2022)
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
Yoshida N, Lagaillardie N, Neykova R, 2022, Stay safe under panic: affine rust programming with multiparty session types, European Conference on Object-Oriented Programming (ECOOP'22)
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).
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
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
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.
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
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
Bertrand N, Alfaro LD, Glabbeek RV, et 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.
Medic D, Mezzina CA, Phillips I, et 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.
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.
Castro-Perez D, Ferreira Ruiz F, Gheri L, et 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.
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.
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.
Castro-Perez D, Ferreira F, Gheri L, et al., 2021, Zooid: a DSL for Certified Multiparty Computation
We design and implement Zooid, a domain specific language for certifiedmultiparty communication, embedded in Coq and implemented atop ourmechanisation framework of asynchronous multiparty session types (the first ofits kind). Zooid provides a fully mechanised metatheory for the semantics ofglobal and local types, and a fully verified end-point process language thatfaithfully reflects the type-level behaviours and thus inherits the globaltypes properties such as deadlock freedom, protocol compliance, and livenessguarantees.
Bravetti M, Carbone M, Lange J, et al., 2021, A sound algorithm for asynchronous session subtyping and its implementation, Logical Methods in Computer Science, Vol: 17, Pages: 1-35, ISSN: 1860-5974
Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of subtyping, since it allows for typing larger classes of system, where a program has not precisely the expected behaviour but a similar one. Unfortunately, recent work has shown that subtyping for session types in an asynchronous setting is undecidable. To cope with this negative result, the only approaches we are aware of either restrict the syntax of session types or limit communication (by considering forms of bounded asynchrony). Both approaches are too restrictive in practice, hence we proceed differently by presenting an algorithm for checking subtyping which is sound, but not complete (in some cases it terminates without returning a decisive verdict). The algorithm is based on a tree representation of the coinductive definition of asynchronous subtyping; this tree could be infinite, and the algorithm checks for the presence of finite witnesses of infinite successful subtrees. Furthermore, we provide a tool that implements our algorithm. We use this tool to test our algorithm on many examples that cannot be managed with the previous approaches, and to provide an empirical evaluation of the time and space cost of the algorithm.
Miu A, Ferreira Ruiz F, Yoshida N, et al., 2021, Communication-safe web programming in TypeScript with routed multiparty session types, The International Conference on Compiler Construction (CC), Publisher: ACM, Pages: 94-106
Modern web programming involves coordinating interactions between browser clients and a server. Typically, the interactions in web-based distributed systems are informally described, making it hard to ensure correctness, especially communication safety, i.e. all endpoints progress without type errors or deadlocks, conforming to a specified protocol.We present STScript, a toolchain that generates TypeScript APIs for communication-safe web development over WebSockets, and RouST, a new session type theory that supports multiparty communications with routing mechanisms. STScript provides developers with TypeScript APIs generated from a communication protocol specification based on RouST. The generated APIs build upon TypeScript concurrency practices, complement the event-driven style of programming in full-stack web development, and are compatible with the Node.js runtime for server-side endpoints and the React.js framework for browser-side endpoints.RouST can express multiparty interactions routed via an intermediate participant. It supports peer-to-peer communication between browser-side endpoints by routing communication via the server in a way that avoids excessive serialisation. RouST guarantees communication safety for endpoint web applications written using STScript APIs.We evaluate the expressiveness of STScript for modern web programming using several production-ready case studies deployed as web applications.
Miu A, Ferreira F, Yoshida N, et al., 2021, Communication-Safe Web Programming in TypeScript with Routed Multiparty Session Types
Please refer to the README on https://github.com/STScript-2020/cc21-artifact/blob/main/README.md
Ghilezan S, Pantović J, Prokić I, et al., 2021, Precise subtyping for asynchronous multiparty sessions, POPL 2021, Publisher: Association for Computing Machinery (ACM), Pages: 1-28, ISSN: 2475-1421
Session subtyping is a cornerstone of refinement of communicating processes: a process implementing a session type (i.e., a communication protocol) T can be safely used whenever a process implementing one of its supertypes T′ is expected, in any context, without introducing deadlocks nor other communication errors. As a consequence, whenever T T′ holds, it is safe to replace an implementation of T′ with an implementation of the subtype T, which may allow for more optimised communication patterns.We present the first formalisation of the precise subtyping relation for asynchronous multiparty sessions. We show that our subtyping relation is sound (i.e., guarantees safe process replacement, as outlined above) and also complete: any extension of the relation is unsound. To achieve our results, we develop a novel session decomposition technique, from full session types (including internal/external choices) into single input/output session trees (without choices).Previous work studies precise subtyping for binary sessions (with just two participants), or multiparty sessions (with any number of participants) and synchronous interaction. Here, we cover multiparty sessions with asynchronous interaction, where messages are transmitted via FIFO queues (as in the TCP/IP protocol), and prove that our subtyping is both operationally and denotationally precise. In the asynchronous multiparty setting, finding the precise subtyping relation is a highly complex task: this is because, under some conditions, participants can permute the order of their inputs and outputs, by sending some messages earlier or receiving some later, without causing errors; the precise subtyping relation must capture all such valid permutations — and consequently, its formalisation, reasoning and proofs become challenging. Our session decomposition technique overcomes this complexity, expressing the subtyping relation as a composition of refinement relations between single input/outpu
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.