316 results found
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
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)
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, 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.
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.
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
Yoshida N, 2021, Preface, ISBN: 9783030720186
This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality inπ-calculus, which differ in the treatment of parallel extrusions of the same name. Hence, by using a parametric way of bookkeeping the order and the dependencies among extruders it is possible to map different causal semantics into the same framework. Starting from this simple observation, we present a uniform framework forreversibleπ-calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Different data structures yield different approaches to the parallel extrusion problem. We map three well-known causal semantics into our framework. We prove causal-consistency for the three instances of our framework. Furthermore, we prove a causal correspondence between the appropriate instances of the framework and the Boreale-Sangiorgi semantics and an operational correspondence with the reversibleπ-calculus causal semantics.
Imai K, Neykova R, Yoshida N, et al., 2020, Multiparty session programming with global protocol combinators, 34th European Conference on Object-Oriented Programming, Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, Pages: 9:1-9:30, ISSN: 1868-8969
Multiparty Session Types (MPST) is a typing discipline for communication protocols. It ensures the absence of communication errors and deadlocks for well-typed communicating processes. The state-of-the-art implementations of the MPST theory rely on (1) runtime linearity checks to ensure correct usage of communication channels and (2) external domain-specific languages for specifying and verifying multiparty protocols. To overcome these limitations, we propose a library for programming with global combinators - a set of functions for writing and verifying multiparty protocols in OCaml. Local behaviours for all processes in a protocol are inferred at once from a global combinator. We formalise global combinators and prove a sound realisability of global combinators - a well-typed global combinator derives a set of local types, by which typed endpoint programs can ensure type and communication safety. Our approach enables fully-static verification and implementation of the whole protocol, from the protocol specification to the process implementations, to happen in the same language. We compare our implementation to untyped and continuation-passing style implementations, and demonstrate its expressiveness by implementing a plethora of protocols. We show our library can interoperate with existing libraries and services, implementing DNS (Domain Name Service) protocol and the OAuth (Open Authentication) protocol.
Gabet J, Yoshida N, 2020, Static race detection and mutex safety and liveness for Go programs, 34th European Conference on Object-Oriented Programming (ECOOP) 2020, Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, Pages: 4:1-4:30, ISSN: 1868-8969
Go is a popular concurrent programming language thanks to its ability to efficiently combine concurrency and systems programming. In Go programs, a number of concurrency bugs can be caused by a mixture of data races and communication problems. In this paper, we develop a theory based on behavioural types to statically detect data races and deadlocks in Go programs. We first specify lock safety/liveness and data race properties over a Go program model, using the happens-before relation defined in the Go memory model. We represent these properties of programs in a μ-calculus model of types, and validate them using type-level model-checking. We then extend the framework to account for Go’s channels, and implement a static verification tool which can detect concurrency errors. This is, to the best of our knowledge, the first static verification framework of this kind for the Go language, uniformly analysing concurrency errors caused by a mix of shared memory accesses and asynchronous message-passing communications.
Zhou F, Ferreira F, Hu R, et al., 2020, Statically verified refinements for multiparty protocols, OOPSLA 2020, Publisher: Association for Computing Machinery (ACM), ISSN: 2475-1421
With distributed computing becoming ubiquitous in the modern era, safe distributed programming is an open challenge. To address this, multiparty session types (MPST) provide a typing discipline for message-passing concurrency, guaranteeing communication safety properties such as deadlock freedom.While originally MPST focus on the communication aspects, and employ a simple typing system for communication payloads, communication protocols in the real world usually contain constraints on the payload. We introduce refined multiparty session types (RMPST), an extension of MPST, that express data dependent protocols via refinement types on the data types.We provide an implementation of RMPST, in a toolchain called Session*, using Scribble, a toolchain for multiparty protocols, and targeting F*, a verification-oriented functional programming language. Users can describe a protocol in Scribble and implement the endpoints in F* using refinement-typed APIs generated from the protocol. The F* compiler can then statically verify the refinements. Moreover, we use a novel approach of callback-styled API generation, providing static linearity guarantees with the inversion of control. We evaluate our approach with real world examples and show that it has little overhead compared to a naive implementation, while guaranteeing safety properties from the underlying theory.
Castro-Perez D, Yoshida N, 2020, CAMP: cost-aware multiparty session protocols, OOPSLA 2020, Publisher: Association for Computing Machinery (ACM), ISSN: 2475-1421
This paper presents CAMP, a new static performance analysis framework for message-passing concurrent and distributed systems, based on the theory of multiparty session types (MPST). Understanding the runtime performance of concurrent and distributed systems is of great importance for the identification ofbottlenecks and optimisation opportunities. In the message-passing setting, these bottlenecks are generallycommunication overheads and synchronisation times. Despite its importance, reasoning about these intensionalproperties of software, such as performance, has received little attention, compared to verifying extensionalproperties, such as correctness. Behavioural protocol specifications based on sessions types capture notonly extensional, but also intensional properties of concurrent and distributed systems. CAMP augmentsMPST with annotations of communication latency and local computation cost, defined as estimated executiontimes, that we use to extract cost equations from protocol descriptions. CAMP is also extendable to analyseasynchronous communication optimisation built on a recent advance of session type theories. We apply ourtool to different existing benchmarks and use cases in the literature with a wide range of communication protocols, implemented in C, MPI-C, Scala, Go, and OCaml. Our benchmarks show that, in most of the cases,we predict an upper-bound on the real execution costs with < 15% error.
Majumdar R, Yoshida N, Zufferey D, 2020, Multiparty motion coordination: from choreographies to robotics programs, OOPSLA 2020, Publisher: Association for Computing Machinery (ACM), ISSN: 2475-1421
We present a programming model and typing discipline for complex multi-robot coordination programming. Our model encompasses both synchronisation through message passing and continuous-time dynamic motion primitives in physical space. We specify continuous-time motion primitives in an assume-guarantee logic that ensures compatibility of motion primitives as well as collision freedom. We specify global behaviour of programs in a choreographic type system that extends multiparty session types with jointly executed motion primitives, predicated refinements, as well as a separating conjunction that allows reasoning about subsets of interacting robots. We describe a notion of well-formedness for global types that ensures motion and communication can be correctly synchronised and provide algorithms for checking well-formedness, projecting a type, and local type checking. A well-typed program is communication safe, motion compatible, and collision free. Our type system provides a compositional approach to ensuring these properties. We have implemented our model on top of the ROS framework. This allows us to program multi-robot coordination scenarios on top of commercial and custom robotics hardware platforms. We show through case studies that we can model and statically verify quite complex manoeuvres involving multiple manipulators and mobile robots---such examples are beyond the scope of previous approaches.
We describe a design for generics in Go inspired by previous work on Featherweight Java by Igarashi, Pierce, and Wadler. Whereas subtyping in Java is nominal, in Go it is structural, and whereas generics in Java are defined via erasure, in Go we use monomorphisation. Although monomorphisation is widely used, we are one of the first to formalise it. Our design also supports a solution to The Expression Problem.
Majumdar R, Yoshida N, Zufferey D, 2020, Multiparty Motion Coordination: From Choreographies to Robotics Programs (Artifact)
Software artifact for the paper "Multiparty Motion Coordination: From Choreographies to Robotics Programs" submitted to OOPSLA 2020The artifact has been packaged into a virtual machine (Ubuntu 20.04). The username and password for the virtual machine is "pgcd".
Griesemer R, Hu R, Kokke W, et al., 2020, Featherweight Go (Artifact)
This paper presents Featherweight Go (FG) and Featherweight Generic Go (FGG), a core calculus of Go and a proposal for extending it with F-bounded polymorphism. The calculi are in the same vein as Featherweight Java (FJ), but where Featherweight Generic Java (FGJ) was translated into FJ via erasure, FGG translates into FG via monomorphization (which is also formalized). The two calculi are proven sound using the normal progress and preservation arguments. Additionally a bisimulation is shown to exist between a FGG program and its monomorphization (if it exists); in other words that monomorphization preserves the semantics of the program.The artifact consists of an implementation of type checkers and interpreters for FG and FGG, as well as a monomorphization procedure (including the check if it is possible). It includes the examples from the paper, and a comparison using the Go compiler as reference. Type preservation and bisimulation for these programs are tested dynamically. Additionally, the same is tested for all well-typed programs up to a certain size (which are generated in a manner similar to property-based testing).
Castro-Perez D, Yoshida N, 2020, CAMP: Cost-Aware Multiparty Session Protocols (artifact)
This is the artifact for the paper *CAMP: Cost-Aware Multiparty Session Protocols*.The artifact comprises:- A library for specifying cost-aware multiparty protocols.- The raw data used for comparing the cost models with real execution costs.- The cost-aware protocol specifications of the benchmarks that we studied.The library for specifying cost-aware protocols also provides functions forextracting cost equations from them, and for estimating recursive protocollatencies (i.e. average cost per protocol iteration). We provide a script forextracting cost equations, and instantiating them using the parameters used inthe paper.
Zhou F, Ferreira F, Hu R, et al., 2020, Statically verified refinements for multiparty protocols, Publisher: arXiv
With distributed computing becoming ubiquitous in the modern era, safedistributed programming is an open challenge. To address this, multipartysession types (MPST) provide a typing discipline for message-passingconcurrency, guaranteeing communication safety properties such as deadlockfreedom. While originally MPST focus on the communication aspects, and employ a simpletyping system for communication payloads, communication protocols in the realworld usually contain constraints on the payload. We introduce refinedmultiparty session types (RMPST), an extension of MPST, that express datadependent protocols via refinement types on the data types. We provide an implementation of RMPST, in a toolchain called Session*, usingScribble, a multiparty protocol description toolchain, and targeting F*, averification-oriented functional programming language. Users can describe aprotocol in Scribble and implement the endpoints in F* using refinement-typedAPIs generated from the protocol. The F* compiler can then statically verifythe refinements. Moreover, we use a novel approach of callback-styled APIgeneration, providing static linearity guarantees with the inversion ofcontrol. We evaluate our approach with real world examples and show that it haslittle overhead compared to a na\"ive implementation, while guaranteeing safetyproperties from the underlying theory.
Zhou F, Ferreira F, Hu R, et al., 2020, Statically Verified Refinements for Multiparty Protocols
Statically Verified Refinements for Multiparty Protocols
Graversen E, Phillips I, Yoshida N, 2020, Event structures for the reversible early internal pi-calculus, Twelfth International Conference on Reversible Computation, Publisher: Springer Verlag, Pages: 71-90, ISSN: 0302-9743
The pi-calculus is a widely used process calculus, which models com-munications between processes and allows the passing of communication links.Various operational semantics of the pi-calculus have been proposed, which canbe classified according to whether transitions are unlabelled (so-called reductions)or labelled. With labelled transitions, we can distinguish early and late semantics.The early version allows a process to receive names it already knows from the en-vironment, while the late semantics and reduction semantics do not. All existingreversible versions of the pi-calculus use reduction or late semantics, despite theearly semantics of the (forward-only) pi-calculus being more widely used than thelate. We define piIH, the first reversible early pi-calculus, and give it a denotationalsemantics in terms of reversible bundle event structures. The new calculus is a re-versible form of the internal pi-calculus, which is a subset of the pi-calculus whereevery link sent by an output is private, yielding greater symmetry between inputsand outputs.
Yoshida N, Jongmans S-S, 2020, Exploring type-level bisimilarity towards more expressive multiparty session types, 29th European Symposium on Programming, Publisher: Springer, Pages: 251-279
A key open problem with multiparty session types (MPST)concerns their expressiveness: current MPST have inflexible choice, noexistential quantification over participants, and limited parallel compo-sition. This precludes many real protocols to be represented by MPST.To overcome these bottlenecks of MPST, we explore a new techniqueusing weak bisimilarity between global types and endpoint types, whichguarantees deadlock-freedom and absence of protocol violations. Basedon a process algebraic framework, we present well-formed conditions forglobal types that guarantee weak bisimilarity between a global type andits endpoint types and prove their check is decidable. Our main practicalresult, obtained through benchmarks, is that our well-formedness condi-tions can be checked orders of magnitude faster than directly checkingweak bisimilarity using a state-of-the-art model checker.
Miu A, Ferreira F, Yoshida N, et al., 2020, Generating Interactive WebSocket Applications in TypeScript, Electronic Proceedings in Theoretical Computer Science, Vol: 314, Pages: 12-22
Castro-Perez D, Yoshida N, 2020, Compiling first-order functions to session-typed parallel code, ACM SIGPLAN 2020 International Conference on Compiler Construction (CC 2020), Publisher: ACM, Pages: 143-154
Building correct and efficient message-passing parallel pro-grams still poses many challenges. The incorrect use ofmessage-passing constructs can introduce deadlocks, anda bad task decomposition will not achieve good speedups.Current approaches focus either on correctness or efficiency,but limited work has been done on ensuring both. In thispaper, we propose a new parallel programming framework,PAlg, which is a first-order language withparticipant anno-tationsthat ensuresdeadlock-freedom by construction.PAlgprograms are coupled with an abstraction of their communi-cation structure, aglobal typefrom the theory ofmultipartysession types(MPST). This global type serves as an outputfor the programmer to assess the efficiency of their achievedparallelisation.PAlgis implemented as an EDSL in Haskell,from which we can: 1. compile to low-level message-passingC code; 2. compile to sequential C code, or interpret as se-quential Haskell functions; and, 3. infer the communicationprotocol followed by the compiled message-passing program.We use the properties of the inferred global types to performbasic message reordering optimisations to the compiled Ccode. We prove theextensional equivalenceof our outputparallelisation, as well as theprotocol compliance. We eval-uate our approach on a number of benchmarks. We achievelinear speedups on a shared-memory 12-core machine, anda speedup of 16 on a 2-node, 24-core NUMA.
Lagaillardie N, Neykova R, Yoshida N, 2020, Implementing multiparty session types in rust, Pages: 127-136, ISBN: 9783030500283
Multiparty Session Types (MPST) is a typing discipline for distributed protocols, which ensures communication safety and deadlock-freedom for more than two participants. This paper reports on our research project, implementing multiparty session types in Rust. Current Rust implementations of session types are limited to binary (two-party communications). We extend an existing library for binary session types to MPST. We have implemented a simplified Amazon Prime Video Streaming protocol using our library for both shared and distributed communication transports.
Ferreira Ruiz F, Yoshida N, Castro-Perez D, 2019, EMTST engineering the meta-theory of session types, International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Gheri L, Yoshida N, 2019, A Very Gentle Introduction to Multiparty Session Types, International Conference on Distributed Computing and Internet Technology
Yoshida N, Castro D, Ferreira F, 2019, EMTST - Engineering Meta-theory of Session Types
A Coq library to implement and reason about Session types. Together with a subject reduction for binary session types.
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.