License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2021.35
URN: urn:nbn:de:0030-drops-144125
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14412/
Go to the corresponding LIPIcs Volume Portal

Majumdar, Rupak ; Mukund, Madhavan ; Stutz, Felix ; Zufferey, Damien

Generalising Projection in Asynchronous Multiparty Session Types

pdf-format:
LIPIcs-CONCUR-2021-35.pdf (1 MB)

Abstract

Multiparty session types (MSTs) provide an efficient methodology for specifying and verifying message passing software systems. In the theory of MSTs, a global type specifies the interaction among the roles at the global level. A local specification for each role is generated by projecting from the global type on to the message exchanges it participates in. Whenever a global type can be projected on to each role, the composition of the projections is deadlock free and has exactly the behaviours specified by the global type. The key to the usability of MSTs is the projection operation: a more expressive projection allows more systems to be type-checked but requires a more difficult soundness argument.
In this paper, we generalise the standard projection operation in MSTs. This allows us to model and type-check many design patterns in distributed systems, such as load balancing, that are rejected by the standard projection. The key to the new projection is an analysis that tracks causality between messages. Our soundness proof uses novel graph-theoretic techniques from the theory of message-sequence charts. We demonstrate the efficacy of the new projection operation by showing many global types for common patterns that can be projected under our projection but not under the standard projection operation.

BibTeX - Entry

@InProceedings{majumdar_et_al:LIPIcs.CONCUR.2021.35,
  author =	{Majumdar, Rupak and Mukund, Madhavan and Stutz, Felix and Zufferey, Damien},
  title =	{{Generalising Projection in Asynchronous Multiparty Session Types}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{35:1--35:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14412},
  URN =		{urn:nbn:de:0030-drops-144125},
  doi =		{10.4230/LIPIcs.CONCUR.2021.35},
  annote =	{Keywords: Multiparty session types, Verification, Communicating state machines}
}

Keywords: Multiparty session types, Verification, Communicating state machines
Collection: 32nd International Conference on Concurrency Theory (CONCUR 2021)
Issue Date: 2021
Date of publication: 13.08.2021
Supplementary Material: Tool available at:
Software (Source Code): https://doi.org/10.5281/zenodo.5144684

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