MAG$\pi$: Types for Failure-Prone Communication

TL;DR

MAGπ introduces a novel type system for multiparty communication protocols that robustly handles a wide range of network failures and unreliable conditions, ensuring safety and reliability in diverse network scenarios.

Contribution

It is the first language and type system to unify handling of various non-Byzantine failures with a general notion of reliability across different network assumptions.

Findings

Proves subject reduction and session fidelity.

Establishes deadlock freedom and termination.

Ensures failure-handling safety and reliability adherence.

Abstract

Multiparty Session Types (MPST) are a typing discipline for communication-centric systems, guaranteeing communication safety, deadlock freedom and protocol compliance. Several works have emerged which model failures and introduce fault-tolerance techniques. However, such works often make assumptions on the underlying network, e.g., TCP-based communication where messages are guaranteed to be delivered; or adopt centralised reliable nodes and an ad-hoc notion of reliability; or only address a single kind of failure, such as node crash failures. In this work, we develop MAG$\pi$ -- a Multiparty, Asynchronous and Generalised $\pi$-calculus, which is the first language and type system to accommodate in unison: (i) the widest range of non-Byzantine faults, including message loss, delays and reordering; crash failures and link failures; and network partitioning; (ii) a novel and most general notion of reliability, taking into account the viewpoint of each participant in the protocol; (iii) a spectrum of network assumptions from the lowest UDP-based network programming to the TCP-based application level. We prove subject reduction and session fidelity; process properties (deadlock freedom, termination, etc.); failure-handling safety and reliability adherence.