摘要：通过对Basic Paxos的重新审视，发现Lamport在算法中对预提议（prepare请求）和提议（accept请求）所作出的一系列要求实质是在提议之间建立了某种happens-before关系，以保证在异步环境下能够满足共识值的唯一性。
回顾Paxos需要满足的条件
安全性条件（safety）：
- 只能选择被提议（propose）的值
- 只有一个值会被选中（不存在某个时刻某个值被选中后，另一个时刻又选中了另外不同的值）
- 只有当某个值被选中后，才能被其他进程学习到
活性条件（liveness）：
- 保证最终能选中一个值 （FLP证明了在异步环境下有一定概率“活锁”）
通信模型条件：
- 异步（允许延迟、消息丢失、重复）、非拜占庭模型
Quorum条件：
- 被大多数接收者所接收的值被视为选中
如何保证满足唯一性（以下推导和Lamport原文略有不同，但使用到的推论几乎相同）
提议以{ID, value}的形式发起，[R1] 每个接收者必须接受收到的第一个提议（没理由拒绝）
假设提议{m, v1}首先被选中，接着提议{n, v2}被选中，要满足唯一性，必须保证v2 = v1。根据Quorum条件，一定存在某个大多数集合C1接受了提议m，同理存在某个大多数集合C2接受了提议n，C1和C2的交集不可能为空，即至少有一个接收者既接受了提议m，也接受了提议n。由于异步环境下提议的选中顺序取决于哪个提议得接受先满足了Quorum原则，而具体某个接收者接受提议m和n的顺序是不一定的，所以加一个限制: [R2] 接收者如果已经接受过提议，之后只能接受ID更大的提议。在这个限制下，n ＞ m（否则提议m不可能达成Quorum）。
现在要保证v2 = v1，那么提议n在被提议前必须先学习到提议m的值，在异步环境下需要满足2个条件:
- 接受过提议m的接收者，手上的值v1不能被覆盖掉(可以接受ID更大的提议，但值不能变)
- 值v1一定是可以被唯一学习到的
先看条件1，假设条件2成立，那么在提议{m, v1}选中后，任意提议者提议前学习（通过预提议）到的值一定是v1，只要[R3] 让提议者提议时携带学习到的值v1，即可满足。但是，也存在在提议m选中前提议者先学习到值v2，之后提议m才选中的情况，v2和v1可能不同，这种情况直接禁止掉: [R4] 学习的过程也让预提议接受者保证拒绝接受ID ＜ n的提议的承诺，并且提议者只有得到大多数接受者的回复才能发起新的提议。这样，只要提议n发起，就意味着存在一个大多数集合答应拒绝接受ID＜n的提议，提议m只能在预提议n完成前选中，否则是无法达成Quorum的（意味着只要提议m被选中，存在某个多数接受者集合，满足：{提议m被接受} $\rightarrow$ {预提议n被接受}）。因此提议n的值一定是在提议m完成后学习到的，同样，只要条件2满足，条件1就能满足。
再看条件2，学习的过程: [R5] 提议前给某个大多数集合发送预提议，让对方返回“选中”的值。但是这个“选中”的值，对每个接受者而言是不知道的，是个全局概念，根据[R1]，每个接收者可以记录已接受到的ID最大的值。那么提议者收到来自某个大多数集合中所有接受到的ID最大的值后(没接受过提议就返回空值)，怎么从这堆返回值中找出v1？因为只有从中选ID最大/最小的值，才算是“可被学习到的”，那么从中选ID最大的值是否一定等于v1？
提议{m, v1}被选中，必定存在大多数集合C1接受提议m，提议n（n > m）被发起，根据R4，必定存在大多数集合C2接受了预提议n，C1和C2必有交集，且交集中的接收者事件顺序一定满足：{提议m被接受} $\rightarrow$ {预提议n被接受}（否则提议m达不到Quorum），所以预提议n学习到的值一定是m..n-1范围内的某个提议值，如果n = m+1，那么提议n的值一定是v1。另外，对任意被发起的提议m和n（n > m），一定满足：存在某个多数集合，其中{预提议m被接受} $\rightarrow$ {预提议n被接受}（否则预提议m达不到Quorum不会被发起）。根据两个happens-before关系，归纳可得：预提议n学习到的值一定是v1，条件2满足。
Paxos流程
将R1至R5整理，得到Paxos流程：
Phase 1.
(a) 提议者发送预提议{n}给某个大多数接收者集合 [R5]
(b) 接收者记录接受过的最大预提议ID，收到更大ID的预提议后，回复保证不再接受ID < n的提议，并携带接受过的最大ID的提议值 [R2, R4, R5]
Phase 2.
(a) 如果提议者收到来自大多数接收者的预提议回复，那么他将正式向那些接收者发起提议{n, v}，v是所有回复中ID最大的提议值，如果没有值，则v是任意值 [R3, R4]
(b) 如果接收者收到提议n，只要之前没接受过ID > n的预提议，就接受提议n [R1, R2, R4]
总结
R4是整个算法的关键，建立了以下2个关系：
对于任意提议m和提议n（m < n），一旦两个提议都发起，就必定满足：
- 存在一个大多数集合，对任意接受预提议m和n的接收者，{预提议m被接受} $\rightarrow$ {预提议n被接受}
如果提议m被选中，那么关系将收窄成：
- 存在一个大多数集合，对任意接受提议m和预提议n的接收者，{提议m被接受} $\rightarrow$ {预提议n被接受}
关系1和2加上Quorum条件，可以确定（见上面条件2的证明），如果提议{m, v}被选中，那么预提议n学习到的值一定是v（提议n的值是v），这是确保唯一性的根本原因。
其它说明
对提议ID的要求
必须保证提议ID的全局唯一，假设提议{m, v1}被部分接受，提议{m, v2}也被部分接受，两个提议都未被选中，那么新一轮预提议返回有可能会出现同一个最高ID具有两种不同的值，无法决策在正式提议阶段携带哪个值。
除了全局唯一外，对于提议ID的生成并没有要求的，任何提议者可以使用随机的ID，只是由于接收者只能接受比已经收到过的预提议ID更大的提议，因此，随机ID会严重影响提议被拒绝的概率，对于同一个提议者来说，保证提议ID单调增是合理的。进一步，保证各个提议者的ID是全局单调递增的能减少各提议者成功率不均匀的情况，这就可以使用Lamport Clock的方式，由于提议者本身也是接收者，提议者的提议ID可以设为max{local_max_id, highest_recv_id} + 1（不过这个方法并不能满足提议ID相同的要求）。
预提议结果无法判断是否达成共识的问题
在某个提议已经被选中的前提下，之后的预提议必定能学习到被选中的值。然而，存在多个提议（不同ID）被不同的少数接受者接受的情况，这时，预提议会学习到某大多数集合中ID最大的提议值，即通过预提议学习到非空值，提议者无法判断之前是否达成共识，这个可能会在某些场景下引入新的问题。
参考资料：
[1] Lamport, L. 2001. Paxos made simple.