Publications
373 results found
Viering M, Chen T-C, Eugster P, et al., 2018, A typing discipline for statically verified crash failure handling in distributed systems, ESOP 2018, Publisher: Springer, Pages: 799-826, ISSN: 0302-9743
A key requirement for many distributed systems is to be resilient toward partial failures, allowing a system to progress despite the failure of some components. This makes programming of such systems daunting, particularly in regards to avoiding inconsistencies due to failures and asynchrony. This work introduces a formal model for crash failure handling in asynchronous distributed systems featuring a lightweight coordinator, modeled in the image of widely used systems such as ZooKeeper and Chubby. We develop a typing discipline based on multiparty session types for this model that supports the specification and static verification of multiparty protocols with explicit failure handling. We show that our type system ensures subject reduction and progress in the presence of failures. In other words, in a well-typed system even if some participants crash during execution, the system is guaranteed to progress in a consistent manner with the remaining participants.
Castellan S, Clairambault P, Hayman J, et al., 2018, Non-angelic concurrent game semantics, FoSSaCS 2018 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Publisher: Springer, Pages: 3-19
The hiding operation, crucial in the compositional aspect of game semantics, removes computation paths not leading to observable results. Accordingly, games models are usually biased towards angelic non-determinism: diverging branches are forgotten.We present here new categories of games, not suffering from this bias. In our first category, we achieve this by avoiding hiding altogether; instead morphisms are uncovered strategies (with neutral events) up to weak bisimulation. Then, we show that by hiding only certain events dubbed inessential we can consider strategies up to isomorphism, and still get a category – this partial hiding remains sound up to weak bisimulation, so we get a concrete representations of programs (as in standard concurrent games) while avoiding the angelic bias. These techniques are illustrated with an interpretation of affine nondeterministic PCF which is adequate for weak bisimulation; and may, must and fair convergences.
Parente Coutinho Fernandes Toninho B, Yoshida N, 2018, On polymorphic sessions and functions: A talk of two (fully abstract) encodings, ESOP 2018 27th European Symposium on Programming (ESOP), Publisher: Springer, Pages: 827-855
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 theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π -calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the λ -calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.
Yoshida N, Parente Coutinho Fernandes Toninho B, 2018, Depending on session typed process, FoSSaCS 2018 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Publisher: Springer, Pages: 128-145
This work proposes a dependent type theory that combines functions and session-typed processes (with value dependencies) through a contextual monad, internalising typed processes in a dependently-typed λ -calculus. The proposed framework, by allowing session processes to depend on functions and vice-versa, enables us to specify and statically verify protocols where the choice of the next communication action can depend on specific values of received data. Moreover, the type theoretic nature of the framework endows us with the ability to internally describe and prove predicates on process behaviours. Our main results are type soundness of the framework, and a faithful embedding of the functional layer of the calculus within the session-typed layer, showcasing the expressiveness of dependent session types.
Neykova R, Hu R, Yoshida N, et al., 2018, Session type providers: Compile-time API generation for distributed protocols with interaction refinements in F#, International Conference on Compiler Construction, Publisher: ACM, Pages: 128-138
We present a library for the specification and implementation of distributed protocols in native F# (and other .NET languages) based on multiparty session types (MPST). There are two main contributions. Our library is the first practical development of MPST to support what we refer to as interaction refinements: a collection of features related to the refinement of protocols, such as message-type refinements (value constraints) and message value dependent control flow. A well-typed endpoint program using our library is guaranteed to perform only compliant session I/O actions w.r.t. to the refined protocol, up to premature termination.Second, our library is developed as a session type provider, that performs on-demand compile-time protocol validation and generation of protocol-specific .NET types for users writing the distributed endpoint programs. It is implemented by extending and integrating Scribble (a toolchain for MPST) with an SMT solver into the type providers framework. The safety guarantees are achieved by a combination of static type checking of the generated types for messages and I/O operations, correctness by construction from code generation, and automated inlining of assertions.
Scalas A, Yoshida N, 2018, Less is more: multiparty session types revisited, Departmental Technical Report: 18/6, Publisher: Department of Computing, Imperial College London
Multiparty Session Types (MPST) are a typing discipline ensuring that a message-passing process implementsa given multiparty session protocol, without errors. In this paper, we propose a new, generalised MPST theory.Our contribution is fourfold. (1) We demonstrate that a revision of the theoretical foundations of MPST isnecessary: classic MPST have a limited subject reduction property, with inherent restrictions that are easilyoverlooked, and in previous work have led to flawed type safety proofs; our new theory removes suchrestrictions and fixes such flaws. (2) We contribute a new MPST theory that is less complicated, and yet moregeneral, than the classic one: it does not require global multiparty session types nor binary session type duality— instead, it is grounded on general behavioural type-level properties, and proves type safety of many moreprotocols and processes. (3) We produce a detailed analysis of type-level properties, showing how, in our newtheory, they allow to ensure decidability of type checking, and statically guarantee that processes enjoy, e.g.,deadlock-freedom and liveness at run-time. (4) We show how our new theory can integrate type and modelchecking: type-level properties can be expressed in modal μ-calculus, and verified with well-established tools.
Castro D, Hu R, Jongmans S-S, et al., 2018, Distributed programming using role-parametric session types in go, Departmental Technical Report: 18/4, Publisher: Department of Computing, Imperial College London
This paper presents a framework for the static specification and safe programming of message passing protocolswhere the number and kinds of participants are dynamically instantiated.We develop the first theory of distributed multiparty session types (MPST) to support parameterisedprotocols with indexed rolesÐour framework statically infers the different kinds of participants inducedby a protocol definition as role variants, and produces decoupled endpoint projections of the protocol ontoeach variant. This enables safe MPST-based programming of the parameterised endpoints in distributedsettings: each endpoint can be implemented separately by different programmers, using different techniques(or languages). We prove the decidability of role variant inference and well-formedness checking, and thecorrectness of projection.We implement our theory as a toolchain for programming such role-parametric MPST protocols in Go. Ourapproach is to generate API families of lightweight, protocol- and variant-specific type wrappers for I/O. TheAPIs ensure a well-typed Go endpoint program (by native Go type checking) will perform only compliantI/O actions w.r.t. the source protocol. We leverage the abstractions of MPST to support the specification andimplementation of Go applications involving multiple channels, possibly over mixed transports (e.g., Gochannels, TCP), and channel passing via a unified programming interface. We evaluate the applicability andrun-time performance of our generated APIs using microbenchmarks and real-world applications.
Castellan S, Yoshida N, 2018, Two sides of the same coin: session types and game semantics, Departmental Technical Report: 18/5, Publisher: Department of Computing, Imperial College London
Game semantics and session types are two formalisations of the same concept: message-passing open programsfollowing certain protocols. Game semantics represents protocols as games, and programs as strategies; whilesession types specify protocols, and well-typed π-calculus processes model programs. Giving faithful modelsof the π-calculus and giving a precise description of strategies as a programming language are two difficultproblems. In this paper, we show how these two problems can be tackled at the same time by building anaccurate game semantics model of the session π-calculus.Our main contribution is to fill a semantic gap between the synchrony of the (session) π-calculus and theasynchrony of game semantics, by developing an event-structure based game semantics for synchronousconcurrent computation. This model supports the first truly concurrent fully abstract (for barbed congruence)interpretation of the synchronous (session) π-calculus.We further strengthen this correspondence, establishingfinite definability of asynchronous strategies by the internal session π-calculus. As an application of theseresults, we propose a faithful encoding of synchronous strategies into asynchronous strategies by call-returnprotocols, which induces automatically an encoding at the level of processes. Our results bring session typesand game semantics into the same picture, proposing the session calculus as a programming language forstrategies, and strategies as a very accurate model of the session calculus. We implement a prototype whichcomputes the interpretation of session processes as synchronous strategies.
Franco J, Hagelin M, Wrigstad T, et al., 2017, You can have it all: Abstraction and good cache performance, 2017 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, co-located with SPLASH 2017, Publisher: ACM, Pages: 148-167
On current architectures, the optimisation of an application's performance often involves data being stored according to access affinity - what is accessed together should be stored together, rather than logical affinity - what belongs together logically stays together. Such low level techniques lead to faster, but more error prone code, and end up tangling the program's logic with low-level data layout details. Our vision, which we call SHAPES - Safe, High-level, Abstractions for oPtimisation of mEmory cacheS - is that the layout of a data structure should be defined only once, upon instantiation, and the remainder of the code should be layout agnostic. This enables performance improvements while also guaranteeing memory safety, and supports the separation of program logic from low level concerns. In this paper we investigate how this vision can be supported by extending a programming language. We describe the core language features supporting this vision: classes can be customized to support different layouts, and layout information is carried around in types; the remaining source code is layout-unaware and the compiler emits layout-aware code. We then discuss our SHAPES implementation through a prototype library, which we also used for preliminary evaluations. Finally, we discuss how the core could be expanded so as to deliver SHAPES's full potential: the incorporation of compacting garbage collection, ad hoc polymorphism and late binding, synchronization of representations of different collections, support for dynamic change of representation, etc.
Clebsch S, Franco J, Drossopoulou S, et al., 2017, Orca: GC and type system co-design for actor languages, OOPSLA 2017, Publisher: Association for Computing Machinery, Pages: 72:1-72:28, ISSN: 2475-1421
ORCA is a concurrent and parallel garbage collector for actor programs,which does not require any stop-the-world steps, or synchronisationmechanisms, and which has been designed to support zero-copy message passing and sharing of mutable data. \ORCA is part of the runtime of the actor-based language Pony. Pony's runtime was co-designed with the Pony language. This co-design allowed us to exploit certain language properties in order to optimise performance of garbage collection. Namely, ORCA relies on the absence of race conditions in order to avoid read/write barriers, and itleverages actor message passing for synchronisation among actors. Thispaper describes Pony, its type system, and the ORCA garbage collection algorithm.An evaluation of the performance of ORCA suggests that it is fast and scalable for idiomatic workloads.
Orchard D, Yoshida N, 2017, Special Issue: PLACES 2016 foreword, JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, Vol: 90, Pages: 1-1, ISSN: 2352-2208
Chen T-C, Dezani-Ciancaglini M, Scalas A, et al., 2017, On the preciseness of subtyping in session types, Logical Methods in Computer Science, Vol: 13, ISSN: 1860-5974
Subtyping in concurrency has been extensively studied since early 1990s asone of the most interesting issues in type theory. The correctness of subtyping relations hasbeen usually provided as the soundness for type safety. The converse direction, the com-pleteness, has been largely ignored in spite of its usefulness to de ne the largest subtypingrelation ensuring type safety. This paper formalises preciseness (i.e. both soundness andcompleteness) of subtyping for mobile processes and studies it for the synchronous and theasynchronous session calculi. We rst prove that the well-known session subtyping, thebranching-selection subtyping, is sound and complete for the synchronous calculus. Nextwe show that in the asynchronous calculus, this subtyping is incomplete for type-safety:that is, there exist session typesTandSsuch thatTcan safely be considered as a subtypeofS, butT6Sis not derivable by the subtyping. We then propose an asynchronous sub-typing system which is sound and complete for the asynchronous calculus. The methodgives a general guidance to design rigorous channel-based subtypings respecting desiredsafety properties. Both the synchronous and the asynchronous calculus are rst consid-ered with linear channels only, and then they are extended with session initialisations andcommunications of expressions (including shared channels).
Yoshida N, Neykova R, 2017, How to Verify Your Python Conversations, Behavioural Types: from Theory to Tools, Editors: Gay, Ravara
Lange J, Tuosto E, Yoshida N, 2017, A Tool for Choreography-Based Analysis of Message-Passing Software, Behavioural Types: from Theory to Tools
Ng CWN, Yoshida N, 2017, Protocol-Driven MPI Program Generation, Behavioural Types: from Theory to Tools
Vasconcelos VT, Martins F, Marques ERB, et al., 2017, Deductive Verification of MPI Protocols, Behavioural Types: from Theory to Tools
Orchard D, Yoshida N, 2017, Session Types with Linearity in Haskell, Behavioural Types: from Theory to Tools
Imai K, Yoshida N, Yuen S, 2017, Session-ocaml: a session-based library with polarities and lenses, 19th International Conference on Coordination Models and Languages, Publisher: Springer, Pages: 99-118, ISSN: 0302-9743
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 and delegations. We show applications of session-ocaml including a travel agency usecase and an SMTP protocol.
Neykova R, Yoshida N, 2017, Let it recover: multiparty protocol-induced recovery, International Conference on Compiler Construction, Publisher: ACM, Pages: 98-108
Fault-tolerant communication systems rely on recovery strategieswhich are often error-prone (e.g. a programmer manually specifiesrecovery strategies) or inefficient (e.g. the whole system is restartedfrom the beginning). This paper proposes a static analysis based onmultiparty session types that can efficiently compute a safe globalstate from which a system of interacting processes should be recov-ered. We statically analyse the communication flow of a program,given as a multiparty protocol, to extract the causal dependenciesbetween processes and to localise failures. We formalise our re-covery algorithm and prove its safety. A recovered communicationsystem is free from deadlocks, orphan messages and reception er-rors. Our recovery algorithm incurs less communication cost (onlyaffected processes are notified) and overall execution time (onlyrequired states are repeated). On top of our analysis, we designand implement a runtime framework in Erlang where failed pro-cesses and their dependencies are soundly restarted from a com-puted safe state. We evaluate our recovery framework on message-passing benchmarks and a use case for crawling webpages. Theexperimental results indicate our framework outperforms a built-instatic recovery strategy in Erlang when a part of the protocol canbe safely recovered.
Scalas A, Dardha O, Hu R, et al., 2017, A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming, 31st European Conference on Object-Oriented Programming (ECOOP 2017)
Graversen E, Phillips ICC, Yoshida N, 2017, Towards a categorical representation of reversible event structures, 10th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES 2017), Publisher: Open Publishing Association, Pages: 49-60, ISSN: 2075-2180
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 formsof event structures, including prime event structures, asymmetric event structures, and general eventstructures. More recently, reversible forms of these types of event structures have been defined.We formulate corresponding categories and functors between them. We show that products and co-products exist in many cases. In most work on reversible computing, including reversible processcalculi, a cause-respecting condition is posited, meaning that the cause of an event may not be re-versed before the event itself. Since reversible event structures are not assumed to be cause-respectingin general, we also define cause-respecting subcategories of these event structures. Our longer-termaim is to formulate event structure semantics for reversible process calculi.
Scalas A, Yoshida N, 2017, Multiparty session types, beyond duality (Abstract), 10th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, Publisher: Open Publishing Association, Pages: 37-38, ISSN: 2075-2180
Multiparty Session Types (MPST) are a well-established typing discipline for message-passing processes interacting on sessions involving two or more participants. Session typing can ensure desirable properties: absence of communication errors and deadlocks, and protocol conformance. However, existing MPST works provide a subject reduction result that is arguably (and sometimes, surprisingly) restrictive: it only holds for typing contexts with strong duality constraints on the interactions between pairs of participants. Consequently, many "intuitively correct" examples cannot be typed and/or cannot be proved type-safe. We illustrate some of these examples, and discuss the reason for these limitations. Then, we outline a novel MPST typing system that removes these restrictions.
Neykova R, Yoshida N, 2017, Multiparty session actors, Logical Methods in Computer Science, Vol: 13, ISSN: 1860-5974
Actor coordination armoured with a suitable protocol description language has beena pressing problem in the actors community. We study the applicability of multiparty session type(MPST) protocols for verification of actor programs. We incorporate sessions to actors by introduc-ing minimum additions to the model such as the notion of actor roles and protocol mailboxes. Theframework uses Scribble, which is a protocol description language based on multiparty session types.Our programming model supports actor-like syntax and runtime verification mechanism guarantee-ing communication safety of the participating entities. An actor can implement multiple roles in asimilar way as an object can implement multiple interfaces. Multiple roles allow for cooperativeinter-concurrency in a single actor. We demonstrate our framework by designing and implement-ing a session actor library in Python and its runtime verification mechanism. Benchmark resultsdemonstrate that the runtime checks induce negligible overhead. We evaluate the applicability of ourverification framework to specify actor interactions by implementing twelve examples from an actorbenchmark suit.
Hu R, Yoshida N, 2017, Explicit connection actions in multiparty session types, 20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017), Publisher: Springer, Pages: 116-133, ISSN: 0302-9743
This work extends asynchronous multiparty session types(MPST) withexplicit connection actionsto support protocols with op-tional and dynamic participants. The actions by which endpoints areconnected and disconnected are a key element of real-world protocolsthat is not treated in existing MPST works. In addition, the use casesmotivating explicit connections often require a more relaxed form of mul-tiparty choice: these extensions do not satisfy the conservative restric-tions used to ensure safety in standard syntactic MPST. Instead, we de-velop a modelling-based approach to validate MPST safety and progressfor these enriched protocols. We present a toolchain implementation, fordistributed programming based on our extended MPST in Java, and acore formalism, demonstrating the soundness of our approach. We discusskey implementation issues related to the proposed extensions: a practi-cal treatment of choice subtyping for MPST progress, and multipartycorrelation of dynamic binary connections.
Lange J, Yoshida N, 2017, On the undecidability of asynchronous session subtyping, 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Publisher: Springer Verlag, Pages: 441-457, ISSN: 0302-9743
Asynchronous session subtyping has been studied extensivelyin [9, 10, 28–31] and applied in [23, 32, 33, 35]. An open question waswhether this subtyping relation is decidable. This paper settles the ques-tion in the negative. To prove this result, we first introduce a new sub-class of two-party communicating finite-state machines (CFSMs), calledasynchronous duplex (ADs), which we show to be Turing complete. Sec-ondly, we give a compatibility relation over CFSMs, which is sound andcomplete wrt. safety for ADs, and is equivalent to the asynchronoussubtyping. Then we show that the halting problem reduces to check-ing whether two CFSMs are in the relation. In addition, we show thecompatibility relation to be decidable for three sub-classes of ADs.
Bocchi L, Chen T-C, Demangeon R, et al., 2017, Monitoring networks through multiparty session types, Theoretical Computer Science, Vol: 669, Pages: 33-58, ISSN: 0304-3975
In large-scale distributed infrastructures, applications are realised through com-munications among distributed components. The need for methods for assuringsafe interactions in such environments is recognised, however the existing frame-works, relying on centralised verification or restricted specification methods, havelimited applicability. This paper proposes a new theory ofmonitoredπ-calculuswith dynamic usage ofmultiparty session types(MPST), offering a rigorous foun-dation for safety assurance of distributed components which asynchronously com-municate through multiparty sessions. Our theory establishes a framework forsemantically precise decentralised run-time enforcement and provides reasoningprinciples over monitored distributed applications, which complement existingstatic analysis techniques. We introduce asynchrony through the means of explicitrouters and global queues, and propose novel equivalences between networks, thatcapture the notion of interface equivalence, i.e. equating networks offering thesame services to a user. We illustrate our static-dynamic analysis system with anATM protocol as a running example and justify our theory with results: satisfac-tion equivalence, local/global safety and transparency, and session fidelity.
Neykova R, Bocchi L, Yoshida N, 2017, Timed runtime monitoring for multiparty conversation, Formal Aspects of Computing, Vol: 29, Pages: 877-910, ISSN: 1433-299X
We propose a dynamic verification framework for protocols in real-time distributed systems. The frame-work is based on Scribble, a tool-chain for design and verification of choreographies based on multiparty sessiontypes, which we have developed with our industrial partners. Drawing from recent work on multiparty session typesfor real-time interactions, we extend Scribble with clocks, resets, and clock predicates in order to constrain the timesin which interactions occur. We present a timed API for Python to program distributed implementations of Scribblespecifications. A dynamic verification framework ensures the safe execution of applications written with our timedAPI: we have implemented dedicated runtime monitors that check that each interaction occurs at a correct timingwith respect to the corresponding Scribble specification. To demonstrate the practicality of the proposed framework,we express and verify four categories of widely used temporal patterns from use cases in literature. We analyse theperformance of our implementation via benchmarking and show negligible overhead.
Lange J, Ng C, Parente Coutinho Fernandes Toninho B, et al., 2017, Fencing off go: liveness and safety for channel-based programming, POPL 2017, Publisher: ACM, Pages: 748-761
Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can only detect global deadlocks at runtime, but provides no compile-time protection against all too common communication mis-matches or partial deadlocks. This work develops a static verification framework for liveness and safety in Go programs, able to detect communication errors and partial deadlocks in a general class of realistic concurrent programs, including those with dynamic channel creation, unbounded thread creation and recursion. Our approach infers from a Go program a faithful representation of its communication patterns as a behavioural type. By checking a syntactic restriction on channel usage, dubbed fencing, we ensure that programs are made up of finitely many different communication patterns that may be repeated infinitely many times. This restriction allows us to implement a decision procedure for liveness and safety in types which in turn statically ensures liveness and safety in Go programs. We have implemented a type inference and decision procedures in a tool-chain and tested it against publicly available Go programs.
Imai K, Yoshida N, Yuen S, 2017, Session-ocaml: a session-based library with polarities and lenses, Departmental Technical Report: 17/8, Publisher: Department of Computing, Imperial College London, 17/8
We propose session-ocaml, a novel library for session-typedconcurrent/distributed programming in OCaml. Our technique solelyrelies on parametric polymorphism, which can encode core session typestructures with strong static guarantees. Our key ideas are: ( ) polarisedsession types, which give an alternative formulation of duality enablingOCaml to automatically infer an appropriate session type in a sessionwith a reasonable notational overhead; and ( ) a parameterised monadwith a data structure called ‘slots’ manipulated with lenses, which canstatically enforce session linearity and delegations. We show applicationsof session-ocaml including a travel agency usecase and an SMTP protocol.
Lange J, Ng N, Toninho B, et al., 2017, Fencing off go: liveness and safety for channel-based programming, ACM SIGPLAN Notices, Vol: 52, Pages: 748-761, ISSN: 0362-1340
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.