License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2017.24
URN: urn:nbn:de:0030-drops-72637
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7263/
Go to the corresponding LIPIcs Volume Portal

Scalas, Alceste ; Dardha, Ornela ; Hu, Raymond ; Yoshida, Nobuko

A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming

pdf-format:
LIPIcs-ECOOP-2017-24.pdf (0.9 MB)

Abstract

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 pi-calculus into linear
pi-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.

BibTeX - Entry

@InProceedings{scalas_et_al:LIPIcs:2017:7263,
  author =	{Alceste Scalas and Ornela Dardha and Raymond Hu and Nobuko Yoshida},
  title =	{{A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{24:1--24:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{Peter M{\"u}ller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7263},
  URN =		{urn:nbn:de:0030-drops-72637},
  doi =		{10.4230/LIPIcs.ECOOP.2017.24},
  annote =	{Keywords: process calculi, session types, concurrent programming, Scala}
}

Keywords: process calculi, session types, concurrent programming, Scala
Collection: 31st European Conference on Object-Oriented Programming (ECOOP 2017)
Issue Date: 2017
Date of publication: 16.06.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI