Brief Announcement: On the Significance of Consecutive Ballots in Paxos
Brief Announcement: On the Significance of Consecutive Ballots in Paxos
复制标题
简短公告：关于Paxos连续投票的意义
DOI：
10.1145/3382734.3405700
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Kapritsos, Manos
中科院分区：
文献类型：
--
作者：
Goldweber, Eli;Zhang, Nuda;Kapritsos, Manos
在本文中，我们研究了Paxos协议，并演示了如何利用选票的离散编号来削弱学习条件。具体地说，我们定义了连续投票的概念，并使用它来定义连续的法定人数。连续的法定人数削弱了学习标准，因此学习者不需要匹配从大多数接受者发送的接受消息来学习一个值。我们证明了这种修改保留了Paxos原有的安全性和活性保证。我们定义了连续型Paxos，它封装了离散连续选票的性质。为了确定这些结果的正确性，除了纸质证明之外，我们还正式验证了状态机复制库的正确性，该状态机复制库构建在经修改以反映连续Paxos的优化版本的多Paxos之上。
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 matchingacceptmessages sent in thesame ballotfrom a majority of acceptors to learn a value. We prove that this modification preserves the original safety and liveness guarantees of Paxos. We defineConsecutive Paxoswhich 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 reflectConsecutive Paxos.