360 results found
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.
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 - 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 (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, 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
Cutner Z, Yoshida N, Vassor M, 2022, Deadlock-Free Asynchronous Message Reordering in Rust with Multiparty Session Types, Pages: 246-261
Rust is a modern systems language focused on performance and reliability. Complementing Rust's promise to provide "fearless concurrency", developers frequently exploit asynchronous message passing. Unfortunately, sending and receiving messages in an arbitrary order to maximise computation-communication overlap (a popular optimisation in message-passing applications) opens up a Pandora's box of subtle concurrency bugs. To guarantee deadlock-freedom by construction, we present Rumpsteak: a new Rust framework based on multiparty session types. Previous session type implementations in Rust are either built upon synchronous and blocking communication and/or are limited to two-party interactions. Crucially, none support the arbitrary ordering of messages for efficiency. Rumpsteak instead targets asynchronous async/await code. Its unique ability is allowing developers to arbitrarily order send/receive messages while preserving deadlock-freedom. For this, Rumpsteak incorporates two recent advanced session type theories: (1) k-multiparty compatibility (k-MC), which globally verifies the safety of a set of participants, and (2) asynchronous multiparty session subtyping, which locally verifies optimisations in the context of a single participant. Specifically, we propose a novel algorithm for asynchronous subtyping that is both sound and decidable. We first evaluate the performance and expressiveness of Rumpsteak against three previous Rust implementations. We discover that Rumpsteak is around 1.7 - 8.6x more efficient and can safely express many more examples by virtue of offering arbitrary ordering of messages. Secondly, we analyse the complexity of our new algorithm and benchmark it against k-MC and a binary session subtyping algorithm. We find they are exponentially slower than Rumpsteak's.
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
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.
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
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.
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
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.
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.
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 (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".
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.