Separation and Encodability in Mixed Choice Multiparty Sessions (Technical Report)

TL;DR

This paper introduces a new type system for mixed choice multiparty session calculus, proving its safety and deadlock-freedom, and analyzes its expressiveness through encodability and separation results.

Contribution

It develops a general typing system for mixed choice sessions and provides the first comprehensive comparison of their expressiveness with classical MP.

Findings

MCMP is more expressive than classical MP.

Eight new encodability results are established.

Twenty new separation results are demonstrated.

Abstract

Multiparty session types (MP) are a type discipline for enforcing the structured, deadlock-free communication of concurrent and message-passing programs. Traditional MP have a limited form of choice in which alternative communication possibilities are offered by a single participant and selected by another. Mixed choice multiparty session types (MCMP) extend the choice construct to include both selections and offers in the same choice. This paper first proposes a general typing system for a mixed choice synchronous multiparty session calculus, and prove type soundness, communication safety, and deadlock-freedom. Next we compare expressiveness of nine subcalcli of MCMP-calculus by examining their encodability (there exists a good encoding from one to another) and separation (there exists no good encoding from one calculus to another). We prove 8 new encodablity results and 20 new separation results. In summary, MCMP is strictly more expressive than classical multiparty sessions (MP) and mixed choice in mixed sessions. This contrasts earlier results where mixed sessions do not add any expressiveness to non-mixed fundamental sessions, shedding a light on expressiveness of multiparty mixed choice.