300 results found
Yoshida N, Majumdar R, Zufferey D, 2020, Multiparty Motion Coordination: From Choreographies to Robotics Programs, OOPSLA 2020
Yoshida N, Griesemer R, Hu R, et al., 2020, Featherweight Go, OOPSLA 2020
Yoshida N, Zhou F, Ferreira F, et al., 2020, Statically Verified Refinements for Multiparty Protocols, OOPSLA 2020
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.
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, 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.
Medic D, Mezzina CA, Phillips I, et al., 2020, Towards a formal account for software transactional memory, Twelfth International Conference on Reversible Computation, Publisher: Springer Verlag, 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.
Yoshida N, Domart M-C, Peddie CJ, et al., 2020, The zebrafish as a novel model for the in vivo study of Toxoplasma gondii replication and interaction with macrophages, DISEASE MODELS & MECHANISMS, Vol: 13, ISSN: 1754-8403
Yoshida N, Jongmans S-S, 2020, Exploring type-level bisimilarity towards more expressive multiparty session types, 29th European Symposium on Programming
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.
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, ISSN: 1868-8969
Go is a popular concurrent programming language thanks to its ability to efficiently combineconcurrency and systems programming. In Go programs, a number of concurrency bugs can becaused by a mixture of data races and communication problems. In this paper, we develop atheory 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 thehappens-before relation defined in the Go memory model. We represent these properties of programsin aμ-calculus model of types, and validate them using type-level model-checking. We then extendthe framework to account for Go’s channels, and implement a static verification tool which can detectconcurrency errors. This is, to the best of our knowledge, the first static verification framework ofthis kind for the Go language, uniformly analysing concurrency errors caused by a mix of sharedmemory accesses and asynchronous message-passing communications.
Yoshida N, Imai K, Neykova R, et al., 2020, Multiparty session programming with global protocol combinators, 34th European Conference on Object-Oriented Programming, Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, ISSN: 1868-8969
Multiparty Session Types (MPST) is a typing discipline for communication protocols. It ensuresthe absence of communication errors and deadlocks for well-typed communicating processes. Thestate-of-the-art implementations of the MPST theory rely on (1)runtime linearity checksto ensurecorrect usage of communication channels and (2) external domain-specific languages for specifyingand verifying multiparty protocols.To overcome these limitations, we propose a library for programming withglobal combinators– a set of functions for writing and verifying multiparty protocols in OCaml. Local behavioursforallprocesses in a protocol are inferredat oncefrom a global combinator. We formalise globalcombinators and prove a sound realisability of global combinators – a well-typed global combinatorderives a set of local types, by which typed endpoint programs can ensure type and communicationsafety. Our approach enables fully-static verification and implementation of the whole protocol, fromthe 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 librarycan interoperate with existing libraries and services, implementing DNS (Domain Name Service)protocol and the OAuth (Open Authentication) protocol.
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
© IFIP International Federation for Information Processing 2020. 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, 2020, 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.
Yoshida N, Medic D, 2019, RELATIVE EXPRESSIVENESS OF CALCULI FOR REVERSIBLE CONCURRENCY, BULLETIN OF THE EUROPEAN ASSOCIATION FOR THEORETICAL COMPUTER SCIENCE, Pages: 89-119, ISSN: 0252-9742
Kouzapas D, Pérez JA, Yoshida N, 2019, On the relative expressiveness of higher-order session processes, Information and Computation, Vol: 268, Pages: 1-54, ISSN: 0890-5401
By integrating constructs from the λ-calculus and the π-calculus, in higher-order process calculiexchanged values may contain processes. This paper studies the relative expressiveness of HOπ,the higher-order π-calculus in which communications are governed by session types. Our maindiscovery is that HO, a subcalculus of HOπ which lacks name-passing and recursion, can serveas a new core calculus for session-typed higher-order concurrency. We show that HO can encodeHOπ fully abstractly (up to typed contextual equivalence) more precisely and efficiently than thefirst-order session π-calculus (π). Overall, under the discipline of session types, HOπ, HO, and πare equally expressive; however, we show that HOπ is more tightly related to HO than to π.
Bravetti M, Carbone M, Lange J, et al., 2019, A sound algorithm for asynchronous session subtyping, 30th International Conference on Concurrency Theory, Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, Pages: 38:1-38:16, ISSN: 1868-8969
Session types, types for structuring communication between endpoints in distributed systems, arerecently being integrated into mainstream programming languages. In practice, a very importantnotion for dealing with such types is that of subtyping, since it allows for typing larger classes ofsystem, where a program has not precisely the expected behavior 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 syntaxof session types or limit communication (by considering forms of bounded asynchrony). Bothapproaches are too restrictive in practice, hence we proceed differently by presenting an algorithm forchecking subtyping which is sound, but not complete (in some cases it terminates without returninga decisive verdict). The algorithm is based on a tree representation of the coinductive definition ofasynchronous subtyping; this tree could be infinite, and the algorithm checks for the presence offinite witnesses of infinite successful subtrees. Furthermore, we provide a tool that implements ouralgorithm and we apply it to many examples that cannot be managed with the previous approaches.
Lange J, Yoshida N, 2019, Verifying asynchronous interactions via communicating session automata, 31st International Conference on Computer-Aided Verification (CAV), Publisher: SPRINGER INTERNATIONAL PUBLISHING AG, Pages: 97-117, ISSN: 0302-9743
This paper proposes a sound procedure to verify properties of communicating session automata (csa), i.e., communicating automata that include multiparty session types. We introduce a new asynchronous compatibility property for csa, called k-multiparty compatibility (k-mc), which is a strict superset of the synchronous multiparty compatibility used in theories and tools based on session types. It is decomposed into two bounded properties: (i) a condition called k-safety which guarantees that, within the bound, all sent messages can be received and each automaton can make a move; and (ii) a condition called k-exhaustivity which guarantees that all k-reachable send actions can be fired within the bound. We show that k-exhaustivity implies existential boundedness, and soundly and completely characterises systems where each automaton behaves equivalently under bounds greater than or equal to k. We show that checking k-mc is pspace-complete, and demonstrate its scalability empirically over large systems (using partial order reduction).
Yoshida N, Neykova R, 2019, Featherweight Scribble, Models, Languages, and Tools for Concurrent and Distributed Programming, Editors: Boreale, Corradini, Loreti, Pugliese, Publisher: Springer, Pages: 236-259, ISBN: 978-3-030-21484-5
Thispapergivesaformaldefinitionoftheprotocolspeci-fication language Scribble. In collaboration with industry, Scribble hasbeen developed as an engineering incarnation of the formalmultipartysession types. In its ten years of development, Scribble has been appliedand extended in manyfold ways as to verify and ensure correctness ofconcurrent and distributed systems, e.g. type checking, runtime monitor-ing, code generation, and synthesis. This paper introduces a core versionof Scribble,Featherweight Scribble. We define the semantics of Scrib-ble by translation to communicating automata and show a behavioural-preserving encoding of Scribble protocols to multiparty session type.
Yoshida N, Majumdar R, Pirron M, et al., 2019, Motion session types for robotic interactions, European Conference on Object-Oriented Programming, Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, Pages: 28:1-28:27, ISSN: 1868-8969
Robotics applications involve programming concurrent components synchronising through messages while simultaneously executing motion primitives that control the state of the physical world. Today, these applications are typically programmed in low-level imperative programming languages which provide little support for abstraction or reasoning. We present a unifying programming model for concurrent message-passing systems that additionally control the evolution of physical state variables, together with a compositional reasoning framework based on multiparty session types. Our programming model combines message-passing concurrent processes with motion primitives. Processes represent autonomous components in a robotic assembly, such as a cart or a robotic arm, and they synchronise via discrete messages as well as via motion primitives. Continuous evolution of trajectories under the action of controllers is also modelled by motion primitives, which operate in global, physical time. We use multiparty session types as specifications to orchestrate discrete message-passing concurrency and continuous flow of trajectories. A global session type specifies the communication protocol among the components with joint motion primitives. A projection from a global type ensures that jointly executed actions at end-points are communication safe and deadlock-free, i.e., session-typed components do not get stuck. Together, these checks provide a compositional verification methodology for assemblies of robotic components with respect to concurrency invariants such as a progress property of communications as well as dynamic invariants such as absence of collision. We have implemented our core language and, through initial experiments, have shown how multiparty session types can be used to specify and compositionally verify robotic systems implemented on top of off-the-shelf and custom hardware using standard robotics application libraries.
King J, Ng N, Yoshida N, 2019, Multiparty Session Type-safe Web Development with Static Linearity, 11th Workshop on Programming Language Approaches to Concurrency- & Communication-cEntric Software, Publisher: OPEN PUBL ASSOC, Pages: 35-46, ISSN: 2075-2180
Altayeva A, Yoshida N, 2019, Service equivalence via multiparty session type isomorphisms, Publisher: arXiv
This paper addresses a problem found within the construction of Service Oriented Architecture: the adaptation of service protocols with respect to functional redundancy and heterogeneity of global communication patterns. We utilise the theory of Multiparty Session Types (MPST). Our approach is based upon the notion of a multiparty session type isomorphism, utilising a novel constructive realisation of service adapter code to establishing equivalence. We achieve this by employing trace semantics over a collection of local types and introducing meta abstractions over the syntax of global types. We develop a corresponding equational theory for MPST isomorphisms. The main motivation for this line of work is to define a type isomorphism that affords the assessment of whether two components/services are substitutables, modulo adaptation code given software components formalised as session types.
Bocchi L, Murgia M, Vasconcelos VT, et al., 2019, Asynchronous timed session types: from duality to time-sensitive processes, 28th European Symposium on Programming (ESOP) 2019, Publisher: Springer Verlag, ISSN: 0302-9743
We present a behavioural typing system for a higher-ordertimed calculus, using session types to model timed protocols, and thecalculus to abstract implementations. Behavioural typing ensures thatprocesses in the calculus will perform actions in the time-windows pre-scribed by their protocols. We introduce duality and subtyping for timedasynchronous session types. Duality includes a class of protocols that pre-vious work on asynchronous timed session types could not type-check.Subtyping is critical for precision of our typing system, especially forsession delegation. The composition of dual (timed asynchronous) typesenjoys progress when using an urgent receive semantics, in which receiveactions are executed as soon as the expected message is available. Ourcalculus increases the modelling power of calculi used in the previouswork on timed sessions, adding a blocking receive primitive with time-out, and a primitive that consumes an arbitrary amount of time in agiven range.
Castellan S, Yoshida N, 2019, Causality in Linear Logic: full completeness and injectivity (unit-free multiplicative-additive fragment), 22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Publisher: Springer Verlag, ISSN: 0302-9743
Commuting conversions of Linear Logic induce a notion of dependencybetween rules inside a proof derivation: a rule depends on a previous rule whenthey cannot be permuted using the conversions. We propose a new interpretation ofproofs of Linear Logic ascausal invariantswhich capturesexactlythis dependency.We represent causal invariants using game semantics based on general eventstructures, carving out, inside the model of , a submodel of causal invariants.This submodel supports an interpretation of unit-free Multiplicative AdditiveLinear Logic with MIX (MALL−) which is (1)fully complete: every element ofthe model is the denotation of a proof and (2)injective: equality in the modelcharacterises exactly commuting conversions of MALL−. This improves over thestandard fully complete game semantics model of MALL−.
Ghilezan S, Jaksic S, Pantovic J, et al., 2019, Precise subtyping for synchronous multiparty sessions, Journal of Logical and Algebraic Methods in Programming, Vol: 104, Pages: 127-173, ISSN: 2352-2208
This paper proves the soundness and completeness, together referred to as preciseness, of the subtyping relation for a synchronous multiparty session calculus.We address preciseness from operational and denotational viewpoints. The operational preciseness has been recently developed with respect to type safety, i.e., the safe replacement of a process of a smaller type in a context where a process of a bigger type is expected. The denotational preciseness is based on the denotation of a type: a mathematical object describing the meaning of the type, in accordance with the denotations of other expressions from the language.The main technical contribution of this paper is a novel proof strategy for the operational completeness of subtyping. We develop the notion of characteristic global type of a session type, which describes a deadlock-free circular communication protocol involving all participants appearing in . We prove operational completeness by showing that, if we place a process not conforming to a subtype of in a context that matches the characteristic global type of , then we obtain a deadlock. The denotational preciseness is proved as a corollary of the operational preciseness.
Graversen E, Phillips I, Yoshida N, 2019, Towards a categorical representation of reversible event structures, Journal of Logical and Algebraic Methods in Programming, Vol: 104, Pages: 16-59, ISSN: 2352-2208
We study categories for reversible computing, focussing on reversible forms of event structures. Event structures are a well-established model of true concurrency. There exist a number of forms of event structures, including prime event structures, asymmetric event structures, and general event structures. More recently, reversible forms of these types of event structure have been defined. We formulate corresponding categories and functors between them. We show that products and coproducts exist in many cases.We define stable reversible general event structures and stable configuration systems, and we obtain an isomorphism between the subcategory of the former in normal form and the finitely enabled subcategory of the latter. In most work on reversible computing, including reversible process calculi, a causality condition is posited, meaning that the cause of an event may not be reversed before the event itself. Since reversible event structures are not assumed to be causal in general, we also define causal subcategories of these event structures.Keywords: reversible computation, reversible event structures, category theory
Cogumbreiro T, Hu R, Martins F, et al., 2019, Dynamic deadlock verification for general barrier synchronisation, ACM Transactions on Programming Languages and Systems, Vol: 41, ISSN: 0164-0925
We present Armus, a verification tool for dynamically detecting or avoiding barrier deadlocks. The core designof Armus is based on phasers, a generalisation of barriers that supports split-phase synchronisation, dynamic membership, and optional-waits. This allows Armus to handle the key barrier synchronisation patterns found in modern languages and libraries. We implement Armus for X10 and Java, giving the first sound and complete barrier deadlock verification tools in these settings.Armus introduces a novel event-based graph model of barrier concurrency constraints that distinguishes task-event and event-task dependencies. Decoupling these two kinds of dependencies facilitates the verification of distributed barriers with dynamic membership, a challenging feature of X10. Our base graph representation can also be dynamically switched between a task-to-task model, Wait-for Graph (WFG), and an event-to-event model, State Graph (SG), to improve the scalability of the analysis. Formally, we show that the verification is sound and complete with respect to the occurrence of deadlock in our core phaser language; and that switching graph representations preserves the soundness and completeness properties. These results are machine checked with the Coq proof assistant. Practically, we evaluate theruntime overhead of our implementations using three benchmark suites in local and distributed scenarios. Regarding deadlock detection, distributed scenarios show negligible overheads and local scenarios show overheads below1. 15×. Deadlock avoidance is more demanding, and highlights the potential gains from dynamic graph selection. In one benchmark scenario, the runtime overheads vary from: 1.8× for dynamicselection, 2.6× for SG-static selection, and 5.9× for WFG-static selection.
Imai K, Yoshida N, Yuen S, 2019, Session-ocaml: a session-based library with polarities and lenses, Science of Computer Programming, Vol: 172, Pages: 135-159, ISSN: 0167-6423
We propose session-ocaml, a novel library for session-typed concurrent/distributed programming in OCaml. Our technique solely relies on parametric polymorphism, which can encode core session type structures with strong static guarantees. Our key ideas are: (1) polarised session types, which give an alternative formulation of duality enabling OCaml to automatically infer an appropriate session type in a session with a reasonable notational overhead; and (2) a parameterised monad with a data structure called ‘slots’ manipulated with lenses, which can statically enforce session linearity including delegations. We introduce a notational extension to enhance the session linearity for integrating the session types into the functional programming style. We show applications of session-ocaml to a travel agency use case and an SMTP protocol implementation. Furthermore, we evaluate the performance of Image 1 on a number of benchmarks.
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.