第二部分主要介绍了Paxos的算法内容和具体的证明过程

Paxos算法的提出与证明

首先在分布式系统中所有节点的角色分为proposers，acceptors，和learners。但是允许一个节点身兼数职。

  • proposers提出提案，提案信息包括提案编号和提议的value；
  • acceptor收到提案后可以接受[accept]提案，若提案获得多数acceptors的接受，则称该提案被批准[chosen]
  • learners只能“学习”被批准的提案。

划分角色后，就可以更精确的定义问题：

  • proposers先提出proposal，被批准后才能成value[决议]；
  • 在一次Paxos算法的执行实例中，只批准[chosen一个value；
  • learners只能获得被批准[chosen]的value。作者通过不断加强上述3个约束[主要是第二个]获得了Paxos算法。

批准value的过程中，首先proposers将value发送给acceptors，之后acceptors对value进行接受[accept]。为了满足只批准一个value的约束，要求经“多数派[majority]”接受的value成为正式的决议[称为“批准”决议]。

这是因为无论是按照人数还是按照权重划分，两组“多数派”至少有一个公共的acceptor，如果每个acceptor只能接受一个value，约束2就能保证。回顾之前举出的5个议员例子，两个并发的草案都要获得至少3个议员批准，所以一定会有至少一个议员同时受到了两份草案。他的决定会觉得哪个草案被批准，也就保证了一次Paxos中，只会批准一个草案[chosen一个value]。

那么对于同时接受多份草案的议员如何选择，先来后到是第一个考虑的因素，即批准第一个。

于是产生了一个新约束：

P1:一个acceptor必须接受[accept]第一次收到的提案。

注意P1是不完备的。比如在一个acceptor总数为偶数的分布式系统中，恰好一半acceptor接受的提案具有value A，另一半接受的提案具有value B，那么就无法形成多数派，无法批准任何一个value。

约束2是一次Paxos算法执行中，只能批准一个value。但并不要求只批准一个提案，暗示可能存在多个提案，因为只要提案的value是一样的，批准多个提案不违背约束2。

于是可以产生新约束：

P2:一旦一个具有value v的提案被批准[chosen]，那么之后批准[chosen]的提案必须具有value v。 注：通过某种方法可以为每个提案分配一个编号，在提案之间建立一个全序关系，所谓“之后”都是指所有编号更大的提案。

也就是虽然几个提案的编号可能不同，但是他们所提出的value是一样的。

如果P1和P2都能够保证，那么约束2就能够保证。 批准一个value意味着多个acceptor接受[accept]了该value。因此，可以对P2进行加强：

P2a:一旦一个具有value v的提案被批准[chosen]，那么之后任何acceptor再次接受[accept]的提案必须具有value v。

由于通信是异步的，P2a和P1会发生冲突。比如设想一个场景，如果一个value被批准后，一个proposer和一个acceptor从休眠中苏醒，前者提出一个具有新的value的提案，对于这个新苏醒acceptor来说，根据P1，这个proposal会被接受。根据P2a，则不应当接受，这中场景下P2a和P1有矛盾。

于是需要换个思路，转而对proposer的行为进行约束：

P2b:一旦一个具有value v的提案被批准[chosen]，那么以后任何proposer提出的提案必须具有value v。

由于acceptor能接受的提案都必须由proposer提出，所以P2b蕴涵了P2a，是一个更强的约束。

但是根据P2b，难以提出具体的实现手段。因此需要进一步加强P2b。 假设一个编号为m的value v已经获得批准[chosen]，来看看在什么情况下对任何编号为n[n>m]的提案都含有value v。因为m已经获得批准[chosen]，显然存在一个acceptors的多数派C，他们都接受[accept]了v。

考虑到任何多数派都和C具有至少一个公共成员，可以找到一个蕴涵P2b的约束P2c：

P2c:如果一个编号为n的提案具有value v，那么存在一个多数派，要么他们中所有人都没有接受[accept]编号小于n 的任何提案，要么他们已经接受[accept]的所有编号小于n的提案中编号最大的那个提案具有value v。

P2c稍微难懂一点，现在一个value v已经获得了多数派C的批准那么如何保证后续的提案都是value v？就是P2c，要求后面再来的任何一个多数派[他们中必有至少一个公共成员是个多数派C]，那就通过要求要么就是所有人都没有接受编号小于n的任何提案，要么就是所有人已经接受所有编号小于n的提案中编号最大的那个提案具有value v。所以如果P2c能够得到保障，那么P2b也必然获得。

可以用数学归纳法证明P2c蕴涵P2b：

假设具有value v的提案m获得批准，当$n=m+1$时，采用反证法，假如提案n不具有value v，而是具有value w，根据P2c，则存在一个多数派S1，要么他们中没有人接受过编号小于n的任何提案，要么他们已经接受的所有编号小于n的提案中编号最大的那个提案是value w。由于S1和通过提案m时的多数派C之间至少有一个公共的acceptor，所以以上两个条件都不成立，导出矛盾从而推翻假设，证明了提案n必须具有value v； 若$(m+1)..(n-1)$所有提案都具有value v，采用反证法，假如新提案N不具有value v，而是具有value w’,根据P2c，则存在一个多数派S2，要么他们没有接受过$m…(n-1)$中的任何提案，要么他们已经接受的所有编号小于N的提案中编号最大的那个提案是value w’。由于S2和通过m的多数派C之间至少有一个公共的acceptor，所以至少有一个acceptor曾经接受了m，从而也可以推出S2中已接受的所有编号小于n的提案中编号最大的那个提案的编号范围在$m…(n-1)$之间，而根据初始假设，$m…(n-1)$之间的所有提案都具有value v，所以S2中已接受的所有编号小于n的提案中编号最大的那个提案肯定具有value v，导出矛盾从而推翻新提案n不具有value v的假设。根据数学归纳法，我们证明了若满足P2c，则P2b一定满足。 P2c是可以通过消息传递模型实现的。另外，引入了P2c后，也解决了前文提到的P1不完备的问题。

Paxos算法内容

要满足P2c的约束，proposer提出一个提案前，首先要和足以形成多数派的acceptors进行通信，获得他们进行的最近一次接受[accept]的提案[prepare过程]，之后根据回收的信息决定这次提案的value，形成提案开始投票。当获得多数acceptors接受[accept]后，提案获得批准[chosen]，由proposer将这个消息告知learner。

这个简略的过程经过进一步细化后就形成了Paxos算法。在一个paxos实例中，每个提案需要有不同的编号，且编号间要存在全序关系。可以用多种方法实现这一点，例如将序数和proposer的名字拼接起来。如何做到这一点不在Paxos算法讨论的范围之内。如果一个没有chosen过任何proposer提案的acceptor在prepare过程中回答了一个proposer针对提案n的问题，但是在开始对n进行投票前，又接受[accept]了编号小于n的另一个提案[例如n-1]，如果n-1和n具有不同的value，这个投票就会违背P2c。因此在prepare过程中，acceptor进行的回答同时也应包含承诺：不会再接受[accept]编号小于n的提案。这是对P1的加强：

P1a:当且仅当acceptor没有回应过编号大于n的prepare请求时，acceptor接受[accept]编号为n的提案。现在已经可以提出完整的算法了。

决议的提出与批准

通过一个决议分为两个阶段：

准备阶段：

proposer选择一个提案编号n并将prepare请求发送给acceptors中的一个多数派；acceptor收到prepare消息后，如果提案的编号大于它已经回复的所有prepare消息，则acceptor将自己上次接受的提案回复给proposer，并承诺不再回复小于n的提案；

批准阶段：

当一个proposer收到了多数acceptors对prepare的回复后，就进入批准阶段。它要向回复prepare请求的acceptors发送accept请求，包括编号n和根据P2c决定的value[如果根据P2c没有已经接受的value，那么它可以自由决定value]。在不违背自己向其他proposer的承诺的前提下，acceptor收到accept请求后即接受这个请求。这个过程在任何时候中断都可以保证正确性。例如如果一个proposer发现已经有其他proposers提出了编号更高的提案，则有必要中断这个过程。因此为了优化，在上述prepare过程中，如果一个acceptor发现存在一个更高编号的提案，则需要通知proposer，提醒其中断这次提案。