月度归档:2016年07月

Paxos算法证明

近来看了《从Paxos到zookeeper》一书,文中对于paxos的推导过程,一直看得迷迷糊糊,在网上找了《Paxos Made Simple》论文,才发现,《从Paxos到zookeeper》一书几乎就是对该文的直接翻译,然后又找了一些中文的博客之类的,始终是懂非懂,究其原因,《Paxos Made Simple》并非对于paxos算法的严谨证明,文中多次出现“value值被chosen之后”这种类似的描述,而在分布式系统中,是很难确定事件之间的先后顺序的,文中的推理过程避开了严格的事件先后顺序,所以总给人一种“好像是这样,又好像不太对的感觉”。

现在我们撇开不管如何推导出这个算法,只管如何证明这个算法是正确的即可,重述一下已知条件及目的:

一些名词定义:
Proposer:负责提出一个提案。
Acceptor:负责批准提案。
提案格式:[number,value]其中,number是提案的编号,value是想要被确定的值。
Value值:可以理解为提案的具体内容,如:A/B/C三人投票选班长,A/B/C共有三票,每人都有一个唯一的编号M0-M2,但是其Value值可以相同,例如A和B选B当班长,C选C当班长,这Value值便是B和C,对应的提案便是[M0,B],[M1,B],[M2,C]。
提案选定的条件:超过半数的Acceptor批准(accept)了这个提案。

算法描述:
Prepare阶段.
1.1 Proposer选择一个提案编号Mn ,然后向半数以上的Acceptors发送编号为 Mn 的prepare请求。
1.2 如果一个Acceptor收到一个编号为Mn 的prepare请求,且 Mn 大于它已经响应的所有prepare请求的编号,那么它就会保证不会再批准(accept)任何编号小于Mn 的提案,同时将它已经accept过的所有提案中编号最大且小于Mn的提案(如果存在的话)作为响应。
2. Accept阶段
2.1 如果Proposer收到来自半数以上的Acceptor对于它的prepare请求(编号为Mn )的响应,那么它就会发送一个针对编号为 Mn ,value值为Vn 的提案的accept请求给Acceptors,在这里 Vn 是收到的响应中编号最大的提案的值,如果响应中不包含提案,那么它就是任意值。
2.2 如果Acceptor收到一个针对编号Mn的提案的accept请求,只要它还未对编号大于Mn的prepare请求作出响应,它就可以通过这个提案。
一个Acceptor可以响应任何一个Prepare请求,但是Accept(批准)请求,必须满足上述条件。
一个请求(Prepare或Accept)必须半数以上Acceptor成功响应,才算成功。
目的:如果某个提案[M,V]被选定了,之后选定的提案Value值都和这个提案相同。

证明如下:
假设[M0,V0]是被选定的提案,比M0大且Prepare阶段成功的所有提案我们按照编号从小到达记录如下:

M0,M1,M2..........Mn

我们用P(M0)表示Acceptor对一个提案进行prepare,A(M0)表示Acceptor对一个提案进行accept,用Time表示时间。

由上面的算法描述我们可知,M0的Accept阶段和M1的Prepare阶段一定有交集,设这个交集中的一个Acceptor为h,则在h上面,有Time(A(M0))<Time(P(M1)),即是说h先对M0进行了accept,然后再对M1进行prepare,因为如果顺序倒过来的话,那么M0不可能accept成功。

所以,h对M1进行prepare的时候,h已经accept过M0这个提案,根据上面的算法,此时prepare的返回会带上accept过的编号最大且小于M1的提案,由于比M1小的编号只能是M0了,所以此时将提案M0返回了。

而对于提出M1提案的Proposer,它接收到的所有prepare返回中,编号最大的也只能是M0了,所以这个Proposer会使用M0提案的value值作为它的value值,所以M1提案的value值与M0相同。

依次类推,M2提案也是类似,会选择M1提案的value值作为其value值,所以结果时,比M0编号大,且Prepare成功的所有编号其value值都和M0相同,再由于一个提案只能先Prepare成功了,才能进行Accept阶段,才能被Acceptor所accept,所以后续所有accept的提案,其value都和M0相同。

而编号比M0小的提案,根据算法,也不可能accept成功,因为acceptor已经承诺过不accept编号小余M0的提案。

《Paxos Made Simple》一文中,对于Acceptor的prepare阶段做了一个优化,如下:

如果一个Acceptor收到一个编号为M的Prepare请求,且编号M大于之前响应过的所有Prepare请求的编号,则将它已经accept过的最大编号的提案返回,同时承诺不会再accept任何编号小余M的提案;否则,不响应该请求。

可以看到,此处做了两处优化:

  • 编号M小余prepare过的最大编号时,不返回。
  • 返回的是accept过的编号最大的提案,而不是“accept过的所有提案中编号最大且下于Mn的提案”。

优化1比较容易理解,因为Acceptor已经对编号大于M的提案prepare过了,所以它肯定不会accept任何编号为M的提案了,此时显然没有必要返回了。

优化2去掉了条件“且小于Mn的提案”,我们依旧可以按照上面的证明思路进行证明,如果M1在prepare的时候,返回的不是M0的提案,而是另外一个编号更大的提案,假设这个提案为Mk,对于Mk,依然有Time(A(M0))<Time(P(Mk)),此时Mk进行prepare的时候,也会返回一个提案,如果这个最大的提案不是M0,那么可以假设为Mj,而对于Mj我们又回到了刚才对于Mk的假设,这样不多假设之后,会将所有编号大于M0的提案全部遍历完,此时最大的提案只能是M0了,所以大于M0的提案的value值也只能跟M0的value值一样了。

到此为止,我们已经完成了证明。

参考资料:
1. 《从Paxos到Zookeeper分布式一致性原理与实践》
2. 《Paxos Made Simple》
3. https://www.zhihu.com/question/19787937/answer/82340987
4. http://blog.csdn.net/anderscloud/article/details/7175209
5. http://iunknown.iteye.com/blog/2246484?from=message&isappinstalled=0