A linear decomposition of multiparty sessions for safe distributed programming

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

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 π-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.

Original languageEnglish
Title of host publication31st European Conference on Object-Oriented Programming, ECOOP 2017
EditorsPeter Muller
Pages24:1-24:31
Volume74
ISBN (Electronic)9783959770354
DOIs
Publication statusPublished - 1 Jun 2017
Event31st European Conference on Object-Oriented Programming, ECOOP 2017 - Barcelona, Spain
Duration: 18 Jun 201723 Jun 2017

Conference

Conference31st European Conference on Object-Oriented Programming, ECOOP 2017
CountrySpain
CityBarcelona
Period18/06/1723/06/17

Fingerprint

Decomposition
Message passing
Application programming interfaces (API)
Acoustic waves
Network protocols
Communication

Bibliographical note

© 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.

Keywords

  • Concurrent programming
  • Process calculi
  • Scala
  • Session types

Cite this

Scalas, A., Dardha, O., Hu, R., & Yoshida, N. (2017). A linear decomposition of multiparty sessions for safe distributed programming. In P. Muller (Ed.), 31st European Conference on Object-Oriented Programming, ECOOP 2017 (Vol. 74, pp. 24:1-24:31) https://doi.org/10.4230/LIPIcs.ECOOP.2017.24
Scalas, Alceste ; Dardha, Ornela ; Hu, Raymond ; Yoshida, Nobuko. / A linear decomposition of multiparty sessions for safe distributed programming. 31st European Conference on Object-Oriented Programming, ECOOP 2017. editor / Peter Muller. Vol. 74 2017. pp. 24:1-24:31
@inproceedings{b354788cd60d43e29f6c35bb3a97dc65,
title = "A linear decomposition of multiparty sessions for safe distributed programming",
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 π-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.",
keywords = "Concurrent programming, Process calculi, Scala, Session types",
author = "Alceste Scalas and Ornela Dardha and Raymond Hu and Nobuko Yoshida",
note = "{\circledC} 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.",
year = "2017",
month = "6",
day = "1",
doi = "10.4230/LIPIcs.ECOOP.2017.24",
language = "English",
volume = "74",
pages = "24:1--24:31",
editor = "Peter Muller",
booktitle = "31st European Conference on Object-Oriented Programming, ECOOP 2017",

}

Scalas, A, Dardha, O, Hu, R & Yoshida, N 2017, A linear decomposition of multiparty sessions for safe distributed programming. in P Muller (ed.), 31st European Conference on Object-Oriented Programming, ECOOP 2017. vol. 74, pp. 24:1-24:31, 31st European Conference on Object-Oriented Programming, ECOOP 2017, Barcelona, Spain, 18/06/17. https://doi.org/10.4230/LIPIcs.ECOOP.2017.24

A linear decomposition of multiparty sessions for safe distributed programming. / Scalas, Alceste; Dardha, Ornela; Hu, Raymond; Yoshida, Nobuko.

31st European Conference on Object-Oriented Programming, ECOOP 2017. ed. / Peter Muller. Vol. 74 2017. p. 24:1-24:31.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - A linear decomposition of multiparty sessions for safe distributed programming

AU - Scalas, Alceste

AU - Dardha, Ornela

AU - Hu, Raymond

AU - Yoshida, Nobuko

N1 - © 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.

PY - 2017/6/1

Y1 - 2017/6/1

N2 - 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.

AB - 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.

KW - Concurrent programming

KW - Process calculi

KW - Scala

KW - Session types

UR - http://www.scopus.com/inward/record.url?scp=85037809001&partnerID=8YFLogxK

UR - http://drops.dagstuhl.de/opus/volltexte/2017/7263/

UR - http://dx.doi.org/10.4230/DARTS.3.2.3

U2 - 10.4230/LIPIcs.ECOOP.2017.24

DO - 10.4230/LIPIcs.ECOOP.2017.24

M3 - Conference contribution

AN - SCOPUS:85037809001

VL - 74

SP - 24:1-24:31

BT - 31st European Conference on Object-Oriented Programming, ECOOP 2017

A2 - Muller, Peter

ER -

Scalas A, Dardha O, Hu R, Yoshida N. A linear decomposition of multiparty sessions for safe distributed programming. In Muller P, editor, 31st European Conference on Object-Oriented Programming, ECOOP 2017. Vol. 74. 2017. p. 24:1-24:31 https://doi.org/10.4230/LIPIcs.ECOOP.2017.24