面向异步不可靠广播通信的会话类型系统
A Session Type System for Asynchronous Unreliable Broadcast Communication
AI总结：
本文提出不可靠广播会话演算及其会话类型系统，刻画广播与汇聚的对偶会话类型，并提供无需确认的自主恢复机制，通过实现Paxos协议验证了框架的表达能力。
摘要：
会话类型是通信协议的形式化规范，使得协议实现可以通过类型检查得到验证。迄今为止，会话类型理论都假设通信介质是可靠的，不存在消息丢失。然而，不可靠广播通信在自组织网络和无线传感器网络等一大类分布式系统中十分常见。这类系统往往具有结构化的通信模式，应当可以通过会话类型进行分析，但此前尚未发展出必要的理论。我们引入了不可靠广播会话演算（Unreliable Broadcast Session Calculus），这是一种具有不可靠广播通信的进程演算，并为其配备了一个会话类型系统，我们证明了该类型系统的可靠性。我们刻画了两种常见操作——广播（broadcast）和汇聚（gather），它们对应于对偶的会话类型。消息丢失可能导致会话端点不同步。为了进一步应对不可靠性，我们提供了一种自主恢复机制，该机制不需要会话参与者的确认。我们的类型系统保证了会话内同步端点之间的可靠性、安全性和进展性。我们通过实现Paxos——在不可靠异步网络中达成共识的教科书式协议——来展示该框架的表达能力。
英文摘要：
Session types are formal specifications of communication protocols, allowing protocol implementations to be verified by typechecking. Up to now, session type disciplines have assumed that the communication medium is reliable, with no loss of messages. However, unreliable broadcast communication is common in a wide class of distributed systems such as ad-hoc and wireless sensor networks. Often such systems have structured communication patterns that should be amenable to analysis by means of session types, but the necessary theory has not previously been developed. We introduce the Unreliable Broadcast Session Calculus, a process calculus with unreliable broadcast communication, and equip it with a session type system that we show is sound. We capture two common operations, broadcast and gather, inhabiting dual session types. Message loss may lead to non-synchronised session endpoints. To further account for unreliability we provide with an autonomous recovery mechanism that does not require acknowledgements from session participants. Our type system ensures soundness, safety, and progress between the synchronised endpoints within a session. We demonstrate the expressiveness of our framework by implementing Paxos, the textbook protocol for reaching consensus in an unreliable, asynchronous network.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
