A Session Type System for Asynchronous Unreliable Broadcast Communication

TL;DR

This work introduces UBSC, a formal framework for asynchronous unreliable broadcast communication with session types. It defines a shared calculus with asynchronous buffers, dual-session types, and autonomous recovery to guarantee soundness, safety, and progress despite loss and non-synchronisation. The type system uses endpoint synchronisation to re-align non-synchronised endpoints and proves preservation, safety, and progress, including recovery-by-design results. Expressiveness is demonstrated by implementing Paxos, showing that the framework can model complex distributed protocols under lossy, asynchronous conditions. The approach advances verification for ad-hoc and wireless networks by yielding static guarantees without requiring detailed failure specifications at the type level.

Abstract

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.

Figures (10)

• Figure 1: Syntax of Processes, Buffers, and Networks
• Figure 2: Structural Congruence for Processes, Buffers, and Networks
• Figure 3: Reduction rules for networks.
• Figure 4: Reduction rules for Broadcast and Gather Operations.
• Figure 5: Reduction rules for recovery.

Theorems & Definitions (41)

• Example 1.1: A simple Heartbeat Protocol
• Example 2.1: A Heartbeat Protocol
• Example 2.2: Dropping Connections
• Example 2.3: Recursive Interaction
• Definition 3.1: Session Type
• Definition 3.2: Type Duality
• Definition 3.3: Buffer Types
• Definition 3.4: Operator $\circ$
• Definition 3.5: Typing Context
• Example 3.6: Typing for Example \ref{['ex:recursive_interaction']}