Paxos算法的一个容易理解的数学证明

Paxos算法的一个容易理解的数学证明

The Paxos algorithm, when presented in plain English, is very simple. 

--- inventor of paxos algorithm

    Leslie Lamport 在文献[1]中提出了解决分布式系统中一致性问题的paxos算法,在那里通过讲述古希腊的paxos议会达成一致投票来讲解算法的.后来在文献[2]又给出了一个简单的说明.

    本文对文献[2]中论说的算法给出了一个更加直观,适合工程技术人员阅读的数学证明.

1 算法要解决的问题

     假定有有限多个进程,可能提出一些"建议".所谓一致性算法就是要能够保证:在建议的不同的值之中,最终只能有一个被确定下来.

    每一个进程有以下三种可能的身份:建议者(proposer),接受者(acceptor),学习者(learner).每一个进程可能有不只一个身份.如果不之名是哪一个身份,就以agent泛指.

    建议者可以提出一个建议,即提议一个"值".接受者,可以建议者的建议,做出响应:接受或者拒绝(后面有详述).学习者最终能够知道确定的值是什么.

    进程之间可以进行网络通信.并做如下假定:

    1) 每一个agent进行某个"操作"(或说,对于任一个网络消息的响应)所需的时间可能是任意长,并且可能停止响应,然后重启程序.

     2) 每一个进程都有一些"非易失性"存储,即如硬盘,磁带等那样的在断电之后可以保存长久数据的存储设备.

    3) 网络消息的传送,可能需要任意长的时间,可能丢失,或者重复.但是消息并没有伪造,篡改的.(即没有所谓"拜占庭问题")

2 算法希望能到达的结果

    三个特性:

    2.1) 终止性. 每一个进程最终确定了一个值

    2.2) 同意性. 每一个进程确定的值是相同的

    2.3) 正确性  每一个所确定的值,是某个进程所"建议"的.即任一进程所确定的值,不是非法的.

    满足这三个条件的算法,足以在实践中使用.

3 paxos算法

    先对算法做一些说明,然后再叙述proposer的acceptor动作.算法希望经过proposer/acceptor的有限个动作以后,确定一个值.

    "确定一个值"意思是:有超过一半的acceptor都接受了同一个值.

    最后学习者在获知确定的结果.这部分不是本文的重点,不做详述.(在实践中,acceptor/proposer可以把确定的值通知给learner)

    建议者提交的每一个建议,都必须有一个"能排序的序号"(下文可能使用英文proposal number),对于不同的建议序号必须不一同.实现方法:1)建议者的序号,加时间做为二元组 .方法2:每一个建议者都确定一个编号(有限证书),它记录它已经发起的建议的个数,这个个数乘以建议者的个数再加上自己的序号.下面假定每一个建议的序号为自然数,并且递增.

    整个算法的运行过程是如下两个阶段的循环:

    阶段1.

        a) proposer选择一个"建议的序号"n,发送一个消息(称为prepare消息)给一定数量的acceptor.这个数量只要大于"acceptor的个数的一半".(注意是大于,不包括等于).

        b) acceptor收到proposer的prepare消息的时候,有两种可能.如果它以前收到过prepare消息,对比以前收到的prepare消息的"建议的序号"最大值, 跟收到的序号对比.

        如果收到的序号大于这个最大值,这个acceptor告诉proposer它已经收到的建议的值和序号(如果已经收到的话).否则不回应.

    阶段2.

        a) proposer的prepare消息收到的回应的个数,如果大于acceptor个数的一半,那么先判断是否已经"确定了一个值"(前面所说的:某这个值被超过半数的acceptor所接受).如果已经确定了一个值,那么一致性达到.否则, 它向这些(有回应的)acceptor发送accept请求:

        发送proposal number n 以及值v.其中的v这样确定:如果acceptor的回应中有若干个值(及其序号),那么选取最大序号的那个值;如果acceptor的回应没有值,那么这个proposer可以自己决定一个值.

    b) acceptor收到accept消息的反应有两种可能:

    如果此acceptor已经回应过的prepare消息的那个序号"大于"收到的建议的序号n,它就什么都不做.否则,接受并记录收到这个建议的序号,值v,以及这个proposer(这称作"承诺"机制).

    上述两阶段中,proposer可以随时主动放弃一个"建议",或者重新启动一个新的建议.

    那么proposer怎么知道,算法已经完成呢?方法之一是:proposer已经在阶段1中已经知道一致性协议已经达成以后,向每一个acceptor发送"询问"的消息.如果所有的有回应的acceptor的建议的值都一样(有个别acceptor可能已经崩溃,正在重启中,从而没有回应),那就认为算法已经结束.

    关于阶段1中的一致性已经达成,要做说明如下:如果再有一个proposer发送走过了阶段1,那么接收它的prepare消息的acceptor一定有一个是先前已经达成一致性协议中的某一个acceptor,所以此时,这个proposer一定会收到达成一致性的那个prpopsal 及其序号.在第二阶段中,只要使用这个proposal及其序号即可. 因为阶段1中,只要有过半的acceptor都一致即可认为是一致性已经达成(也正是因此,paxos算法可以在"少于一半"的acceptor停止工作的情况下,仍然可以正常运行).   

    考虑一个极端的情况.有一个proposer a,向编号为1,2,3,….m的m个acceptor发送了prepare消息,…成功走完第一阶段,正准备发送acceptor消息.这时,有另一个proposer b,想向1,2,…m这m个acceptor发送了prepare消息,走完第一个阶段.这时候,a再继续发送accept消息.根据上面来"两阶段"的描述,a向1,2,…m中的任一个提交的值,都无法成功.类似地,a可能导致b永远也无法导致某个值设置到1,2,..m上.

    这种极端情况如果有"无限次"出现的话,那就永远无法达成一致了.引入一个"时间窗口"的机制:算法开始之前,选定一个足够的值t表示时间.每一个acceptor收到prepare消息以后的t之内,不再收任何prepare消息.所以假定上面的极端情况不再发生.或者说有如下结论成立:

    (假设)当一个proposer在阶段2中向编号为1,2,….m的m个acceptor发送accept消息,一定存在一个acceptor i (1≤ i ≤ m),它的值被设为值v,并且在这之前不是v. 

    另外,为了保证阶段中的acceptor的承诺起作用,我们还必须假定:对于两个建议propose_1, propose_2,如果propose_2 发现的时刻大于 propose_1的发起时刻,那么propose_2的序号大于propose_1的序号.即序号的大小代表了时间先后.(这在实践上相当于假定了每一个agent上都有一个时钟并且时钟的差别不大).关于时钟的问题,请参见文献[3].

4 paxos算法的新的证明.

    这里是要证明,任何一个proposer按照步骤1,2那样的循环进行,一定可以停止,即在阶段2中发现某个值被超过半数的acceptor所接受.

    这里给出一种新的数学证明,与paxos算法提出者Leslie Lamport的证明相比更容易理解.

    acceptor不妨假定有2m+1个,使用编号1,2,….2m+1分别代表.

    根据3中的"假设",任一个proposer走到阶段二的时候,至少使上述排列中的某一个元素的v发生变化.所以,一个proposer 经过有限个循环(走完两个阶段),一定可以使超过半数(不妨假设为m+1个)的acceptor的值都被设置了(即不再是空值).但是不同的acceptor被设置的值可能不同,原因在于可能出现以下类似的现象:

    当某个proposer a向编号为1,2,3…m的acceptor发送accept消息,成功给它设置了某个值value_1(其建议的序号记为proposal_number_1).此时有另一个proposer b向,2,3,4,…m, m+1,m+2这些acceptor发送prepare消息,其建议的序号为proposal_number_2 ,并且proposal_number_2 > proposal_number_1.当a向

    此时,m+1个acceptor已经被设置了值,另外一些acceptor还没有被设置值.

    不妨假设这m+1个acceptor每一个被设置的值都不同.当然也都不是空.这些值的序号也不相同.这些序号中最大的序号不妨记为max_proposal_number,其值记为max_value.于是,一定存在一个proposer曾经以序号max_proposal_number走过阶段1,阶段2,把这个max_value设置到某个acceptor上.

    此时,对于某个proposer(不妨称呼为a),如果走完了阶段1:proposer a收到的回应个数超过半数,于是它一定可以从某个acceptor处收到max_proposal_number及max_value.这个proposer在阶段2中,会使用一个新的序号n(大于max_proposal_number),把max_value 设置到一个新的acceptor上,使max_value出现的次数变大,同时满足:现在现有已经被设置了值的acceptor中,被设置的序号最大的那个序号所对应的值仍然是 max_value.

(注意:不同的序号,值可能是一样的).

    这样再有proposer(或者是a或者是其他的proposer)发起accept消息的时候,像上面分析一样,所选定的值,仍然是max_value.于是经过若干次个循环以后,一定会max_value出现的次数超过半数.

参考文献

[1] Leslie Lamport, The part-time parliament

[2] Leslie Lamport, paxos-simple

[3] Fischer, et al, The impossibility of distributed consensus with one faulty process