Session types provide a typing discipline for message-passing systems. However, their theory often assumes an ideal world: one in which everything is reliable and without failures. Yet this is in stark contrast with distributed systems in the real world. To address this limitation, we introduce a new asynchronous multiparty session types (MPST) theory with crash-stop failures, where processes may crash arbitrarily and cease to interact after crashing. We augment asynchronous MPST and processes with crash handling branches, and integrate crash-stop failure semantics into types and processes. Our approach requires no user-level syntax extensions for global types, and features a formalisation of global semantics, which captures complex behaviours induced by crashed/crash handling processes. Our new theory covers the entire spectrum, ranging from the ideal world of total reliability to entirely unreliable scenarios where any process may crash, using optional reliability assumptions. Under these assumptions, we demonstrate the sound and complete correspondence between global and local type semantics, which guarantee deadlock-freedom, protocol conformance, and liveness of well-typed processes by construction, even in the presence of crashes.

翻译：会话类型为消息传递系统提供了一种类型化规约。然而，其理论通常假设理想世界：所有组件均可靠且无故障。但这与现实世界中的分布式系统形成鲜明对比。为克服这一局限，我们提出了一种具有崩溃停止故障的异步多参与者会话类型(MPST)新理论，其中进程可能任意崩溃，并在崩溃后停止交互。我们在异步MPST和进程中引入崩溃处理分支，并将崩溃停止故障语义整合至类型与进程中。本方法无需对全局类型进行用户级语法扩展，并通过形式化全局语义来刻画崩溃/崩溃处理进程引发的复杂行为。我们的新理论覆盖了从完全可靠的理想世界到任意进程可能崩溃的完全不可靠场景的完整谱系，支持可选可靠性假设。在这些假设下，我们证明了全局与局部类型语义之间的完备对应关系，该对应关系能确保良类型进程在构造时即具备无死锁性、协议合规性及活跃性——即使存在崩溃情形。