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及进程，并将崩溃停止故障语义集成到类型与进程中。该方法无需对全局类型进行用户级语法扩展，并建立了全局语义的形式化体系，以捕捉由崩溃进程/崩溃处理进程引发的复杂行为。通过可选的可靠性假设，我们的新理论涵盖了从完全可靠的理想世界到任意进程可能崩溃的完全不可靠场景的完整谱系。在这些假设下，我们证明了全局与局部类型语义间具备可靠且完备的对应关系，该关系通过构造保证了良类型进程的无死锁性、协议一致性及活性，即使在存在崩溃的情况下依然成立。