作者丨郑建军
编辑丨Cindy
“与其预测未来，不如限制未来”，这应该是Paxos协议的核心思想。Paxos协议本身是比较简单的，如何将Paxos协议工程化，才是真正的难题。这是来自微信工程师的经验，以供参考。
引言
早在1990年，Leslie Lamport（即 LaTeX 中的"La"，微软研究院科学家，获得2013年图灵奖）向ACM Transactions on Computer Systems (TOCS)提交了关于Paxos算法的论文The Part-Time Parliament。几位审阅人表示，虽然论文没什么特别的用处，但还是有点意思，只是要把Paxos相关的故事背景全部删掉。Leslie Lamport心高气傲，觉得审阅人没有丝毫的幽默感，于是撤回文章不再发表。
直到1998年，用户开始支持Paxos，Leslie Lamport重新发表文章，但相比1990年的版本，文章没有太大的修改，所以还是不好理解。于是在2001年，为了通俗性，Leslie Lamport简化文章发表了Paxos Made Simple，这次文中没有一个公式。
但事实如何？大家不妨读一读Paxos Made Simple。Leslie Lamport在文中渐进式地、从零开始推导出了Paxos协议，中间用数学归纳法进行了证明。可能是因为表述顺序的问题，导致这篇文章似乎还是不好理解。
于是，基于此背景，本文根据Paxos Made Simple，重新描述Paxos协议，提供两种证明方法，给出常见的理解误区。期望读者通过阅读本文，再结合Paxos Made Simple，就可以深入理解基本的Paxos协议理论。
基本概念
注意，提议跟提议的值是有区别的，后面会具体说明。协议中Proposer有两个行为，一个是向Acceptor发Prepare请求，另一个是向Acceptor发Accept请求；Acceptor则根据协议规则，对Proposer的请求作出应答；最后Learner可以根据Acceptor的状态，学习最终被确定的值。
方便讨论，在本文中，记{n，v}为提议编号为n，提议的值为v的提议，记(m，{n，v})为承诺了Prepare（m）请求，并接受了提议{n，v}。
协议过程
第一阶段A
Proposer选择一个提议编号n，向所有的Acceptor广播Prepare（n）请求。
第一阶段B
Acceptor接收到Prepare（n）请求，若提议编号n比之前接收的Prepare请求都要大，则承诺将不会接收提议编号比n小的提议，并且带上之前Accept的提议中编号小于n的最大的提议，否则不予理会。
第二阶段A
Proposer得到了多数Acceptor的承诺后，如果没有发现有一个Acceptor接受过一个值，那么向所有的Acceptor发起自己的值和提议编号n，否则，从所有接受过的值中选择对应的提议编号最大的，作为提议的值，提议编号仍然为n。
第二阶段B
Acceptor接收到提议后，如果该提议编号不违反自己做过的承诺，则接受该提议。
需要注意的是，Proposer发出Prepare（n）请求后，得到多数派的应答，然后可以随便再选择一个多数派广播Accept请求，而不一定要将Accept请求发给有应答的Acceptor，这是常见的Paxos理解误区。
小结
上面的图例中，P1广播了Prepare请求，但是给A3的丢失，不过A1、A2成功返回了，即该Prepare请求得到多数派的应答，然后它可以广播Accept请求，但是给A1的丢了，不过A2，A3成功接受了这个提议。因为这个提议被多数派（A2，A3形成多数派）接受，我们称被多数派接受的提议对应的值被Chosen。
三个Acceptor之前都没有接受过Accept请求，所以不用返回接受过的提议，但是如果接受过提议，则根据第一阶段B，要带上之前Accept的提议中编号小于n的最大的提议。
Proposer广播Prepare请求之后，收到了A1和A2的应答，应答中携带了它们之前接受过的{n1, v1}和{n2, v2}，Proposer则根据n1，n2的大小关系，选择较大的那个提议对应的值，比如n1 > n2，那么就选择v1作为提议的值，最后它向Acceptor广播提议{n, v1}。
Paxos协议最终解决什么问题？
当一个提议被多数派接受后，这个提议对应的值被Chosen（选定），一旦有一个值被Chosen，那么只要按照协议的规则继续交互，后续被Chosen的值都是同一个值，也就是这个Chosen值的一致性问题。
协议证明
上文就是基本Paxos协议的全部内容，其实是一个非常确定的数学问题。下面用数学语言表达，进而用严谨的数学语言加以证明。
Paxos原命题
如果一个提议｛n0，v0｝被大多数Acceptor接受，那么不存在提议｛n1，v1｝被大多数Acceptor接受，其中n0
Paxos原命题加强
如果一个提议｛n0，v0｝被大多数Acceptor接受，那么不存在Acceptor接受提议｛n1，v1｝，其中n0
Paxos原命题进一步加强
如果一个提议｛n0，v0｝被大多数Acceptor接受，那么不存在Proposer发出提议｛n1，v1｝，其中n0
如果“Paxos原命题进一步加强”成立，那么“Paxos原命题”显然成立。下面我们通过证明“Paxos原命题进一步加强”，从而证明“Paxos原命题”。论文中是使用数学归纳法进行证明的，这里用比较紧凑的语言重新表述证明过程。
归纳法证明
假设，提议｛m，v｝（简称提议m）被多数派接受，那么提议m到n（如果存在）对应的值都为v，其中n不小于m。
这里对n进行归纳假设，当n = m时，结论显然成立。
设n = k时结论成立，即如果提议｛m，v｝被多数派接受，
那么提议m到k对应的值都为v，其中k不小于m。
当n = k+1时，若提议k+1不存在，那么结论成立。
若提议k+1存在，对应的值为v1，
因为提议m已经被多数派接受，又k+1的Prepare被多数派承诺并返回结果。
基于两个多数派必有交集，易知提议k+1的第一阶段B有带提议回来。
那么v1是从返回的提议中选出来的，不妨设这个值是选自提议｛t，v1｝。
根据第二阶段B，因为t是返回的提议中编号最大，所以t >= m。
又由第一阶段A，知道t
即有v1 = v。所以由n = k结论成立，可以推出n = k+1成立。
于是对于任意的提议编号不小于m的提议n，对应的值都为v。
所以命题成立。
反证法证明
