Less is More Revisited: Association with Global Protocols and Multiparty Sessions

TL;DR

This paper revisits multiparty session types (MPST), clarifies their soundness issues, and introduces a new proof technique ensuring type safety and behavioral properties in distributed communication protocols.

Contribution

It proposes a novel proof method for MPST type soundness based on an association relation, addressing previous concerns about end-point projection correctness.

Findings

New proof technique guarantees session fidelity, deadlock freedom, and liveness.

Clarifies the soundness of MPST end-point projection with mergeability.

Provides detailed comparison with existing MPST systems.

Abstract

Ensuring correctness of communication in distributed systems remains challenging. To address this, Multiparty session types (MPST), initially introduced by Honda et al. [52, 53], offer a type discipline in which a programmer or architect specifies an overall view of communication as a global protocol (global type), and each distributed program is locally type-checked against its end-point projection. In practice, the MPST framework has been integrated into over 25 programming languages or tools. Ten years after the emergence of MPST, Scalas and Yoshida [84] discovered that existing proofs of type safety using end-point projection with mergeability are flawed, where the mergeability operator enlarges the typability of MPST end-point programs, admits easy implementation, and is more efficient than alternative approaches, including model checking. Nevertheless, following the result in [84], the soundness of end-point projection (with mergeability) has been interpreted in the literature as problematic. We clarify this concern by proposing a new general proof technique for type soundness (subject reduction) of multiparty session $\pi$-calculus, which relies on an association relation between the behavioural semantics of a global type and its end-point projection. With this approach, behavioural properties, namely session fidelity, deadlock freedom, and liveness, are also guaranteed based on global types. Additionally, we provide detailed comparisons with existing MPST typing systems and discuss their respective proof methods for type soundness.