A linear decomposition of multiparty sessions for safe distributed programming


Multiparty Session Types (MPST) is a typing discipline for message-passing distributed processes that can ensure properties such as absence of communication errors and deadlocks, and protocol conformance. Can MPST provide a theoretical foundation for concurrent and distributed programming in "mainstream" languages? We address this problem by (1) developing the first encoding of a full-fledged multiparty session π-calculus into linear π-calculus, and(2) using the encoding as the foundation of a practical toolchain for safe multiparty programming in Scala. Our encoding is type-preserving and operationally sound and complete. Crucially, it keeps the distributed choreographic nature of MPST, illuminating that the safety properties of multiparty sessions can be precisely represented with a decomposition into binary linear channels. Previous works have only studied the relation between (limited) multiparty and binary sessions via centralised orchestration means. We exploit these results to implement an automated generation of Scala APIs for multiparty sessions, abstracting existing libraries for binary communication channels. This allows multiparty systems to be safely implemented over binary message transports, as commonly found in practice. Our implementation is the first to support distributed multiparty delegation: Our encoding yields it for free, via existing mechanisms for binary delegation.

Publication DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2017.24
Divisions: College of Engineering & Physical Sciences > School of Informatics and Digital Engineering > Computer Science
College of Engineering & Physical Sciences
Additional Information: © Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida; licensed under Creative Commons License CC-BY Funding: Partially supported by EPSRC (grants EP/K034413/1, EP/K011715/1, EP/L00058X/1, EP/N027833/1, EP/N028201/1) and EU (FP7 612985 “Upscale”). Dardha was awarded a SICSA PECE bursary for visiting Imperial College London in January–March 2016.
Event Title: 31st European Conference on Object-Oriented Programming, ECOOP 2017
Event Type: Other
Event Dates: 2017-06-18 - 2017-06-23
Uncontrolled Keywords: Concurrent programming,Process calculi,Scala,Session types,Software
ISBN: 9783959770354
Full Text Link:
Related URLs: http://www.scop ... tnerID=8YFLogxK (Scopus URL)
http://drops.da ... exte/2017/7263/ (Publisher URL)
PURE Output Type: Conference contribution
Published Date: 2017-06-01
Accepted Date: 2017-01-01
Authors: Scalas, Alceste (ORCID Profile 0000-0002-1153-6164)
Dardha, Ornela
Hu, Raymond
Yoshida, Nobuko



Version: Published Version

License: Creative Commons Attribution

| Preview

Export / Share Citation


Additional statistics for this record