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.

翻译：会话类型是通信协议的形式化规范，通过类型检查可实现协议实现的验证。迄今为止，会话类型理论体系均假设通信媒介是可靠的，不存在消息丢失。然而，不可靠广播通信在众多分布式系统（如自组织网络和无线传感器网络）中普遍存在。这类系统通常具有结构化的通信模式，本应适合通过会话类型进行分析，但必要的理论框架此前尚未建立。本文提出不可靠广播会话演算——一种支持不可靠广播通信的进程演算，并为其配备了经证明具备可靠性的会话类型系统。我们刻画了广播与收集这两种常见操作，它们分别对应对偶的会话类型。消息丢失可能导致会话端点失步。为进一步处理不可靠性，我们设计了无需会话参与者确认的自主恢复机制。我们的类型系统能确保会话内同步端点间的可靠性、安全性及进展性。通过实现Paxos——不可靠异步网络中达成共识的经典协议，我们展示了该框架的表达能力。