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$\pi$ -- -- 一个多党、同步和通用的美元计算法,这是首个语言和类型系统,可以兼容:(一) 最广泛的非Byzantine断层,包括信息丢失、延误和重新排序;崩溃故障和连接故障;以及网络隔断;(二) 一种新颖和最普遍的可靠性概念,同时考虑到协议每个参与者的观点;(三) 从基于UDP的最底层网络编程到基于TCP的应用水平的网络假设,是一系列网络假设,这是第一个语言和类型系统:(一) 最广泛的非Byzantine断层断层断裂,包括信息丢失、故障、降低和保密性会议。