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.2018.15
URN: urn:nbn:de:0030-drops-92209
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9220/
Go to the corresponding LIPIcs Volume Portal

de'Liguoro, Ugo ; Padovani, Luca

Mailbox Types for Unordered Interactions

pdf-format:
LIPIcs-ECOOP-2018-15.pdf (0.6 MB)

Abstract

We propose a type system for reasoning on protocol conformance and deadlock freedom in networks of processes that communicate through unordered mailboxes. We model these networks in the mailbox calculus, a mild extension of the asynchronous pi-calculus with first-class mailboxes and selective input. The calculus subsumes the actor model and allows us to analyze networks with dynamic topologies and varying number of processes possibly mixing different concurrency abstractions. Well-typed processes are deadlock free and never fail because of unexpected messages. For a non-trivial class of them, junk freedom is also guaranteed. We illustrate the expressiveness of the calculus and of the type system by encoding instances of non-uniform, concurrent objects, binary sessions extended with joins and forks, and some known actor benchmarks.

BibTeX - Entry

@InProceedings{deliguoro_et_al:LIPIcs:2018:9220,
  author =	{Ugo de'Liguoro and Luca Padovani},
  title =	{{Mailbox Types for Unordered Interactions}},
  booktitle =	{32nd European Conference on Object-Oriented Programming  (ECOOP 2018)},
  pages =	{15:1--15:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Todd Millstein},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9220},
  URN =		{urn:nbn:de:0030-drops-92209},
  doi =		{10.4230/LIPIcs.ECOOP.2018.15},
  annote =	{Keywords: actors, concurrent objects, first-class mailboxes, unordered communication protocols, behavioral types, protocol conformance, deadlock freedom, junk f}
}

Keywords: actors, concurrent objects, first-class mailboxes, unordered communication protocols, behavioral types, protocol conformance, deadlock freedom, junk f
Collection: 32nd European Conference on Object-Oriented Programming (ECOOP 2018)
Issue Date: 2018
Date of publication: 10.07.2018

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