Brief Announcement: On the Significance of Consecutive Ballots in Paxos
| Autor: | Nuda Zhang, Manos Kapritsos, Eli Goldweber |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Correctness
Ballot Theoretical computer science State machine replication Matching (graph theory) Paxos Computer science ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION Liveness 0202 electrical engineering electronic engineering information engineering 020206 networking & telecommunications 02 engineering and technology Numbering |
| Zdroj: | PODC |
| DOI: | 10.1145/3382734.3405700 |
| Popis: | 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 weaken the learning criterion such that a learner does not need matching accept messages sent in the same ballot 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 Consecutive Paxos which encapsulates the properties of discrete consecutive ballots. To establish the correctness of these results, in addition to a paper proof, we formally verify the correctness of a State Machine Replication Library built on top of an optimized version of Multi-Paxos modified to reflect Consecutive Paxos. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|