一句话：提出不可靠广播会话演算及其会话类型系统，保证同步端点间的健全性、安全性与进展，并支持无确认恢复。
论文针对分布式系统中广泛存在但此前会话类型理论未覆盖的不可靠广播通信，提出不可靠广播会话演算（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.
@article{paperbot2736,
title = {A Session Type System for Asynchronous Unreliable Broadcast Communication},
author = {Dimitrios Kouzapas and Ramunas Forsberg Gutkovas and A. Laura Voinea and Simon J. Gay},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 3},
year = {2024},
doi = {10.46298/lmcs-20(3:13)2024}
}