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及其进程引入崩溃处理分支，将崩溃停止故障语义整合到类型与进程中。该方法无需对全局类型进行用户级语法扩展，并通过全局语义形式化建模，捕获由崩溃/崩溃处理进程引发的复杂行为。新理论覆盖从完全可靠的理想世界到任何进程可能崩溃的完全不可靠场景的全频谱，并引入可选可靠性假设。在这些假设下，我们证明了全局与局部类型语义之间的完备对应关系，即使存在崩溃，该关系也能通过构造保证良好类型进程的无死锁性、协议合规性及活性。