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.

翻译：多参与方会话类型（MPST）是面向通信密集型系统的一种类型规约，可保障通信安全性、无死锁特性及协议合规性。现有多种研究工作通过建模失效场景引入容错机制，然而此类方法往往基于底层网络假设（例如基于TCP的通信能保证消息可靠投递），或采用集中式可靠节点及特定化可靠性定义，或仅针对单一失效类型（如节点崩溃失效）。本文提出MAG$π$——一种多参与方、异步且广义化的π演算，这是首个统一实现以下特性的语言与类型系统：（i）覆盖最广泛非拜占庭故障类型，包括消息丢失、消息延迟与乱序、节点崩溃故障、链路故障及网络分区；（ii）从协议中每个参与方视角出发，提出新颖且最具普适性的可靠性概念；（iii）涵盖从最低级基于UDP的网络编程到基于TCP的应用层这一完整网络假设光谱。我们证明了主题归约性与会话保真性、进程属性（无死锁性、可终止性等）、失效处理安全性及可靠性遵从性。