Paxos算法介绍—Basic Paxos

作者: WILL_HUNTING | 来源:发表于2019-02-14 14:07 被阅读0次

1算法背景和问题分析

1.1 Paxos算法解决的问题

Paxos算法解决的问题是一个分布式系统如何就某个值(决议)达成一致。一个典型的场景是，在一个分布式数据库系统中，如果各节点的初始状态一致，每个节点都执行相同的操作序列，那么他们最后能得到一个一致的状态。为保证每个节点执行相同的命令序列，需要在每一条指令上执行一个“一致性算法”以保证每个节点看到的指令一致。一个通用的一致性算法可以应用在许多场景中，是分布式计算中的重要问题。

节点通信存在两种模型：共享内存(Shared memory)和消息传递(Messages passing)。Paxos算法就是一种基于消息传递模型的一致性算法。

1.2 不一致性问题的产生

如图1所示，一般银行ATM系统的体系结构：C={c1,c2,…,cn}代表n个客户端（ci一个实例是取款机），S={ s1,s2,…,sm }代表m个服务端（si响应每个与之相连的客户端的命令请求；Paxos算法运行的实体）。

1 银行ATM结构图

采用这样的体系结构的目的就是保证在若干个服务端出现故障的情况下，所有的客户端仍能不受影响地进行工作。从而，本文讨论的一致性问题始终是在保证系统可靠性的前提下------因为解决一致性问题最简单而又最不明智的办法就是只设置一个数据处理端（在ATM模型中只存在一个S），这样永远都不会出现不一致的问题。

由于C与S之间的通信是异步的，那么如果c1,c2,c3分别发出如下命令a, b, c，即operation(c1)=a，operation(c2)=b, operation(c3)=c，那么总共可能会产生A³₃=3!=6种合法命令序列，即(a, b, c), (a, c, b),…, (c, b, a)。本文不讨论不合法的命令序列，譬如(a, a, c)，这在下文会给假设与解释（此外，如果a任务一定要在b之间执行，那么(b, a, c)此类序列也变得不合法。在本文中假设a, b任务之间是没有顺序制约的，可以想象成a任务为某一个用户在帐户A上进行一个取款操作，b任务为另一个用户在帐户B上进行一个存款操作，由于A, B是两个不相同的帐户，所以a任务的执行与b任务的执行不相关）。如果S中的每一个服务端执行了不同的合法命令序列，将会导致整个系统的不一致性问题，所以Paxos的任务是保证S中每一个处于正常工作的服务端都将执行一个相同的命令序列，例如(a, b, c)。

1.3 推广到更一般的情况

Lamport的论文 "Paxos Made Simple"中更通用地描述了这个问题的模型。

2. 分布式系统一致性问题模型

1.3.1 问题描述

假设一组进程可以用来提出不同的值（例如在数据库系统中，不同的事务可能对同一个表格中的同一行中的同一个元素进行更新，而且这些事务所修改的值也不相同）。一致性算法就是用来保证仅有一个进程/事务所提出的值能够被选中（这里的仅有一个我想可能是说每次更新表格元素时仅有一个值被选中，不同的值可能在下一次更新时被选中）。如果没有值被提出，那么就没有值被选中。如果某个值被选中，那么这些进程应该能够学习到被选中的值。该一致性算法的安全性要求如下：

仅有一个被提议的值可以被选中。
仅有一个值被选中，且
一个进程不可能学习到一个被选中的值，除非这个值真的被选中。

这里作者不想说明算法的详细Liveness特性的要求。Liveness属性的目的大致就是为了保证某些被提议的值最终能够被选中，且，如果一个值被选中，那么一个进程最终能够学到这个被选中的值。（这里的最终（eventually）在上述的TLA+中是一种时序逻辑，Liveness笼统的含义就是“某些好的事情最终能够发生”，Safety的笼统含义就是“某些坏的事情一定不会发生”）。

1.3.2 假设前提

假设进程间可以通过消息传递来进行通信（大多数分布式算法/协议的通信模型都是基于消息传递）。文中基于的通信模型是异步的、非拜占庭模型【The Byzantine Generals Problem】，其中：

每个Agent/角色以任意的速度处理事务，可能失败并停止，也可能重启。因为所有的进程可能在一个值被选出后失败并重启，那么失败重启前已知的信息需要被保存，使得在重启后仍保留之前已知的信息。
消息传递的时间可能很长，消息可能被重复发送，消息可能丢失，但是消息的内容不会被篡改。

1.4 问题分析

1.4.1 角色分类

便于理解，在这里把一个结点的所有行为概括成3种角色：Proposer, Acceptor, Learner。可以认为在一个结点中Paxos算法的行为可以被独立地分成3种对象来执行，对象之间的交互是统一的。其中：

Proposer向Acceptor提交提案（proposal），提案中含有决议（value）。
Acceptor审批提案。
Learner执行通过审批的提案中含有的决议。

在具体的工程实践中一个进程可能同时具有三种角色，这不会影响算法的正确性，但这里作者不关心这个情况。我们可以认为一个进程仅有一个角色。

1.4.2 Lamport的方法

一个最简单的选值的办法就是仅仅使用一个acceptor agent（集中式）。一个proposer发送一个proposal给acceptor，acceptor选择第一个接收到的proposal中的value。虽然简单，但是该方法会存在单点故障：这个acceptor失效后，无法进行下面的操作。

Lamport使用了另一种方法，也就是分布式的方法。在系统中使用多个acceptor。一个proposer可以向一组acceptor发送proposal（问题一：这里的一组是所有的acceptor还是其中的一部分？）。一个acceptor可能接受proposer发送的proposal（意味着也可能不接受/决绝）。一个proposal中的value被选中的条件是：大部分的aceptor接受了该proposal。大部分指的具体数量是多少呢？大部分就是指的大多数（超过一半的数量，假设一个proposer将一个proposal发送给n个acceptor，那么这里的大多数就是指超过n/2个acceptor。由此可知，n最好是奇数）。这样就能保证任意两拨接收了proposal的acceptor之间存在至少一个相同的acceptor，也就保证了这两拨acceptor接收的是同一个proposal。

2 算法推导和介绍

2.1 算法推导

以下翻译自Lamport的论文 "Paxos Made Simple"，参考的是这篇翻译稿【Paxos Made Simple（Paxos算法）】

众所周知Paxos算法很难理解，以至于Lamport发表"The Part-Time Parliament"论文之后又发表了一篇 "Paxos Made Simple"论文来进一步用更直观的语言解释Paxos。跟"The Part-Time Parliament"不同，这篇文章并没有对Paxos严格的数学证明过多解释（没有解释证明过程），而是从问题出发，一步一步演绎归纳出Paxos算法。

在这我们假设大多数这个约束条件为rule 1：

R1：大多数acceptor接受了某个值后，该值才算被接受。

在没有进程失效或者消息丢失的情况下，我们想要选择一个value就需要当仅有一个proposer提出一个value时，acceptor就要选中这个value。这需要我们的算法满足如下的条件：

P1：一个acceptor需要接受/同意其第一次收到的proposal中的value。

这个条件是保证被提出的proposal能够被接受。但是这存在一个问题，不同的proposer可能提出不同的proposal且proposal中的value都不一样。极端的情况下：n个proposal提出了n个不同的proposal，正好有n个acceptor分别接受了其中一个proposal。这就导致了每个acceptor接受的proposal和将要选中的value都不一样。这就不满足上述的大多数同意的要求（即R1）。即使仅有两个proposer提出proposal，当系统中的一个acceptor失效后，也存在每个proposal被一般的acceptor接受的情况，这时候，失效的那个acceptor无法学习到那个proposal中的value最终被接受了。（这里说的是一个acceptor在某个value被选出来之前失效。）

P1和R1意味着一个acceptor必须能够接受超过一个proposal。为了便于区分proposal，我们使用编号来为每个proposal做记号（编号就是一个数字）。因此，一个proposal需要包含两个元素：编号和value。（这里将这个proposal表示为p<n,v>，n表示标号，v表示value）。为了保证不同的proposer提出的proposal上面的编号不一样，需要特殊的机制来获取编号（比如可以根据系统中的acceptor的数量n以及这个proposer的编号m，例如编号为m的proposer提出的proposal的编号变化方式为m+i*n，i是提出proposal的次数，即i>=0）。一个value被接受的条件就是一个带有该value的proposal被大多数的acceptor接受。这样，我们就说这个value和该proposal被接受了。

我们允许多个proposal被接受，但是我们需要保证所有的被选中的proposal里面带有的value是相同的。我们得出了下面的约束条件：

P2：如果一个带有某个value的proposal被选中，那么所有的带有较高编号的proposal中的值必须也是这个value。

即，如果p<n,v>被选中，那么对于所有的其它proposal p<n',v'>，必须满足：如果n'>n，那么v'=v。既然编号n是全局编号的，那么P2就保证了算法的Safety，即仅有一个value会被选中。（这里意味着，某个值被选中后，仍然有可能存在一些proposer继续对某个值提出proposal。所以这里要求后续的proposal中携带的value需要满足一些条件以实现唯一的value被选择。）

某个proposal被选中，这个proposal就需要被至少一个acceptor接受。（接受操作在选中操作之前，二者具有时间的先后顺序）。因此，我们将约束向向前推：

P2a：如果一个带有某个value的proposal被选中，那么所有被acceptor接受的带有较高编号的proposal中的值必须也是这个value。

P2a保证了P1，为了同时保证P2和P2a，进一步提出了约束条件：

P2b：如果一个带有某个value的proposal被选中，那么所有proposer提出的带有较高编号的proposal中的值必须也是这个value。

因为proposal只有proposer能够发出，因此P2b就隐含了P2a和P2。

既然proposer的行为被约束了，那么acceptor的行为也要发生改变，这种改变要保证P2b的满足。P2c给出了acceptor需要满足的条件P2c：

P2c：对于任意的v（value）和n（number），如果一个有<n,v>构成的proposal被某个proposer发出，那么形成大多数acceptor集合S中的acceptor具有这样的特点：要么，S中没有一个acceptor接受过任何一个编号小于n的proposal；要么，S中的acceptor接受过的编号小于n的proposal中编号最高的那个proposal携带的value为v。

P2c的满足隐含了P2b的满足（证明略）。

为了保证P2c，一个proposer想要发出一个编号为n的proposal时需要学习小于编号n的所有proposal中编号最高的proposal，这个proposal是将要或者已经被S中的acceptor接收的proposal。（有点绕，意思就是，一个proposer想要发出更高编号的proposal之前需要learn系统中已经被大多数acceptor接收或者将要接收的proposal的编号）。这里原文说明的不是很详细，首先proposer想要发出一个proposal时候如何获得已经被接受的proposal的编号呢？其实这和步骤是在proposer发送上一个proposal'是从acceptor的回复中获得的。同时，此处也没说细说acceptor的如何回复接受到的proposal。后面会详细说。

这里的P2c的目的就是要保证每一个新的proposal的编号大于之前的编号，而且新的proposal的value要与已经接受的proposal的value保持一致（如果之前没有value被接受的话，那么新value可以为任意值）。

为了保证P2c，下面的两个算法描述了一个proposer发送proposal时需要执行的步骤：
（1）一个proposer选择一个新的编号并发送一个request给某个大多数acceptor组成的acceptor集合中的每一个，并要求acceptor承诺以下两件事：
（a）不再接受编号小于n的其它的proposal，且
（b）将这个acceptor已经接受过的编号小于n的proposal中编号最大的那个proposal放在回复消息中（如果这个acceptor确实接受过其它的proposal，否则回复空）。

我们将这个步骤称为带有编号为n的prepare request阶段。
（2）如果一个proposer收到了大多数的acceptor的满足上述承诺的回复消息，那么这个proposer就可以发送一个编号为n，且带有value为v的proposal给acceptor（给多少个acceptor？我觉得大多数的acceptor就可以。或者比较低效的方法就是每一个acceptor，这里原文也没有细说）。这里的value就是上一个prepare request阶段中收到的回复消息中的value。这个value是编号小于n中最大的那个proposal携带的value，如果所有的acceptor回复的消息中显示没有任何的proposal被接受，bane这个proposer就可以根据自己的需要设定value值。

此处要注意，proposer通过发送一个proposal给某些acceptor来提交最终的proposal。这里作者也没有细说发送给哪些acceptor。只是说了这次发送的acceptor可以和上一轮发送回复的acceptor不一样。当然，肯定是超过半数的acceptor会接收到这次的proposal消息。这个阶段被称为accept request阶段。（此阶段也可能会选不出value，即accept request也可能不会被接受，因为在prepare request回复和accept request被acceptor接收之间，acceptor可能接受一个编号大于n且value同样为v的新的proposal，这样的情况不断循环出现的话，没完没了了--活锁。basic paxos还没什么彻底的方法解决活锁问题）。

下面来介绍acceptor可能执行的操作，一个acceptor可能会接收到两种请求：prepare请求和accept请求。一个acceptor可以拒绝任何请求而不会导致算法出现Safety问题（但是没有必要的情况下，acceptor还是会好好工作，而不会任性的随意拒绝一个request）。也就是说，当这个acceptor允许回复request请求时，它总是会回复的。其总是会回复一个prepare request，但是，当且仅当一个acceptor没有对其它的带有更高编号的proposal做出承诺时，该acceptor才会回复accept request并接受这个proposal。也就是对P1的加强：

P1a：一个acceptor仅在没有对含有比当前收到的accept request请求中的proposal携带的编号还要高的其它proposal做出上述承诺时，该acceptor才可接受此次accept request中的proposal。（也就是说acceptor虽然对你做出了不接受较小编号的proposal的承诺，但是它不承诺不会接受较高编号的新proposal。意思就是现在你的身份只是备胎，在没有找到新备胎之前我还是你女朋友，否则你就成前任备胎了）。

一个acceptor将不再回复带有低编号的proposal（你都称为前任备胎了，我也就不用回你短信了，你自己就清楚状况了）。同时，一个acceptor也不会再次回复已经回复过的相同的prepare request（可能是因为消息重复接受，没有必要再回复一次）。

所以一个acceptor仅需要记住已经接受过的编号最大的那个proposal，和回复这个proposal所对应的proposer。因为P2c必须要能够保证才能保证算法的正确性（Safety），也就是说一个acceptor必须记住这个信息，即使它失效后重启（持久化这个信息）。而一个proposer可以不负责任的随时忘记自己发送过的proposal，只要之后别再发送具有相同编号的proposal即可。

2.1 算法描述

将proposer和acceptor的操作放在一起，我们可以看出，这个算法可以分为两个阶段：

Phase 1：

一个proposer选择一个编号n，并发送一个携带该编号的prepare request给大多数的acceptor；
当一个acceptor接收到一个prepare request，如果n大于之前已经恢复过的所有prepare request中的编号，那么acceptor将回复这个prepare request（带上承诺：不再接受编号小于n的prepare request，和，当前已经接受的编号最高的proposal的信息）给这个proposer（如果这个acceptor之前确实回复过这样的prepare request，如果这个acceptor第一次被prepare request，那么其承诺：不再接受编号小于n的prepare request，并回复一个空给proposer）。

Phase 2：

如果一个proposer收到了来自大多数的acceptorprepare request的回复，那么其将再次发送一个accept request给这些acceptor（这儿又说回复相同的acceptor）带上编号n和value v。这里的v时根据acceptor对prepare request的回复消息来定的，如果回复消息中有前一个proposal已经提出的value，那么v就等于之前的value，否则这个proposer可以自己确定想要的value。
如果一个acceptor收到了一个编号为n的accept request，除非在此之前其又接受了一个编号比n大的新的proposal，否则，这个acceptor将接受这个accept request。

一个proposer可以发出多个proposal，只要遵守上述的协议。一个proposer也可以在任何时候放弃自己的请求。从性能方面来考虑的话，如果一个acceptor接受了一个编号较高的新的proposal后，它应该通知之前回复过的proposer一遍这个proposer能够及时放弃后续操作而避免性能损失。这里仅仅是一个性能优化方面的考虑，不涉及到正确性问题。

2.2 算法分角色描述

2.2.1 Proposer行为分析

(1.1). 向所有的Acceptors发送Prepare(N_A)请求；
(1.2). 如果收到Reject(N_H)信息，那么重新发送Prepare(N_H+1)；
(2.1). 如果收到Acceptors集合的任意一个Majority的Promise(N_A, V_A)回复，那么如果所有的V_A均为空，Proposer自由选取一个V_A’，回发Accept(N_A, V_A’)；否则回发Accept(N_A, V_i)；
(2.2). 如果收到Nack(N_H)，回到(1.1)过程，发送Prepare(N_H+1)；
(3.1). 如果收到任意一个Majority所有成员的Accepted信息（表明选举完成），向所有Proposers发送自身成为leader的消息；
(3.2). 向Learner发送value值。

其中：
N_A为该次提案的编号；
N_H为当前提案的最高编号；
V_i为V_A中提案编号最高的value；

2.2.2 Acceptor行为描述

(1.1). 接收Prepare(N_A)，如果N_A>N_H，那么回复Promise(N_A, V_A)，并置N_H=N_A；否则回复Reject(N_H)
(2.1). 接收Accept(N_A, V_A)，如果N_A<N_H，那么回复Nack(N_H)信息（暗示了该Proposer提完案后至少有一个其余的Proposer广播了具有更高编号的提案）；否则设置this.V_A=V_A，并且回复Accepted信息。

其中：
Promise(N_A, V_A)：向Proposer保证不再接受编号不大于N_H的提案；
Accepted向Proposer发送决议被通过信息；
V_A为Acceptor之前审批过的决议（允许为空）；
N_H为Acceptor之前接收提案的最高编号。

2.2.3 Learner行为描述

相对来说，Learner的行为理解更简单一些：学习value，开始执行任务。

2.3 算法整体描述

角色/时段	Phase1	Phase2	Phase3
Proposer(P)	[1]提议：向A发送prepare	[1]接收A的promise；[2]选取一个value并发送accept	（*）
Acceptor(A)	[1]接收处理P的prepare；[2]回复reject或promise	[1]接收处理accept；[2]回复accpted或nack；[3]通知Learner	（*）
Learner(L)	无	无	[1]接收广播学习value或创建proposer对象学习value

2.4 学习一个被选中的value

一个learner如果想要学习被选中的value的话，那么其就要去查询被大多数acceptor接受的proposal。最简单的做法就是，每当一个acceptor接受了一个新的proposal后就主动将该信息发送给所有的learner。这种方法能够保证所有的learner及时的更新被选中的value，但是会导致性能上的问题，因为这个方法在更新learner的知识时候需要的消息发送条数为：acceptor的个数 * learner的个数。

前面的非拜占庭消息发送模型保证了一个learner可以从其它的learner处学习某个被选中的value。那么一个acceptor在接受一个proposal后仅仅需要通知其中一个不同的learner就可以，其它的learner可以从这个learner处学习到。但是这优惠导致一个问题，如果这个learner在传播新学到的value之前挂掉的话，那么这个心value就无法被学习了。同样，那就折中考虑吧，选择更新部分learner，这里就要在具体实现的时候综合考虑性能和一致性之间的平衡问题了。

如果一个learner实在学不到新value的话，那么还有最后一招，这个learner自己起一个proposer来提交proposal，这时候肯定就能学到最新的value了。

3 算法证明

正式的表述是，一轮表决B由下面4个要素组成:(除非特别说明，集合指有限集合)

$B_{dec}$ 一条法令(被投票的那条 decree)
$B_{qrm}$ 一个牧师的非空集合(表决的法定人数集 quorum)
$B_{vot}$ 一个牧师的集合(所有对法令作出投票(赞成)的牧师)
$B_{bal}$ 这轮表决的编号

说一轮表决B是成功的，当且仅当 $B_{qrm} \subseteq B_{vot}$ ，所以一轮成功的投票是每一个法定人数集的成员都投了票的(赞成票，不赞成则不投票)。
表决的编号从一个无界有序的数字集合中选取。如果 $B_{bal}^1 > B_{bal}$ ，则说B¹ 比B大。但这并不能表明表决进行的顺序。一个大的表决实际上可以在一个小的表决之前发生。(这里故意将 later 翻译成了大，省得 later 和 before 掺杂不清)
Paxos 的数学家在一个由多轮表决构成的集合上定义了3个条件，然后展示了如果已经进行过的表决满足这些条件，那么一致性会得到保证，进行性也是可能的。头两个条件比较简单，可以被非正式的描述如下:

$B1(\beta)$ : 中的每一轮表决，都有一个唯一的编号
$B2(\beta)$ : 中任意两轮表决的法定人数集中，至少有一个公共的牧师成员
第三个条件更复杂一些。在一个Paxos人的手稿中包含了如下内容，比较绕，描述了这个条件:
$B3(\beta)$ :对于 $\beta$ 中每一轮表决B，如果B的法定人数集中的任何一个牧师在 $\beta$ 中一个更小轮的表决中投过(赞成)票，那么B的法令与所有这些更小轮表决中的最大的那次表决的法令相同

图1的手稿帮助诠释了这一段隐晦的文本。手稿画出了5个牧师 A、B、C 、D和 E 的5轮投票来阐明条件 $B3(\beta)$ 的含义。5轮表决组成了集合，对于其中的每轮表决，投了票的牧师集合是定额集合牧师的子集，投了票的牧师被方框圈起来。例如，第14轮表决的法令是，定额集合包含3位牧师和两个投票者。条件 $B3(\beta)$ 有这样的形式:“对于中的每一个B:...”，这里“...”是一个限制在表决B 上的条件。图1中5个表决的条件描述如下:

#	法令	Α	Β	C	D	E
2	α	×	×	×	√	缺席
5	β	×	×	√	缺席	×
14	α	缺席	√	缺席	×	√
27	β	√	缺席	√	√	缺席
29	β	缺席	√	×	×	缺席

图 1:Paxos 手稿展示了五轮表决组成的集合，满足条件 $B1(\beta)- B3(\beta)$ (加上了说明性的列头)

2.编号为2的表决是最小(早)的表决，从而这轮投票的条件也都满足
5.编号为5的表决中没有牧师在更小号的投票中投过票，所以这轮的条件也平凡的满足
14.这轮表决的定额集合中，唯一一个在更小编号的表决中投过票的牧师是，他在编号为2的表决中投了票，所以要求这轮的法令和2的法令必须相等(成立)
27.(这是一次成功的表决)27 轮表决的定额集合是 A、C、D。牧师A没有在更小号的表决中投过票。投过票的小编号表决只有5，投过票的小编号表决只有2；这两个更小编号表决中最大的是5，所以条件要求本轮的法令和5的法令相同。(成立)
29.本轮的定额集合是 B、C、D。B投过票的小编号表决只有14，是5和27，是 2和27。这4个小编号表决中最大的一个是27，所以条件要求29的法令和27的法令相同

正式的表述 $B1(\beta)- B3(\beta)$ 需要更多的符号标记。我们用符号 v 表示一个投票，那么 v 包含 3 个组成部分:投票的牧师 $v_{pst}$ ，本论表决的编号 $v_{bal}$ ，和所表决的法令 $v_{dec}$ 。Paxos 人同时定义了 $v_{bal} =-\infty$ ， $v_{dec}=BLANK$ 的投票 v 为 null 投票。对于 $-\infty< b < \infty$ 的所有编号为 b 的表决，不会以 BLANK 作为法令。对于任意牧师 p，他们定义了 $NULL_{p}$ 作为唯一的 null 投票 v， $v_{pst}=p$ 。

Paxos 数学家为所有投票定义了一个全局顺序，但是手稿里包含了这个定义那一部分遗失了，剩下的片段显示，对于任意 v' 和v ，如果 $v'_{bal} < v_{bal}$ ，则 v < v' 。当 v = v'时，v 和 v' 的相对顺序怎样定义的并不知道。

对于任意的表决组成的集合，定义集合 $Votes(\beta)$ 为包含所有满足如下条件的投票 v:存在 $B\in \beta$ ，B 使得 $v_{pst} \in B_{vot} ，v_{pst} \in B_{bal} ，v_{dec} = B_{dec}$ (即用 $Votes(\beta)$ 表示所有在 $\beta$ 中的投票)。

如果p是一个牧师，b是一个表决的编号或 $\infty$ ，则 $MaxVote(b,p,\beta)$ 定义为 $Votes(\beta)$ 投出的表决编号小于 $b(v_{bal} < b)$ 的最大的投票 v 或者空投票。如果没有这样的投票，因为 $NULL_{p}$ 比所有 p 实际投出的票都要小，这就意味着 $MaxVote(b,p, \beta)$ 是下面集合中的最大投票:

$\{v \in Votes(\beta) : (v_{pst}=p) \land (v_{bal}<b)\} \cup \{null_{p}\}$

对于任意非空的牧师集合 $Q$ ， $MaxVote(b,Q,\beta)$ 定义为对于所有 $p \in Q$ ，所有 $MaxVote(b,p,\beta)$ 中的最大值。
条件 $B1(\beta)-B3(\beta)$ 正式表述如下:

$B1(\beta) \triangleq \forall B, B' \in B : (B \ne B') \Rightarrow (B_{bal} \ne B'_{bal})$

$B2(\beta) \triangleq \forall B, B' \in B : B_{qrm} \cap B'_{qrm} \ne \phi$

$B1(\beta) \triangleq \forall B, B' \in B : MaxVote(B_{bal}, B_{qrm}, \beta)_{bal} \ne -\infty) \Rightarrow (B_{dec} = MaxVote(B_bal, B_{qrm}, \beta)_{dec})$

虽然MaxVote的定义依赖于投票的顺序，但是 $B1(\beta)$ 表明 $MaxVote(B, Q, \beta)$ 是与表决编号相同的投票间有怎样的顺序无关的。
为了展示这些条件能够导出一致性，Paxos 人首先展示 $B1(\beta)- B3(\beta)$ 能够得出，如果β 中的表决 B 是成功的，那么β 中更大编号的表决和 B 有相同的法令:
引理：如果保持 B1(β)、B2(β) 和 B3(β)成立，那么对于任意β中的B，B' 有:

$(B_{qrm} \subseteq B_{vot}) \land (B_{bal} < B_{bal}) \Rightarrow(B'_{dec} = B_{dec})$

引理的证明:

对于任意 $β$ 中的表决 B，令 $ψ (B, β )$ 表示 $β$ 中所有编号大于 B 且法令与 B 不同的所有表决的集合:

$\Psi(B, \beta) \triangleq \{B' \in \beta : (B'_{bal} > B_{bal}) \land (B'_{dec} \ne B_{dec})\}$

证明引理只需证明如果 $B_{qrm} \subseteq B_{vot}$ ，则 $ψ (B, β )$ 为空。Paxos 人给出了一个反证法的证明。他们假设存在 B 使得 $B_{qrm} \subseteq B_{vot}$ 同时 $\psi(B, \beta) != \phi$ ，然后得到一个矛盾：

选择 $C \in ψ (B, β)$ ，使得 $C_{bal}=min\{B^{1}_{bal}:B^{1} \in \psi(b, \beta)\}$
证明:由 $ψ (B, β)$ 不为空并且有限，所以 C 存在得出。
$C_{bal} > B_{bal}$
证明:由 1 和的定义得出
$B_{vot} \cap C_{qrm} \ne \phi$
证明:由 $B2(β)$ 和假设 $B_{qrm} \subseteq B_{vot}$ 得出
$MaxVote(C_{bal},C_{qrm},\beta)_{dec} = C_{dec}$
证明:由 2、3 和 $MaxVote(C_{bal},C_{qrm},\beta)_{bal}$ 的定义得出
$MaxVote(C_{bal},C_{qrm},\beta) \in Votes(\beta)$
证明:由 4 和 $MaxVote(C_{bal},C_{qrm},\beta)_{bal}$ 的定义得出
$MaxVote(C_{bal},C_{qrm},\beta) = C_{dec}$
证明:由5和 $B3(β)$ 得出
$MaxVote(C_{bal},C_{qrm},\beta)_{dec} \ne B_{dec}$
证明:由 6、1 和 $\psi(B, \beta)$ 的定义得出
$MaxVote(C_{bal},C_{qrm},\beta)_{bal} > B_{bal}$
证明:由 4、7 和 $B1(β )$ 表明 $MaxVote(C_{bal},C_{qrm},\beta)_{bal} \ne B_{bal}$ 得出
$MaxVote(C_{bal},C_{qrm},\beta) \in Votes(\psi(B, \beta))$
证明:由 7、8 和 $\psi(B, \beta)$ 的定义得出
$MaxVote(C_{bal},C_{qrm},\beta)_{bal} < B_{bal}$
证明:由 $MaxVote(C_{bal},C_{qrm},\beta)_{bal}$ 的定义得出
矛盾
证明:由 9、10 和 1 得出
引理证明结束

通过这个条引理，可以很容易的得出，如果 B1-B3 成立，那么任意两轮成功的表决，都是对相同法令的表决。
定理 1. 如果保持 $B1(β)$ 、 $B2(β)$ 和 $B3(β)$ 成立，那么对于任意 $β$ 中的 B，有:

$(B_{qrm} \subseteq B_{vot}) \land (B'_{qrm} \subseteq B_{vot}) \Rightarrow(B'_{dec} = B_{dec})$

定理的证明:
如果 $B^{1}_{bal}=B_{bal}$ ，则 $B1(β)$ 表明 $B^1=B$ 。如果 $B^{1}_{bal} \ne B_{bal}$ 则根据引理直接可以得到定理
定理证明结束

Poxos 人接下来证明了另一个定理:如果议会厅有足够的牧师，那么在遵守 B1-B3 要求的前提下，是有可能作出一次成功的表决的(既可能会产生一轮达成一致的表决)。尽管这不能保证进行性(不能保证一定会产生一轮成功表决)，但至少表明在 B1-B3 基础上的表决协议不会产生死锁

定理 2. 令表决编号 b 和牧师集合 Q 满足对于任意 $B \in \beta$ ， $b>B_{bal}$ 同时，如果 $B1(β)$ 、 $B2(β)$ 和 $B3(β)$ 条件成立，那么存在一轮表决 $B^1$ ， $B^1_{bal}=b$ 同时 $B^1_{qrm}=B^1_{vot}=Q$ 使得 $\beta \cup B^1$ 也满足 $B1(\beta \cup B^1)$ 、 $B2(\beta \cup B^1)$ 和 $B3(\beta \cup B^1)$ 这3个条件被满足的表决，以使程序进行下去)

定理的证明:
$B1(β)$ 、 $B^1$ 的选择，和 b 的假定可以得出 $B1(\beta \cup B^1)$ ， $B2(β)$ 、 $B^1_{qrm}$ 的选择和Q的假设得出 $B2(\beta \cup B^1)$ 。如果 $MaxVote(b,Q,\beta)_bal = -\infty$ 则让 $B^1_{dec}$ 等于任意法令，否则让 $B^1_{dec}$ 等于 $MaxVote(b,Q,\beta)_{dec}$ ，然后加上 $B3(β)$ ， $B3(\beta \cup B^1)$ 得以成立
定理证明结束

4 算法示例

下面的示例图展示了Basic Paxos协议的集中代表性的例子/场景。同时，一些例子展示了Paxos处理分布式系统同某个（冗余）设备失败的情况。参考自wikipedia: Paxos

在首轮，由于没有Acceptor接收过任何value，所以首次提出proposal的时候，Acceptor返回的Promise信息是null。

4.1 正常流程

下图包含了1个Client，1个Proposer，3个Acceptors（在这个例子中，法定集合大小是3），2个Learners（下图中的两条竖线）。这个例子表示的是第一轮就成功达成一致的情况（消息通信过程中没有失败的情况）

Client   Proposer      Acceptor     Learner
   |         |          |  |  |       |  |
   X-------->|          |  |  |       |  |  Request
   |         X--------->|->|->|       |  |  Prepare(1)
   |         |<---------X--X--X       |  |  Promise(1,{Va,Vb,Vc})
   |         X--------->|->|->|       |  |  Accept!(1,V)
   |         |<---------X--X--X------>|->|  Accepted(1,V)
   |<---------------------------------X--X  Response
   |         |          |  |  |       |  |

其中,Va、Vb、Vc对应三个Acceptor接受过得最大编号对应的value；V是{Va, Vb, Vc}中最近的（对应编号最大的）。

4.2 Paxos处理故障的case

最简单的故障案例是一个Acceptor故障（法定集合的Acceptors仍然可用）和一个冗余Learner的故障。在这种情况下，Paxos协议无需恢复，仍然能成功达成一致：不需要重新发起一轮选举或者进行额外的信息传递。下面两张图展示了这两种情况。

一个Acceptor故障

下图中，Acceptors法定集合中的一个Acceptor故障了，法定集合size变成了2，这种场景下，Basic Paxos协议仍然成功达成一致。

Client   Proposer      Acceptor     Learner
   |         |          |  |  |       |  |
   X-------->|          |  |  |       |  |  Request
   |         X--------->|->|->|       |  |  Prepare(1)
   |         |          |  |  !       |  |  !! FAIL !!
   |         |<---------X--X          |  |  Promise(1,{Va, Vb, null})
   |         X--------->|->|          |  |  Accept!(1,V)
   |         |<---------X--X--------->|->|  Accepted(1,V)
   |<---------------------------------X--X  Response
   |         |          |  |          |  |

一个冗余的Learner故障

下面的例子里，一个冗余的Learner出现故障了，但是Basic Paxos协议依然执行成功。

Client Proposer         Acceptor     Learner
   |         |          |  |  |       |  |
   X-------->|          |  |  |       |  |  Request
   |         X--------->|->|->|       |  |  Prepare(1)
   |         |<---------X--X--X       |  |  Promise(1,{Va,Vb,Vc})
   |         X--------->|->|->|       |  |  Accept!(1,V)
   |         |<---------X--X--X------>|->|  Accepted(1,V)
   |         |          |  |  |       |  !  !! FAIL !!
   |<---------------------------------X     Response
   |         |          |  |  |       |

一个Proposer失败

在这个case中，一个Proposer提出一个proposal后，收到Acceptor的回复之前发生了故障。特别地，这个Proposer在发送Accept message期间故障了，因此法定集合中只有一个Acceptor收到了Accept请求以及请求value。同时，一个新的Leader（属于Proposer）被选举出来了（选举过程细节没有展示）。此时，第二轮选举发起，这个场景中Paxos算法进行了两轮选举达成一致。

Client  Proposer        Acceptor     Learner
   |      |             |  |  |       |  |
   X----->|             |  |  |       |  |  Request
   |      X------------>|->|->|       |  |  Prepare(1)
   |      |<------------X--X--X       |  |  Promise(1,{Va, Vb, Vc})
   |      |             |  |  |       |  |
   |      |             |  |  |       |  |  !! Leader fails during broadcast !!
   |      X------------>|  |  |       |  |  Accept!(1,V)
   |      !             |  |  |       |  |
   |         |          |  |  |       |  |  !! NEW LEADER !!
   |         X--------->|->|->|       |  |  Prepare(2)
   |         |<---------X--X--X       |  |  Promise(2,{V, null, null})
   |         X--------->|->|->|       |  |  Accept!(2,V)
   |         |<---------X--X--X------>|->|  Accepted(2,V)
   |<---------------------------------X--X  Response
   |         |          |  |  |       |  |

多个Proposer出现冲突（活锁）

最复杂的case是多个Prposer都认为他们是Leader，例如，当前的Leader可能故障然后马上恢复了，但此时其他Proposer已经重新选举了一个新的Leader。回复后的Leander当时没有了解到这个信息并且尝试发起一轮投票，这轮投票跟当前新的Leader冲突了。下图展示了4轮失败的选举，当然，接下来的轮次仍然可能出现冲突。

Client   Leader         Acceptor     Learner
   |      |             |  |  |       |  |
   X----->|             |  |  |       |  |  Request
   |      X------------>|->|->|       |  |  Prepare(1)
   |      |<------------X--X--X       |  |  Promise(1,{null,null,null})
   |      !             |  |  |       |  |  !! LEADER FAILS
   |         |          |  |  |       |  |  !! NEW LEADER (knows last number was 1)
   |         X--------->|->|->|       |  |  Prepare(2)
   |         |<---------X--X--X       |  |  Promise(2,{null,null,null})
   |      |  |          |  |  |       |  |  !! OLD LEADER recovers
   |      |  |          |  |  |       |  |  !! OLD LEADER tries 2, denied
   |      X------------>|->|->|       |  |  Prepare(2)
   |      |<------------X--X--X       |  |  Nack(2)
   |      |  |          |  |  |       |  |  !! OLD LEADER tries 3
   |      X------------>|->|->|       |  |  Prepare(3)
   |      |<------------X--X--X       |  |  Promise(3,{null,null,null})
   |      |  |          |  |  |       |  |  !! NEW LEADER proposes, denied
   |      |  X--------->|->|->|       |  |  Accept!(2,Va)
   |      |  |<---------X--X--X       |  |  Nack(3)
   |      |  |          |  |  |       |  |  !! NEW LEADER tries 4
   |      |  X--------->|->|->|       |  |  Prepare(4)
   |      |  |<---------X--X--X       |  |  Promise(4,{null,null,null})
   |      |  |          |  |  |       |  |  !! OLD LEADER proposes, denied
   |      X------------>|->|->|       |  |  Accept!(3,Vb)
   |      |<------------X--X--X       |  |  Nack(4)
   |      |  |          |  |  |       |  |  ... and so on ...

参考文献

Paxos Made Simple【翻译】
《Paxos Made Simple》
《The Part Time Parliament》
Paxos
Paxos Made Live(译)