Publications
373 results found
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
Modern web applications can now offer desktop-like experiences from within the browser, thanksto technologies such as WebSockets, which enable low-latency duplex communication between thebrowser and the server. While these advances are great for the user experience, they represent anew responsibility for web developers who now need to manage and verify the correctness of morecomplex and potentially stateful interactions in their application.In this paper, we present a technique for developing interactive web applications that are stati-cally guaranteed to communicate following a given protocol. First, the global interaction protocol isdescribed in the Scribble protocol language – based on multiparty session types. Scribble protocolsare checked for well-formedness, and then each role is projected to a Finite State Machine represent-ing the structure of communication from the perspective of the role. We use source code generationand a novel type-level encoding of FSMs using multi-parameter type classes to leverage the typesystem of the target language and guarantee only programs that communicate following the protocolwill type check.Our work targets PureScript – a functional language that compiles to JavaScript – which cru-cially has an expressive enough type system to providestaticlinearity guarantees. We demonstratethe effectiveness of our approach through a web-based Battleship game where communication isperformed through WebSocket connections.
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.
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.
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, Pages: 150-168, 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 [6], 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−.
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
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.
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, Pages: 1-38, 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.
Scalas A, Yoshida N, 2019, Less is more: multiparty session types revisited, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Publisher: Association for Computing Machinery, Pages: 30:1-30:29, ISSN: 2475-1421
Multiparty Session Types (MPST) are a typing discipline ensuring that a message-passing process implements a 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 is necessary: classic MPST have a limited subject reduction property, with inherent restrictions that are easily overlooked, and in previous work have led to flawed type safety proofs; our new theory removes such restrictions and fixes such flaws. (2) We contribute a new MPST theory that is less complicated, and yet more general, 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 more protocols and processes. (3) We produce a detailed analysis of type-level properties, showing how, in our new theory, they allow to ensure decidability of type checking, and statically guarantee that processes enjoy, , deadlock-freedom and liveness at run-time. (4) We show how our new theory can integrate type and model checking: type-level properties can be expressed in modal µ-calculus, and verified with well-established tools.
Castellan S, Yoshida N, 2019, Two sides of the same coin: session types and game semantics, Proceedings of the ACM on Programming Languages, Vol: 3, ISSN: 2475-1421
Game semantics and session types are two formalisations of the same concept: message-passing open programs following certain protocols. Game semantics represents protocols as games, and programs as strategies; while session types specify protocols, and well-typed π-calculus processes model programs. Giving faithful models of the π-calculus and giving a precise description of strategies as a programming language are two difficult problems. In this paper, we show how these two problems can be tackled at the same time by building an accurate game semantics model of the session π-calculus.Our main contribution is to fill a semantic gap between the synchrony of the (session) π-calculus and the asynchrony of game semantics, by developing an event-structure based game semantics for synchronous concurrent computation. This model supports the first truly concurrent fully abstract (for barbed congruence) interpretation of the synchronous (session) π-calculus. We further strengthen this correspondence, establishing finite definability of asynchronous strategies by the internal session π-calculus. As an application of these results, we propose a faithful encoding of synchronous strategies into asynchronous strategies by call-return protocols, which induces automatically an encoding at the level of processes. Our results bring session types and game semantics into the same picture, proposing the session calculus as a programming language for strategies, and strategies as a very accurate model of the session calculus. We implement a prototype which computes the interpretation of session processes as synchronous strategies.
Castro-Perez D, Hu R, Jongmans S, et al., 2019, Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Publisher: Association for Computing Machinery, ISSN: 2475-1421
This paper presents a framework for the static specification and safe programming of message passing protocols where the number and kinds of participants are dynamically instantiated.We develop the first theory of distributed multiparty session types (MPST) to support parameterised protocols with indexed roles—our framework statically infers the different kinds of participants induced by a protocol definition as role variants, and produces decoupled endpoint projections of the protocol onto each variant. This enables safe MPST-based programming of the parameterised endpoints in distributed settings: 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 the correctness of projection.We implement our theory as a toolchain for programming such role-parametric MPST protocols in Go. Our approach is to generate API families of lightweight, protocol- and variant-specific type wrappers for I/O. The APIs ensure a well-typed Go endpoint program (by native Go type checking) will perform only compliant I/O actions w.r.t. the source protocol. We leverage the abstractions of MPST to support the specification and implementation of Go applications involving multiple channels, possibly over mixed transports (e.g., Go channels, TCP), and channel passing via a unified programming interface. We evaluate the applicability and run-time performance of our generated APIs using microbenchmarks and real-world applications.
Toninho B, Yoshida N, 2019, Polymorphic session pocesses as morphisms, Departmental Technical Report: 19/2, Publisher: Department of Computing, Imperial College London
The study of expressiveness of concurrent processes via session typesopens a connection between linear logic and mobile processes, grounded in therigorous logical background of propositions-as-types. One such study includes anotion of parametric session polymorphism, which connects session typed processeswith rich higher-order functional computations. This work proposes anovel and non-trivial application of session parametricity – an encoding of inductiveand coinductive session types, justified via the theory of initial algebrasand final co-algebras using a processes-as-morphisms viewpoint. The correctnessof the encoding (i.e. universality) relies crucially on parametricity and the associatedrelational lifting of sessions.
Castellan S, Stefanesco L, Yoshida N, 2019, Game semantics: easy as Pi, Departmental Technical Report: 19/3, Publisher: Department of Computing, Imperial College London
Game semantics has proven to be a robust method to give compositional semantics for a variety of higher-orderprogramming languages. However, due to the complexity of most game models, game semantics has remainedunapproachable for non-experts.In this paper, we aim at making game semantics more accessible by viewing it as a syntactic translationto a dialect of the π-calculus, referred to as metalanguage, followed by a semantic interpretation of themetalanguage into a particular game model. The semantic interpretation is done once and for all; while thesyntactic translation can be defined for a wide range of programming languages without knowledge of theparticular game model used. Reasoning on the interpretation (soundness and adequacy) can be done at thelevel of the metalanguage through a sound equational theory, escaping tedious technical proofs usually foundin game semantics. We call this methodology programming game semantics.We expose the methodology in three steps of increasing expressivity, building on concurrent game semanticsbased on event structures. By developing an extension of the existing models to deal with non-angelicnondeterminism, and nonlinear computation, we can give very accurate models of complex languages by asimple translation into a typed variant of the π-calculus inspired by Differential Linear Logic. We illustratethis expressivity on IPA, a higher-order programming language with shared-memory concurrency. By simplytranslating it into the metalanguage, we give the first model of IPA, which is (1) causal and (2) adequate forthe usual operational notion of bisimulation — a novel result.To make the development more concrete, we have built a simple prototype to compute the interpretation ofthe target programming language into the metalanguage and games strategies.
Scalas A, Yoshida N, Benussi E, 2019, Verifying message-passing programs with dependent behavioural types, Departmental Technical Report: 19/1, Publisher: Department of Computing, Imperial College London
Concurrent and distributed programming is notoriously hard.Modern languages and toolkits ease this difficulty by offeringmessage-passing abstractions, such as actors (e.g., Erlang,Akka, Orleans) or processes (e.g., Go): they allow for simplerreasoning w.r.t. shared-memory concurrency, but do notensure that a program implements a given specification.To address this challenge, it would be desirable to specifyand verify the intended behaviour of message-passing applicationsusing types, and ensure that, if a program type-checksand compiles, then it will run and communicate as desired.We develop this idea in theory and practice. We formalisea concurrent functional language λπ⩽, with a new blend ofbehavioural types (from π-calculus theory), and dependentfunction types (from the Dotty programming language, a.k.a.the future Scala 3). Our theory yields four main payoffs: (1) itverifies safety and liveness properties of programs via type–level model checking; (2) unlike previous work, it accuratelyverifies channel-passing (covering a typical pattern of actorprograms) and higher-order interaction (i.e., sending/receivingmobile code); (3) it is directly embedded in Dotty, as atoolkit called Effpi, offering a simplified actor-based API;(4) it enables an efficient runtime system for Effpi, for highlyconcurrent programs with millions of processes/actors.
Castro-Perez D, Ferreira Ruiz F, Yoshida N, 2019, EMTST engineering the meta-theory of session types, Departmental Technical Report: 19/4, Publisher: Department of Computing, Imperial College London
Session types provide a principled programming discipline for structured interactions. They are used tostatically check the safety of protocol composition and the absence of communication errors. These propertiesdepend upon the meta-theory of the typing discipline, usually a type safety proof. These proofs, whileconceptually simple, are very delicate and error prone due to the presence of linearity and name passing andhave been falsified in several works in the literature. In this work, we explore mechanised proofs in theoremassistants as tools to develop trustworthy proofs, and at the same time to guide extensions that do not violatetype safety. To that end, we study the meta-theory of two of the most used binary session types systems,the Honda-Vasconcelos-Kubo system and the more flexible revisited system by Yoshida and Vasconcelos.Additionally, we show the subtlety of representing the first system in α-equivalent representations.We developthese proofs in the Coq proof assistant, using a locally nameless representation for binders, and small scalereflection and overloaded lemmas to simplify the handling of linear typing environments.
Scalas A, Yoshida N, Benussi E, 2019, Verifying Message-Passing Programs with Dependent Behavioural Types, 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) part of ACM's Federated Computing Research Conference (FCRC), Publisher: ASSOC COMPUTING MACHINERY, Pages: 502-516
- Author Web Link
- Cite
- Citations: 14
Atzei N, Bartoletti M, Lande S, et al., 2019, Developing Secure Bitcoin Contracts with BitML, 27th ACM Joint Meeting on European Software Engineering Conference (ESEC) / Symposium on the Foundations of Software Engineering (FSE), Publisher: ASSOC COMPUTING MACHINERY, Pages: 1124-1128
- Author Web Link
- Cite
- Citations: 14
Toninho B, Yoshida N, 2019, Polymorphic Session Processes as Morphisms, ART OF MODELLING COMPUTATIONAL SYSTEMS: A JOURNEY FROM LOGIC AND CONCURRENCY TO SECURITY AND PRIVACY: ESSAYS DEDICATED TO CATUSCIA PALAMIDESSI ON THE OCCASION OF HER 60TH BIRTHDAY, Editors: Alvim, Chatzikokolakis, Olarte, Valencia, Publisher: SPRINGER INTERNATIONAL PUBLISHING AG, Pages: 101-117, ISBN: 978-3-030-31174-2
- Author Web Link
- Cite
- Citations: 5
Scalas A, Yoshida N, Benussi E, 2019, Effpi: Verified Message-Passing Programs in Dotty, 10th ACM SIGPLAN International Symposium on Scala (Scala), Publisher: ASSOC COMPUTING MACHINERY, Pages: 27-31
- Author Web Link
- Cite
- Citations: 4
Toninho B, Yoshida N, 2018, Interconnectability of session-based logical processes, ACM Transactions on Programming Languages and Systems, Vol: 40, ISSN: 0164-0925
In multiparty session types, interconnection networks identify which roles in a session engage in communica-tion (i.e. two roles are connected if they exchange a message). In session-based interpretations of linear logicthe analogue notion corresponds to determining which processes are composed, or cut, using compatible channels typed by linear propositions. In this work we show that well-formed interactions represented ina session-based interpretation of classical linear logic (CLL) form strictly less expressive interconnection networks than those of a multiparty session calculus. To achieve this result we introduce a new compositionalsynthesis property dubbed partial multiparty compatibility (PMC), enabling us to build a global type denoting the interactions obtained by iterated composition of well-typed CLL threads. We then show thatCLL composition induces PMC global types without circular interconnections between three (or more) participants. PMC is then used to define a new CLL composition rule which can form circular interconnections but preserves the deadlock-freedom of CLL.
Medic D, Mezzina CA, Phillips I, et al., 2018, A parametric framework for reversible π-calculi, Express/SOS 2018, Publisher: Open Publishing Association, Pages: 87-103, ISSN: 2075-2180
This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality in pi-calculus, which differ in the treatment of parallel extrusions of the same name. In this paper we present a uniform framework for reversible pi-calculi that is parametric with respect to a data structure that stores information about an 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 show that the (parametric) reversibility induced by our framework is causally-consistent and prove a causal correspondence between an appropriate instance of the framework and Boreale and Sangiorgi's causal semantics.
Graversen E, Phillips ICC, Yoshida N, 2018, Event structure semantics of (controlled) reversible CCS, Tenth International Conference on Reversible Computation, Publisher: Springer Verlag, ISSN: 0302-9743
CCSK is a reversible form of CCS which is causal, meaning that ac-tions can be reversed if and only if each action caused by them has already beenreversed; there is no control on whether or when a computation reverses. We pro-pose an event structure semantics for CCSK. For this purpose we define a cat-egory of reversible bundle event structures, and use the causal subcategory tomodel CCSK. We then modify CCSK to control the reversibility with a rollbackprimitive, which reverses a specific action and all actions caused by it. To definethe event structure semantics of rollback, we change our reversible bundle eventstructures by making the conflict relation asymmetric rather than symmetric, andwe exploit their capacity for non-causal reversibility.
Demangeon R, Yoshida N, 2018, Causal computational complexity of distributed processes, Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science, Publisher: ACM / IEEE, Pages: 344-353
his paper studies the complexity ofπ-calculus processes with res-pect to the quantity of transitions caused by an incoming message.First we propose a typing system for integrating Bellantoni andCook’s characterisation of polynomially-bound recursive functionsinto Deng and Sangiorgi’s typing system for termination. We thendefine computational complexity of distributed messages based onDegano and Priami’s causal semantics, which identifies the depen-dency between interleaved transitions. Next we apply a syntacticflow analysis to typable processes to ensure the computational boundof distributed messages. We prove that our analysis isdecidablefora given process;soundin the sense that it guarantees that the totalnumber of messages causally dependent of an input request receivedfrom the outside is bounded by a polynomial of the content of thisrequest; andcompletewhich means that each polynomial recursivefunction can be computed by a typable process.
Scalas A, Yoshida N, 2018, Multiparty session types, beyond duality, Journal of Logical and Algebraic Methods in Programming, Vol: 97, Pages: 55-84, ISSN: 2352-2208
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.We propose a novel MPST theory based on a rely/guarantee typing system, that checks (1) the guaranteed behaviour of the process being typed, and (2) the relied upon behaviour of other processes. Crucially, our theory achieves type safety by enforcing a typing context liveness invariant throughout typing derivations.Unlike “classic” MPST works, our typing system does not depend on global session types, and does not use syntactic duality checks. As a result, our new theory can prove type safety for processes that implement protocols with complex inter-role dependencies, thus sidestepping an intrinsic limitation of “classic” MPST.
Lange J, Ng CWN, Toninho B, et al., 2018, A static verification framework for message passing in go using behavioural types, ICSE 2018, Publisher: ACM, Pages: 1137-1148
The Go programming language has been heavily adopted in industry as a language that efficiently combines systems programming with concurrency. Go's concurrency primitives, inspired by process calculi such as CCS and CSP, feature channel-based communication and lightweight threads, providing a distinct means of structuring concurrent software. Despite its popularity, the Go programming ecosystem offers little to no support for guaranteeing the correctness of message-passing concurrent programs.This work proposes a practical verification framework for message passing concurrency in Go by developing a robust static analysis that infers an abstract model of a program's communication behaviour in the form of a behavioural type, a powerful process calculi typing discipline. We make use of our analysis to deploy a model and termination checking based verification of the inferred behavioural type that is suitable for a range of safety and liveness properties of Go programs, providing several improvements over existing approaches. We evaluate our framework and its implementation on publicly available real-world Go code.
Vicente Franco J, Clebsch S, Drossopoulou S, et al., 2018, Correctness of a concurrent object collector for actor languages, 27th European Symposium on Programming, Publisher: Springer
ORCAis a garbage collection protocol for actor-based pro-grams. Multiple actors may mutate the heap while the collector is run-ning without any dedicated synchronisation.ORCAis applicable to anyactor language whose type system prevents data races and which sup-ports causal message delivery. We present a model ofORCAwhich isparametric to the host language and its type system. We describe theinterplay between the host language and the collector. We give invariantspreserved byORCA, and prove its soundness and completeness.
Vicente Franco J, Clebsch S, Drossopoulou S, et al., 2018, Soundness of a concurrent collector for actors, 27th European Symposium on Programming (ESOP), Publisher: Springer, Pages: 885-911
ORCA is a fully concurrent garbage collection protocol foractor-based programs. Multiple actors may mutate the heap while thecollector is running without any dedicated synchronization. ORCA isapplicable to any actor language whose type system prevents data racesand which supports causal message delivery. We present a model ofORCA which is parametric to the host language and its type system. Wedescribe the interplay between the host language and the collector. Wegive eight invariants preserved by the protocol, and prove its soundnessand completeness.
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.