On the Significance of Consecutive Ballots in Paxos
Eli Goldweber, Nuda Zhang, and Manos Kapritsos

TL;DR
This paper introduces Consecutive Paxos, a variant of Paxos that leverages consecutive ballots to weaken learning conditions while maintaining safety and liveness guarantees, supported by formal verification.
Contribution
It defines Consecutive Quorums and proves that they preserve Paxos's safety and liveness, with formal verification of a State Machine Replication Library built on this approach.
Findings
Consecutive Quorums weaken the learning condition in Paxos.
Consecutive Paxos maintains safety and liveness guarantees.
Formal verification confirms the correctness of the modified protocol.
Abstract
In this paper we examine the Paxos protocol and demonstrate how the discrete numbering of ballots can be leveraged to weaken the conditions for learning. Specifically, we define the notion of consecutive ballots and use this to define Consecutive Quorums. Consecutive Quorums weakens the learning criterion such that a learner does not need matching messages sent in the from a majority of acceptors to learn a value. We prove that this modification preserves the original safety and liveness guarantees of Paxos. We define which encapsulates the properties of discrete consecutive ballots. To establish the correctness of these results, we, in addition to a paper proof, formally verify the correctness of a State Machine Replication Library built on top of an optimized version of Multi-Paxos modified to reflect .
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDistributed systems and fault tolerance · Cryptography and Data Security · Security and Verification in Computing
