一句话：提出带崩溃停止故障的异步多方会话类型理论，借助崩溃处理分支与全局语义，证明良类型进程在崩溃下仍保证无死锁与活性。
会话类型为消息传递系统提供类型规约，但既有理论通常假设系统完全可靠，难以刻画真实分布式系统中的进程崩溃。本文提出一种带崩溃停止故障的异步多方会话类型（MPST）理论：进程可任意崩溃并在崩溃后停止交互；类型与进程被扩展以包含崩溃处理分支，并将崩溃停止故障语义集成其中。该方法无需扩展用户级全局类型语法，同时形式化全局语义以捕捉崩溃及崩溃处理引发的复杂行为。通过可选可靠性假设，该理论覆盖从完全可靠到任意进程可崩溃的全部场景，并证明全局与局部类型语义的可靠完备对应，从而保证良类型进程在存在崩溃时仍满足无死锁、协议一致性与活性。
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.Comment: arXiv admin note: substantial text overlap with arXiv:2305.06238
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BarwellHYZ25,
title = {Crash-Stop Failures in Asynchronous Multiparty Session Types},
author = {Adam D. Barwell and Ping Hou and Nobuko Yoshida and Fangyi Zhou},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 2},
year = {2025},
doi = {10.46298/lmcs-21(2:5)2025}
}