链路故障的会话类型（技术报告）
Session Types for Link Failures (Technical Report)
摘要：
我们努力使用会话类型技术来证明容错分布式算法的行为特性。会话类型被设计为抽象地捕获（甚至多方）通信协议的结构。会话类型的目标是分析和验证协议的行为属性。一个重要的属性是进步，即，没有（意外的）死锁。分布式算法通常类似于多方通信协议（的组合）。与通常研究会话类型的协议相反，它们通常被设计为应对系统故障。一个基本的行为属性是（成功）终止，尽管失败，但它往往是精心证明分布式算法。我们通过可选块扩展了多方会话类型（以及具有嵌套会话的多方会话类型），这些可选块覆盖了有限的链接和崩溃故障类。这使我们能够自动推导出在这些限制范围内的分布式算法的终止。为了说明我们的方法，我们证明终止的 * 旋转协调 * 共识算法的实施。
英文摘要：
We strive to use session type technology to prove behavioural properties of fault-tolerant distributed algorithms. Session types are designed to abstractly capture the structure of (even multi-party) communication protocols. The goal of session types is the analysis and verification of the protocols' behavioural properties. One important such property is progress, i.e., the absence of (unintended) deadlock. Distributed algorithms often resemble (compositions of) multi-party communication protocols. In contrast to protocols that are typically studied with session types, they are often designed to cope with system failures. An essential behavioural property is (successful) termination, despite failures, but it is often elaborate to prove for distributed algorithms. We extend multi-party session types (and multi-party session types with nested sessions) by optional blocks that cover a limited class of link and crash failures. This allows us to automatically derive termination of distributed algorithms that come within these limits. To illustrate our approach, we prove termination for an implementation of the *rotating coordinator* Consensus algorithm.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
