New framework enables asynchronous message passing with transient state inconsistencies in distributed systems

A team led by Laura Bocchi has unveiled a novel approach to managing communication in distributed systems, addressing a fundamental challenge in asynchronous multiparty protocols: how to handle situations where different participants are temporarily at different points in a conversation.

The Core Problem#

Building reliable distributed systems requires coordinating actions across multiple independent participants. Traditional multiparty session types (MSTs) enforce strict synchronization—all parties must be in lockstep about the current protocol state. However, in real-world asynchronous systems, messages travel at different speeds, creating inevitable delays and state mismatches. The new framework eases this constraint while maintaining correctness guarantees.

Mixed Choice Framework#

The researchers propose a construct called mixed choice that permits transient inconsistencies between participants' local views of the protocol. Rather than requiring everyone to agree on the state at every moment, the system ensures that all participants can eventually converge to a shared understanding. This approach mirrors how real messaging systems like RabbitMQ actually operate—where asynchrony is a fact of life, not an afterthought.

The team establishes formal correctness guarantees through two key properties: a progress property confirming that systems won't deadlock, and operational correspondence showing that global protocol specifications properly project down to individual participant behaviors.

Practical Implementation#

Beyond theory, the researchers built a working toolchain that lets developers write distributed protocol specifications and automatically generate compliant Erlang/OTP code. They validated the approach by specifying and reimplementing part of RabbitMQ's amqp_client library—a real, complex protocol used in production message brokers worldwide.

This work bridges the gap between formal verification methods and practical distributed systems engineering, offering developers both theoretical soundness and practical usability in building asynchronous protocols.