Asynchronous Multiparty Sessions with Mixed Choice

TL;DR

This paper introduces an asynchronous calculus for multiparty sessions with mixed choice, extending existing frameworks to support nondeterministic communication with proven safety properties.

Contribution

It develops a novel type system based on global types and coherence, orthogonal to projection-based methods, ensuring session safety and expressiveness for asynchronous protocols.

Findings

Proves Subject Reduction and Session Fidelity for typable sessions.

Shows that typable sessions are Lock-Free and Orphan-Message-Free.

Demonstrates the expressiveness of mixed choice in asynchronous protocols.

Abstract

We present an asynchronous calculus for multiparty sessions with mixed choice, which extends the Simple MultiParty Session framework in order to support nondeterministic choices with both input and output prefixes. Global types -- equipped with a coinductively defined labelled transition system -- form the basis of a type system that exploits the key notion of coherence of communication label sets. Roughly, a coherent set contains either all the communications enabled in the session, or all the actions currently exhibited by a participant, provided that at least one input is enabled for each expected sender. Our approach to the typing of multiparty sessions is orthogonal to the well-established, projection-based approaches of the MultiParty Session Type framework. We prove fundamental theorems for typable multiparty sessions, including Subject Reduction and Session Fidelity. These properties imply that typable sessions are both Lock-Free and Orphan-Message-Free. We also investigate the Eventual Reception property for an extension of the type system. Some examples demonstrate the expressiveness of mixed choice in asynchronous multiparty protocols and the effectiveness of the proposed type discipline.