“与其预测将来，不如限度将来”，这应该是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协定实践。

基本概念

  • Proposal Value：提议的值；
  • Proposal Number：提议编号，要求提议编号不能抵触；
  • Proposal：提议 = 提议的值 + 提议编号；
  • Proposer：提议发起者；
  • Acceptor：提议接受者；
  • Learner：提议学习者。

留神，提议跟提议的值是有区别的，前面会具体阐明。协定中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的大小关系，抉择较大的那个提议对应的值，比方n1x > n2，那么就抉择v1作为提议的值，最初它向Acceptor播送提议{n, v1}。

Paxos协定最终解决什么问题？

当一个提议被多数派承受后，这个提议对应的值被Chosen（选定），一旦有一个值被Chosen，那么只有依照协定的规定持续交互，后续被Chosen的值都是同一个值，也就是这个Chosen值的一致性问题。

协定证实

上文就是根本Paxos协定的全部内容，其实是一个十分确定的数学问题。上面用数学语言表达，进而用谨严的数学语言加以证实。

Paxos原命题

如果一个提议｛n0，v0｝被大多数Acceptor承受，那么不存在提议｛n1，v1｝被大多数Acceptor承受，其中n0 < n1，v0 != v1。

Paxos原命题增强

如果一个提议｛n0，v0｝被大多数Acceptor承受，那么不存在Acceptor承受提议｛n1，v1｝，其中n0 < n1，v0 != v1。

Paxos原命题进一步增强

如果一个提议｛n0，v0｝被大多数Acceptor承受，那么不存在Proposer收回提议｛n1，v1｝，其中n0 < n1，v0 != v1。

如果“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 < n。所以依据假如t对应的值为v。

即有v1 = v。所以由n = k论断成立，能够推出n = k+1成立。

于是对于任意的提议编号不小于m的提议n，对应的值都为v。

所以命题成立。

反证法证实

假如存在，无妨设n1是满足条件的最小提议编号。

即存在提议｛n1，v1｝，其中n0 < n1，v0 != v1。-------------（A）

那么提议n0，n0+1，n0+2，...，n1-1对应的值为v0。-------------（B）

因为存在提议｛n1，v1｝，则阐明大多数Acceptor曾经接管n1的Prepare，并承诺将不会承受提议编号比n1小的提议。

又因为｛n0，v0｝被大多数Acceptor承受，

所以存在一个Acceptor既对n1的Prepare进行了承诺，又承受了提议n0。

由协定的第二阶段B知，这个Acceptor先承受了｛n0，v0｝。

所以收回｛n1，v1｝提议的Proposer会从大多数的Acceptor返回中得悉，

至多某个编号不小于n0而且值为v0的提议曾经被承受。-------------（C）

由协定的第二阶段A知，

该Proposer会从曾经被承受的值中抉择一个提议编号最大的，作为提议的值。

由（C）知该提议编号不小于n0，由协定第二阶段B知，该提议编号小于n1，

于是由（B）知v1 == v0，与（A）矛盾。

所以命题成立。

通过下面的证实过程，咱们反过来回味一下协定中的细节。

  • 为什么要被多数派承受？

因为两个多数派之间必有交加，所以Paxos协定个别是2F+1个Acceptor，而后容许最多F个Acceptor停机，而保障协定仍然可能失常进行，最终失去一个确定的值。

  • 为什么须要做一个承诺？

能够保障第二阶段A中Proposer的抉择不会受到将来变动的烦扰。另外，对于一个Acceptor而言，这个承诺决定了它回应提议编号较大的Prepare申请，和承受提议编号较小的Accept申请的先后顺序。

  • 为什么第二阶段A要从返回的协定中抉择一个编号最大的？

这样选出来的提议编号肯定不小于曾经被多数派承受的提议编号，进而能够依据假如失去该提议编号对应的值是Chosen的那个值。

原文的第一阶段B

Acceptor接管到Prepare（n）申请，若提议编号n比之前接管的Prepare申请都要大，则承诺将不会接管提议编号比n小的提议，并且带上之前Accept的提议中编号最大的提议，否则不予理睬。

绝对下面的表白少了“比n小的”，通过邮件向Leslie Lamport求教了这个问题，他示意承受一个提议，蕴含回应了一个Prepare申请。这个有点费解，但也齐全正当，有了这个条件，下面的证实也就通顺了。就是说Acceptor承受过的提议的编号总是不大于承诺过的提议编号，于是能够将这个“比n小的”去掉，在理论工程实际中咱们往往只保留承受过的提议中编号最大的，以及承诺过的Prepare申请编号最大的。

Leslie Lamport也示意在去掉“比n小的”的状况下，就算承受一个提议不蕴含回应一个Prepare申请，最终论断也是对的，因为前者显著能够推导出后者，去掉反而把条件增强了。

如果返回的提议中有编号大于n的，比方{m，v}，那么必定存在多数派承诺回绝小于m的Accept申请，所以提议{n，v}不可能被多数派承受。

学习过程

如果一个提议被少数Acceptor承受，则这个提议对应的值被选定。

一个简略间接的学习办法就是，获取所有Acceptor承受过的提议，而后看哪个提议被少数的Acceptor承受，那么该提议对应的值就是被选定的。

另外，也能够把Learner看作一个Proposer，依据协定流程，发动一个失常的提议，而后看这个提议是否被少数Acceptor承受。

这里强调“一个提议被少数Acceptor承受”，而不是“一个值被少数Acceptor”承受，如果是后者会有什么问题？

提议{3，v3}，{5，v3}别离被B、C承受，即有v3被多数派承受，但不能阐明v3被选定（Chosen），只有提议{7，v1}被多数派（A和C组成）承受，咱们能力说v1被选定，而这个选定的值随着协定持续进行不会扭转。

总结

“与其预测将来，不如限度将来”，这应该是Paxos协定的核心思想。如果你在浏览Paxos的这篇论文时感到困惑，无妨找到“限度”的段落回味一番。Paxos协定自身是比较简单的，如何将Paxos协定工程化，才是真正的难题。

目前在微信外围存储PaxosStore中，每分钟调用Paxos协定过程数十亿次量级，而《微信PaxosStore内存云揭秘：十亿Paxos/分钟的挑战》一文， 则对内存云子系统做了开展。

后续咱们将发表更多的实际计划，包含万亿级别的海量闪存存储，反对单表亿行的NewSQL解决方案，以及有别于业界的开源实现，PaxosStore架构计划基于非租约的Paxos实现等内容。

作者简介

郑建军，微信工程师，目前负责微信根底存储服务，致力于强统一、高可用的大规模分布式存储系统的设计与研发。

本文转自微信后盾团队,如有进犯,请分割咱们立刻删除

OpenIMgithub开源地址：

https://github.com/OpenIMSDK/...

OpenIM官网 ： https://www.rentsoft.cn

OpenIM官方论坛： https://forum.rentsoft.cn/

更多技术文章：

开源OpenIM：高性能、可伸缩、易扩大的即时通讯架构
https://forum.rentsoft.cn/thr...

【OpenIM原创】简略轻松入门 一文解说WebRTC实现1对1音视频通信原理
https://forum.rentsoft.cn/thr...

【OpenIM原创】开源OpenIM：轻量、高效、实时、牢靠、低成本的音讯模型
https://forum.rentsoft.cn/thr...