Formal Specification and Safety Proof of a Leaderless Concurrent Atomic Broadcast Algorithm

TL;DR

This paper provides a formal specification and safety proof for the AllConcur algorithm, a decentralized atomic broadcast protocol that improves scalability and fault tolerance in distributed agreement systems.

Contribution

It offers the first formal specification and safety proof for AllConcur, enhancing understanding and reliability of decentralized agreement protocols.

Findings

Formal specification of AllConcur introduced.

Safety property of AllConcur formally proven.

Supports safe and scalable distributed agreement.

Abstract

Agreement plays a central role in distributed systems working on a common task. The increasing size of modern distributed systems makes them more susceptible to single component failures. Fault-tolerant distributed agreement protocols rely for the most part on leader-based atomic broadcast algorithms, such as Paxos. Such protocols are mostly used for data replication, which requires only a small number of servers to reach agreement. Yet, their centralized nature makes them ill-suited for distributed agreement at large scales. The recently introduced atomic broadcast algorithm AllConcur enables high throughput for distributed agreement while being completely decentralized. In this paper, we extend the work on AllConcur in two ways. First, we provide a formal specification of AllConcur that enables a better understanding of the algorithm. Second, we formally prove AllConcur's safety property on the basis of this specification. Therefore, our work not only ensures operators safe usage of AllConcur, but also facilitates the further improvement of distributed agreement protocols based on AllConcur.