序
Basic-Paxos是分布式一致性算法的元祖算法之一,现代的分布式一致性算法基本都是Basic-Paxos算法的优化、改进或简化。
由于过于晦涩难懂,Basic-Paxos也是最难理解的算法之一,然而有理由相信,直接从数学证明推导出Basic-Paxos算法是理解它最便捷的方法。
单提案表决:单轮投票一致性
定义1
设分布式节点总集合
,定义集合
,且
中任意两个成员的交集不为空,则称
为
的法定集(或称多数派)。
定义2
定义
为单轮投票的全部要素的集合,
为参加投票的法定集合的集合,
为本轮投票的编号,
为本轮提出的决议
约束α
轮投票中,每个节点只能支持一个提案
约束β
轮投票中,只有被法定集合
接受的提案才被确认为本轮决议
断言A
在同时满足约束α和约束β的情况下,一轮投票
中不可能同时有两个不同的提案被表决通过
断言A的证明(反证法)
假设法定集合
通过了提案
,法定集合
通过了提案
,且
,由于任意两个法定集合之间存在交集,那么必定存在节点
,且N同时支持提案
和
,这违反了约束α,因此断言A成立。
多提案带来的问题
约束α和约束β定义了单轮投票一致性约束,能够保证单轮投票产生唯一合法决议。但多个不同的提案需要多轮表决来决出唯一合法决议
多提案表决:多轮投票一致性
定义3
定义R的最大通过决议
表征在R轮投票之前通过的所有决议中比R轮编号小的编号最大的一轮
表决所通过的表决结果,如过它不存在则定义为
。
约束γ
在任一轮投票中,如果
,则设
可以任意选定;如果
,则设
断言B(弱一致性):
理想状态下(每轮投票按编号顺序产生并按序表决),在同时满足约束α、约束β和约束γ的情况下,则多轮投票后总能保证一致性
断言B的证明(反证法):
在理想状态下(每轮投票按编号顺序产生并按序表决),假设经过
轮投票后,存在新的一轮投票
,使得
,
如果
,则
为
任意自定义决议,根据约束γ,
,这将导出
,与假设矛盾。
如果
,则
,根据约束γ,
,这将导出
,仍与假设矛盾。
因此断言B得证。
时序导致的问题
多轮投票表决中,即使每轮投票按序产生,也不能保证最终形成决议的顺序与编号顺序一致(现实模型中的网络传输因素或系统设计因素),这将导致断言B导出的弱一致性不成立。
非理想状态下断言B的证伪:
在非理想状态下,假定存在以下表决序列
,如果
轮投票产生了决议
,根据约束γ,
。
但由于
的决议产生于
决议发生之前,此时并不存在
的表决结果
,于是
。
值此时被任意表决。
因此约束γ被破坏,断言B不成立。
多轮投票强一致性
约束δ
如果
轮投票之前,存在
轮投票,
轮投票已经产生了表决结果,且
轮投票的编号大于
,则
轮投票的任何决议都不被接受(
轮表决被放弃并无效化)
断言C(强一致性):
在同时满足约束α、约束β、约束γ和约束δ的情况下,多轮投票后总能保持决议一致性。
断言C的证明:
假设在非理想条件下,存在下列乱序表决
,根据约束δ,
与
的表决将被无效化,等效于将
与
从表决序列中丢弃,因此原表决序列化简为
于是被转换为理想状态下的多轮投票一致性问题,根据断言B,一致性成立,因此断言C成立。
两阶段原型导出
断言D
在支持多提案表决的一致性框架(强一致性和弱一致性)内,每一轮投票都必须遵循两阶段模型,其目的是:
第一阶段:
获取
的值
第二阶段:
得出本轮决议
断言D的证明:
根据约束γ和约束δ,断言D自动成立
Basic-Paxos算法的自然导出
首先定义角色Proposers和Acceptors。Proposers提出提案,提案信息包括提案编号和提议的value(提案的内容);Acceptor收到提案后可以接受(accept)提案,若提案获得多数Acceptors的接受,则称该提案被批准(chosen)。
两阶段协议表决:
Prepare阶段
- Proposer选择一个提案号n,向大于半数的Acceptor发送Prepare消息;
- 如果Acceptor还没有承若过不接受编号小于m(m>n)的提案,则承诺不再接受编号小于n的提案,并返回它已经接受的编号小于n的提案中编号最大的提案。
Accept阶段
- Proposer接受到所有Acceptor对Prepare请求的回应后,提出编号为n值为v的提案。值v是Acceptor接受到的所有编号小于n的提案中编号最大的提案的值。如果没有Acceptor接受过编号小于n的提案,则值v可由Proposer自己决定。提出提案后,向所有的Acceptor发送Accept消息,以期Acceptor接受提案。
- 如果Acceptor没有向其它的Prepare请求承诺过不再接受编号小于m(m>n)的提案,则接受编号为n的提案。