Mailbox Types for Unordered Interactions
De' Liguoro, Ugo, Luca Padovani · Institutional Research Information System University of Turin (University of Turin) · 2018
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 π-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. 2012