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