2022.6.29 by zz
【后文方括号内为译者注】
Paxos 论文的原始论文 The Part-Time Parliament 在正文中大量使用隐喻，有比较多模糊的描述，真正精确对算法的描述实际上是放在了论文的附录证明中。
原文：http://lamport.azurewebsites.net/pubs/lamport-paxos.pdf
一个还不错的不包含附录证明部分的论文翻译：https://ying-zhang.github.io/dist/1989-paxos-cn/
译文
证明 Synodic 协议的一致性（consistency）
A1 基础协议（basic protocol）
Synod 基础协议在2.3节非正式的描述，这里使用现代算法符号表达。我们从讨论一个牧师 p 必须维护的变量开始。首先是一些变量，表示他需要记在账本(ledger)上的信息。（方便起见， 投票 prevVote[p] 被替换为其组件 prevBal[p] 和 prevDec [p].）【记在账本 是 记录可靠不能丢的含义，记在纸片 是 记录可以一次性丢失变为初始值，但不能拿到错乱记录的含义】
outcome[p] 法案，写在 p 账本上，或者为 BLACK 如果还什么都没写。
lastTried[p] 数字，上一个p试图开始的ballot，或者为负无穷如果为空
prevBal[p] 数字，上一个p投票过的ballot number，或者为负无穷如果没有投票。
prevDec[p] 法案，上一个p投票过的，或者为BLANK如果p从未投票。
nextBal[p] 数字，上一个p已同意参与的ballot，或者为负无穷如果没有统一参与任何 ballot
接下来的变量表示牧师可以记录在 纸片(slip of paper)上的信息
status[p] 为以下几种值之一：
idle 没有主导或开始一个ballot
trying 尝试开始ballot ，以 lastTried[p]为ballot number
polling 正在主导ballot，以lastTried[p]为ballot number
如果 p 丢失了他的纸条，则status[p] 一定为 idle，且下列4个变量无关。
prevVotes[p] 在当前ballot中收到的LastVote 消息中 vote 的集合
（ballot 号为 lastTried[p]）
quorum[p] 如果 status[p] == polling，为当前ballot构成quorum的牧师集合；否则无意义
voters[p] 如果 status[p] == polling，为当前ballot下p接收过 Voted 消息的quorum成员；否则无意义
decree[p] 如果 status[p] == polling，为当前ballot的法案，否则无意义
历史变量 BETA【译注，对应原文中的 $\mathcal{B}$，其实是B的手写体，这里用BETA指代】是ballot集合，包含了已启动的ballots 和其进展，也就是哪些牧师投了票。（历史变量是用于开发和证明算法的，但没有真正实现）【BETA 不是任意节点可以观察到的量，而是一个理论上的全局状态信息，】
接下来是牧师 p 可能才去的行动。这些行动被假设是原子的，这意味着一个action开始后，必须在p的其他action开始前结束。一个action被描述为一个enable condition和一个effects list。enable condition描述了当一个信使带着消息到达；一些action在接受合适的消息后就可以被enable。effect list描述了action如何改变算法的变量，以及会发出哪些消息。（每个独立action会发出最多一个消息）
回顾 ballot numbers 会随着牧师个体而分片，对于任意ballot number b。Paxons 定义了 owner(b) 作为允许使用这个ballot number的牧师。
action 在基础协议中是个允许 action ; 协议并不要求牧师做任何事。没有尝试提高效率；actions 允许 p 做愚蠢的事情，如发送另一个 BeginBallot 消息给一个已经收到过期LastVote消息的牧师
Try New Ballot
always enabled
- 设置 lastTried[p] 为任意 ballot number b，大于其之前的值，使得 owner(b) = p
- 设置 status[p] 为 trying
- 设置 prevVotes[p] 为 ∅
Send NextBallot Message
enable whenever status[p] = trying
- 发送一个 NextBallot（lastTried[p]） 消息给任意牧师
Receive NextBallot(b) Message
If b >= nextBal[p] then
- 设置 nextBal[p] 为 b
Send LastVote Message
enable whenever nextBal[p] > prevBal[p].
发送一个 LastVote(nextBal[p], v） 消息给 牧师 owner(nextBal[p])，
- v.pst = p
- v.bal = prevBal[p]
- v.dec = prevDec[p]
Receive LastVote(b, v) Message
if b = lastTried[p] and status[p] = trying, then
- 设置 prevVotes[p] 为 原始值 和 {v} 的并集
Start Polling Majority Set Q
enable when status[p] = trying and Q ⊆ {v.pst : v ∈ prevVotes[p]}, 且Q是个多数集【这里的多数指的是按照牧师（或者进程）数量的多数，任意一个多数牧师集合都可以看做Q，牧师和进程缩写都是 p】
- 设置 status[p] 为 polling
- 设置 quorum[p] 为 Q
- 设置 voters[p] 为 ∅
设置 decree[p] ，用以下方式选择一个 decree d :
- 设 v 是 prevVotes[p] 的最大元素
- 如果 v.bal != 负无穷 则 d = v.dec，否则 d 可以等于任意 decree
设置 BETA 为 其之前值和 {B} 的并集
- B.dec = d
- B.qrm = Q
- B.vot = ∅
- B.bal = lastTried [p]
Send BeginBallot Message
enabled when status[p] == polling.
- 发送 BeginBallot(lastTried[p], decree[p]) 消息到任意在 quorum[p] 集合中的 牧师
Receive BeginBallot(b, d) Message
if b == nextBal[p] > prevBal[p] then
- 设置 prevBal[p] 为 b
- 设置 prevDev[p] 为 d
- 如果 一个 ballot B 在 BETA 中 且 B.bal = b （会存在）, 则 选择任意 B （会存在唯一一个）并 设置BETA 中 B.vot 为 其旧值 和 {p} 的并集【建议看原文中前面章节的图示理解 BETA 的修改】
Send Voted Message
enable whenever prevBal[p] != -∞
- 发送一个 Voted(prevBal[p], p) 消息给 owner(prevBal[p])
Receive Voted(b, q) Message
if b = lastTried[p] and status[p] == polling, then
- 设置 voters [p] 为 其旧值 和 {q} 的并集
Succeed
enable whenever status[p] == polling, quorum[p] ⊆ voters[p], and outcome[p] =
blank.
- 设置 outcome[p] 为 decree [p]
Send Success Message
enable whenever outcome[p] != BLACK
- 发送一个 Success(outcome[p]) 消息给任意牧师
Receive Success(d) Message
if outcome[p] == BLANK, then
- 设置 outcom[p] 为 d
这个算法是一个Paxon 牧师实际使用协议的抽象描述。是否这个算法的 actions 精确的建模了实际的牧师？这里有三种类型的action 牧师可以“原子的”执行：接收消息，写一个 note 【对应到纸片上的记录】 或 ledger 项，以及发送一个消息。每个都有单个action表达，除了接受action同时设置了一个变量。我们可以假装接受消息在牧师依据消息行动时发生；如果他在行动前离开了大厅，可以看做消息从未被接收。因为这种看法不影响一致性条件，我们可以基于算法的一致性推断出synod 协议的一致性。
A2 Proof of Consistency
【补充前文的 B1B2B3，Theorem1，Theorem2 。Theorem1 说明了法令决策的安全性（quorum投票的值的不会在改变），Theorem2 说明了活性（不会死锁，更大的ballot number可以推动解析继续）】：
$\begin{array}{l} B 1(\mathcal{B}) \triangleq \forall B, B^{\prime} \in \mathcal{B}: B \neq B^{\prime} \Rightarrow(B_{b a l} \neq B_{b a l}^{\prime}) \\ B 2(\mathcal{B}) \triangleq \forall B, B^{\prime} \in \mathcal{B}: B_{\text {qrm }} \cap B_{\text {qrm }}^{\prime} \neq \emptyset \\ B 3(\mathcal{B}) \triangleq \forall B \in \mathcal{B}:MaxVote(B_{b a l},B_{\text {qrm }}, \mathcal{B})_{b a l} \neq-\infty) \Rightarrow \\ \qquad \qquad \qquad \qquad \qquad (B_{\text {dec }}=\operatorname{Max} \operatorname{Vote}(B_{b a l}, B_{q r m}, \mathcal{B})_{\text {dec }}) \end{array}$
$\begin{array}{l} T{\scriptsize HEOREM \Large } \ 1.\ \ If\ B 1(\mathcal{B}),\ B 2(\mathcal{B}) ,\ and\ B 3(\mathcal{B})\ hold,\ the\\ \qquad \left(\left(B_{q r m} \subseteq B_{v o t}\right) \wedge\left(B_{q r m}^{\prime} \subseteq B_{v o t}^{\prime}\right)\right) \Rightarrow\left(B_{d e c}^{\prime}=B_{d e c}\right) \end{array}$
$\begin{array}{l} T{\scriptsize HEOREM \Large }\text { 2. Let b be a ballot number and Q a set of priests such that } \\ b>B_{bal}\text { and }Q \cap B_{\text {qrm }} \neq \emptyset\text { for all } B \in \mathcal{B} . If\, B 1(\mathcal{B}),\, B 2(\mathcal{B}) ,\, and\, B 3(\mathcal{B}) \text { hold,} \\ \text { then there is a ballot }B^{\prime}\text{ with }B_{bal}^{\prime}=b\text{ and }B_{qrm }^{\prime}=B_{vot }^{\prime}=Q\text{ such that }\\ B1(\mathcal{B} \cup\{B^{\prime}\}), B2(\mathcal{B} \cup\{B^{\prime}\}) ,\text{ and }B3(\mathcal{B} \cup\{B^{\prime}\})\text{ hold}. \end{array}$
为了证明一致性条件，需要说明当 outcome[p] 和 outcome [q] 同时不为 BLANK 时是相等的。一个严格的正确性证明需要完整描述算法。上面的描述已经大部分完成。缺失的变量 MU 【原文实际上是手写体M，也就是 $\mathcal{M}$】是个 所有传递中消息的 multiset (注：multiset指不去重的set)。每个 Send action 增加了一个消息到这个 multiset，每个 Receive action 删除一个。 同时也需要action表达消息的丢失和重复。同时，Forget action 表示牧师丢失了他的纸片。
加上这些之后，我们得到了一个定义了多种可能行为的算法，其中每个状态变化对应于一个允许发生的action。Paxons 证明正确性通过找到一个谓词 I ：
（1）I 初始化时为true
（2）I 包含了需要的正确性条件
（3）每个 action 保持 I 仍然为 true
谓词 I 写成 连接式(conjunction)【连接式(conjunction) 由 多个 连词(conjuct) 合取组成，本文中连词更像是个“可判断真假的独立谓词”的概念，连接式则是多个谓词的合取。后续证明过程是先证明每个action 不会证伪一个具体的连词，然后说明整个连接式不会被证伪，最后连接式不变量满足协议要解决的问题】的模式，I1∧. . .∧ I7。 I1 - I5 依次是每个牧师 p 的连接式 I1(p) - I5 (p) 。虽然多数变量在多个连词(conjuct)中提到，除了 status[p] 外每个变量自然的关联到单个连接词，并且每个连接词可以看做一个对其关联变量的约束。每个I连接词的定义分别在下面给出，用 ∧ 连接的列表给出了这些项目的连接式表示。连词相关变量列在了括号注释中。
I1
【outcome 为确定的法案，outcome 存在 则 存在一轮 ballot 满足投票 quorum 覆盖，且值为 outcome 。invariant 对应到第三阶段通信】
$\begin{array}{l} I 1(p) \triangleq \quad \text { [Associated variable: outcome }[p] \text { ] }\\ \qquad (\text { outcome }[p] \neq \text { BLANK }) \Rightarrow \exists B \in \mathcal{B}:\left(B_{\text {qrm }} \subseteq B_{\text {vot }}\right) \wedge\left(B_{\text {dec }}=\text { outcome }[p]\right)\\ \end{array}$
I2
【lastTried 是指 p Try New Ballot 的最大 ballot number，
任意 BETA 中属于 p 的 ballot B 都 小于等于 lastTried 且 如果p处于 trying 状态（还没加新的 B 到BETA中）则B.bal 小于 lastTried。invariant 对应到第一阶段通信】
$\begin{array}{l} I 2(p) \triangleq \quad \text { [Associated variable: lastTried }[p] \text { ] }\\ \qquad \wedge \text { owner }(\text { lastTried }[p])=p\\ \qquad \wedge \forall B \in \mathcal{B}:\left(\operatorname{owner}\left(B_{b a l}\right)=p\right) \Rightarrow\\ \quad \quad \quad \quad \quad \quad \quad \quad \wedge B_{\text {bal }} \leq \text { lastTried }[p]\\ \quad \quad \quad \quad \quad \quad \quad \quad \wedge(\operatorname{status}[p]=\operatorname{trying}) \Rightarrow\left(B_{b a l}<\text { lastTried }[p]\right) \end{array}$
I3
【prevBal 为 p 已投票的最大 ballot number，prevDec 为 p 已投票的最大值，nextBal 为已同意参与的最大 ballot number, 这里是想说明 MaxVote 对于 p 永远保持拿到最大的ballot 对应 vote。同时p已同意的ballot大于等于自己用于投票的ballot。对应到第一/二阶段通信被动方】
$\begin{array}{l} I 3(p) \triangleq \quad[\text { Associated variables: } \operatorname{prevBal}[p] \text {, prevDec }[p], \operatorname{nextBal}[p]]\\ \qquad \wedge \operatorname{prevBal}[p]=\operatorname{Max} \operatorname{Vote}(\infty, p, \mathcal{B})_{b a l}\\ \qquad \wedge \operatorname{prevDec}[p]=\operatorname{Max} \operatorname{Vote}(\infty, p, \mathcal{B})_{\mathrm{dec}}\\ \qquad \wedge \operatorname{nextBal}[p] \geq \operatorname{prevBal}[p]\\ \end{array}$
I4
【prevVotes 指 trying 过程收集到的 vote 列表，I4 想说明在非idle情况下，p 收集到的 preVote[p] 一定是vote对应 牧师 在 lastTried[p] 值上的 MaxVote，且 vote 对应牧师已同意的 ballot number >= lastTried[p] （因为已经收集到其返回之前的 vote）。对应到第二阶段通信主动方】
$\begin{array}{l} I 4(p) \triangleq \quad \text { [Associated variable: prevVotes }[p]]\\ \qquad (\text { status }[p] \neq i d l e) \Rightarrow\\ \qquad \qquad \forall v \in \operatorname{prevVotes}[p]: \wedge v=\operatorname{Max} \operatorname{Vote}\left(\text { lastTried }[p], v_{p s t}, \mathcal{B}\right)\\ \qquad \qquad \qquad \qquad \qquad \qquad \wedge \operatorname{nextBal}\left[v_{p s t}\right] \geq \text { last Tried }[p]\\ \end{array}$
I5
【如果状态为 polling，则法定集被包含于 preVote中 p的集合 且 存在 B 属于 BETA （因为 start polling 会初始化这些为唯一的B）。对应第二阶段的开始。】
$\begin{array}{l} I 5(p) \triangleq \quad \text { [Associated variables: quorum }[p] \text {, voters }[p] \text {, decree }[p]]\\ \qquad (\text { status }[p]=\text { polling }) \Rightarrow\\ \qquad \qquad \wedge \text { quorum }[p] \subseteq\left\{v_{p s t}: v \in \text { prevVotes }[p]\right\}\\ \qquad \qquad \wedge \exists B \in \mathcal{B}: \wedge \text { quorum }[p]=B_{\text {qrm }}\\ \qquad \qquad \qquad \qquad \wedge \operatorname{decree}[p]=B_{\text {dec }}\\ \qquad \qquad \qquad \qquad \wedge \text { voters }[p] \subseteq B_{\text {vot }}\\ \qquad \qquad \qquad \qquad \wedge \text { lastTried }[p]=B_{b a l}\\ \end{array}$
I6
【对应全局投票轮次状态BETA的演进。BETA 演进满足的 轮次不重叠(B.bal 唯一)，多轮法定集交错，法定集MaxVote确定后在之后的ballot轮次中法定集MaxVote不变，同时对于任意 B 用多数派选择法定集。】
$\begin{array}{l} I 6 \triangleq \quad \text { [Associated variable: } \mathcal{B} \text { ] }\\ \qquad \wedge B 1(\mathcal{B}) \wedge B 2(\mathcal{B}) \wedge B 3(\mathcal{B})\\ \qquad \wedge \forall B \in \mathcal{B}: B_{\text {qrm }} \text { is a majority set }\\ \end{array}$
I7
【对应全局消息队列状态MU的演进。
NextBallot(b) 消息的b小于等于其owner的 lastTried。
LastVote(b,v) 消息保证 v 稳定为 MaxVote(b,v.pst. BETA) 且 nextBal 大于b。
BeginBallot(b,d) 消息保证 BETA 创建了一个 B 有固定的 b，d 值
Voted(b,p) 消息保证对应B 上 p 属于 B.vot（注意voted消息发出时在发出端牧师上持久化，就已经属于B.vot，无需主动方接收）
Success(d) 消息保证存在 p 上outcome值为 d
】
$\begin{array}{l} I 7 \triangleq \quad \text { [Associated variable: } \mathcal{M} \text { ] }\\ \qquad \wedge \forall \operatorname{NextBallot}(b) \in \mathcal{M}:(b \leq \text { lastTried }[\text { owner }(b)])\\ \qquad \wedge \forall \operatorname{LastVote}(b, v) \in \mathcal{M}: \wedge v=\operatorname{MaxVote}\left(b, v_{pst}, \mathcal{B}\right)\\ \qquad \qquad \qquad \qquad \qquad \qquad \wedge \operatorname{nextBal}\left[v_{p s t}\right] \geq b\\ \qquad \wedge \forall \operatorname{BeginBallot}(b, d) \in \mathcal{M}: \exists B \in \mathcal{B}:\left(B_{b a l}=b\right) \wedge\left(B_{\text {dec }}=d\right)\\ \qquad \wedge \forall \operatorname{Voted}(b, p) \in \mathcal{M}: \exists B \in \mathcal{B}:\left(B_{b a l}=b\right) \wedge\left(p \in B_{\text {vot }}\right)\\ \qquad \wedge \forall \operatorname{Success}(d) \in \mathcal{M}: \exists p: \text { outcome }[p]=d \neq \text { BLANK } \end{array}$
【不变量证明前言】
Paxons 必须证明 I 满足上面的三个条件。第一个条件，I 初始化，需要检查对于初始变量每个连词是true。虽然没有明确的说明，这些初始值可以从变量的描述中判断，校验也是直接 (straightforward) 的。第二个条件，I 表明一致性，从 I1本身， I6 的第一个连词，和 Theorem 1 可以一起给出。
难的部分在于证明第三个条件，I 的不变性，意味着任意action后I仍然为true。证明方法为对于每个 I 的连词，执行当I为true时，任意 action 过后 I 中的连词为true。证明框架见下。
I1(p)
BETA 的变化只发生在增加新 ballot 【start polling】或者增加新牧师到 B.vot 【 Receive begin ballot 】，这两个都不能将 I1(p) false 化。outcome[p] 只在Succeed 和 Receive Success Message 两个action上变化。对应 enable condition 和 I5(p) 蕴含（implies）了 I1(p) 在 Succeed action 后保持 true。对应 enable condition ， I1(p) 和i7(p)最后的连词说明了 I1(p) 在 Receive Success Message action 后保持 true.
I2(p)
这个连词依赖 lastTried[p], status[p], 和 BETA。只有 Try New Ballot 修改 lastTried[p]，并且只有那个action能设置 status[p] 为 trying。 因为这个action增加lastTried[p] 到一个值 b 且 owner(b) = p，其保持 I2(p) 为 true。只有在 Start Polling是会加一个全新的元素到 BETA 中；I2(p) 的首个连词和这个action规格蕴含了增加新元素不会证伪I2(p)第二个连词。BETA 另外的变化方法为增加新牧师到B.vot （for some B ∈ BETA），也不会影响 I2(p)
I3(p)
因为投票不会从 BETA 中删除，修改 MaxVote(∞, p, B) 的唯一办法是增加 p 的一个投票到BETA中，只有Receive Begin Ballot Message可以做到，并且只有那个action修改 prevBal [p] 和 prevDec[p]。BeginBallot 和 I7 蕴含了这个action确实增加了一个vote到BETA中，并且B1(BETA) （I6 的首个连词）蕴含了这个vote 只有唯一一个ballot可以加进去。这个enable condition， I3 的假设，和MaxVote 定义蕴含了这个action会保持 I3(p) 的前两个连词为true。第三个连词也保持true，因为 prevBal [p] 只会被设置成 nextBal [p] 而修改, 且 nextBal [p] 从不减少。
I4(p)
这个连词依赖几个变量 status[p], prevVotes[p], lastTried[p], 一些牧师 q的 nextBal[q], 以及 BETA. status[p] 的值从 idle 到非 idle 变化只可能由 Try New Ballot action 导致，该action设置 prevVotes[p] 为 ∅，使 I4(p) 空真（vacuously true） 。唯一可以修改 prevVotes[p] 的 action 是 Forget action，其保持 I4(p) 为true，因为设置 status[p] 为 idle。另一个是 Receive LastVote Message action 。根据其 enable condition 和I7的 LastVote 连词， Receive LastVote Message action 保持了 I4(p)。lastTried[p] 只会随 Try New Ballot action 变化，其会保持 I4(p) true 因为设置 status[p] 为 trying。nextBal[q] 的值只能增加，不会导致I4(p) 为false。最后MaxVote(lastTried[p], v.pst , BETA) 只会在 v.pst 加到 B.vote 时发生，B ∈ BETA 且 B.bal < lastTried[p].但 v.pst 增加到B.vot （随 Receive BeginBallot Message action）只可能因为 nextBal [v.pst] = B.bal，这种场景下 I4(p) 蕴含了 B.bal ≥ lastTried[p].
I5(p)
status[p] 被设置为 polling 只可能由 Start Polling action 导致。这个action 的 enable condition保证了首个连词为true，并且其增加这个ballot 到 BETA 使得第二个连词为 true。没有其他 action 会修改quorum[p], decree[p], 或 lastTried[p] 同时保持 status[p] 为 polling. prevVotes[p] 的值不会在 status[p] = polling 时改变，且 BETA 的变化只在增加新元素或增加新牧师到B.vot 时。唯一遗留的证伪 I5(p) 的可能性是随 Receive Voted Message action 增加新元素到 voters[p]。I7 的 Voted 连词，B1(BETA) (I6首个 连词)，和action 的 enable condition 蕴含元素增加到 voters[p] 时一定存在于B.vot，B 是一个 ballot，其存在性在 I5(p) 中断言。
I6
因为B.bal 和 B.qrm 不会因任意 B ∈ BETA 而变化，唯一证伪B1(B), B2(B), I6第二个连词的方法是增加新的 ballot 到 BETA，其只能由Start Polling Majority Set Q 在 status[p] 为 trying 时完成。根据 I2(p) 的第二个连词，这个action保持 B1(BETA)为true；并且这个 enable condition 中的断言，也就是Q is 多数派， 蕴含了这个action保持 B2(BETA) 和 I6 第二连词为true。有两种方法证伪 B3(BETA) ：修改 MaxVote(B.bal, B.qrm, BETA) 随增加新的 vote 到 BETA 或者增加新的 Ballot 到BETA。一个新的 vote 只随 Receive BeginBallot Message action 加入，I3(p) 蕴含了增加 vote 在 任意其他 BETA 中的 p 的 vote 之后，所以不会修改 任意 BETA 中 B 的MaxVote(B.bal, B.qrm, BETA) 。连词I4(p) 蕴含 Start Polling action 增加的新 ballot 不会证伪 B3(B)。
I7
I7 被证伪的条件要么是增加新消息到 MU 或者 修改其他一个I7依赖的变量。因为lastTried[p] and nextBal [p] 从不减少，修改他们不会证伪 I7。因为 outcome[p] 在value不会BLACK时不会再改变，修改其不会证伪 I7。因为 BETA 只在 增加 ballot 或增加 vote 时变化，唯一能导致I7为false的情况是由 v.pst 增加一个 vote，通过修改MaxVote(b, v.pst , BETA) 让 LastVote(b, v) 为false。这只能在v.pst 的 vote 存在 ballot B 中且B.bal < b。但 v.pst 只能在 ballot number nextBal [v.pst ] 上发起vote，且这个连词在初始时的假设蕴含了 nextBal [v.pst] > b。因此，我们只需要检查每个发送的消息满足I7中合适的连词。
NextBallot：根据Send NextBallot Message action 的定义和 I2(p) 首个连词。
LastVote：Send LastVote Message action 的 enable condition 和 I3(p) 蕴含了MaxVote(nextBal [p], p, BETA) = MaxVote(∞, p, BETA)，从中可以得到发出的 LastVote message 满足 I7.
BeginBallot: 根据 I5(p) 和 Send BeginBallot Message action的定义。
Voted: 根据 I3(p), MaxVote 的定义, 和 Send Voted Message action 定义。
Success: 根据 Send Success Message 定义
阅读心得
lamport 早年是数学专业出身，习惯用数学语言描述算法问题。其持续关注并发理论， lamport著作（译者了解过的）涵盖时序，原子寄存器快照，memory order，cpu 原语的并发数，活性/安全性，lockfree/waitfree，分布式系统快照，并发程序证明等等。
lamport 在意识到数学证明缺少时序逻辑之后，推出TLA语言 (TLA: Lamport's Temporal Logic of Actions) ，以及结构化分层证明来严格的描述并发问题。本文采用了TLA风格描述证明。
- 文中提到的 paxos 岛上的数学家不用自然语言证明 对应 本文的 TLA 分层证明。
- 其倾向不愿意将证明逻辑中的变量带上类型表示，丰富的隐喻，以及用手写体区分不同变量等奇葩命名方法，使得阅读证明时增加了难度
- 数学证明和程序逐步推导不同，数学证明在一开始所有状态空间均已存在，后续的操作只是证明某些状态不可达的过程。
其早年论文 Time, Clocks, and the Ordering of Events ina Distributed System 给出了分布式系统事件全排序的办法，是 state + action + invariant 的 状态机 方法可以严格的分析一个并发分布式系统的正确性的基础。happened before 基础上的全序摒弃了现实世界的“相对论”效应。隐式信道也是讨论 paxos 读的理论基础。
- 文中 BETA 量就是一个不能用计算机通信手段观测，（但足够 "well define"）可以作为状态机演进推理基础的全局状态。
- Lynch 的 FLP 定理是 本文提出 法定集(quorum) 概念(在多轮之间进程必须至少一个相交)的思想基础。
- 三阶段提交， 也就是 两阶段提交 的活性改进版本，是本文提出三阶段 Synod （也就是 basic paxos）算法保证活性的思想基础。
- 自稳定系统概念，是本文处理拜占庭类错误的基础。
lamport 提出的 安全性，活性 概念是构造和证明并发算法主要关注点，本文也是先描述了这两点。
- 通常在实际业务中，安全性没了会导致数据持续不一致，也就是丢失和损坏。活性没了会导致卡死，需要运维手段介入处理
- 文中提到当指定一个死去的节点为唯一成员后，后续走向军事独裁，说明 paxos 算法本身需要一些外部强制手段协助恢复协议状态。
状态机方法（state + action + invariant）证明分布式系统通信问题的建模思路主要是
- 确定每个进程状态，包含可靠(持久化)状态，临时(可以丢失)状态，可欺骗（可以任意变化）状态。
- 用消息 multiset M 表示网络中的消息集合，M 上的action 允许丢包，重复等
- 每个进程 的 action 要么是改变自己状态，要么是和 M 中的消息交互
给出 invariant 并证明随着系统的演进，invariant不会改变。
- 实际上在思考算法时会先从 invariant 出发来给出 action
并发分析与设计的通用方法：给出状态机初始状态，用搜索的方式演进状态 并 注意状态演进过程的原子性（需要特别注意每一步状态变化中其余状态保持不变，否则就不是原子的），最后对可演进状态进行分类归纳，得出一个封闭的状态分类集合，在这个状态分类集合下每一类状态都不会打破 invariant。同时关注演进过程满足业务所需安全性和活性, 以及关注可能面临的的 Process fail，Process hang ，Message duplicate，Message lost，Message reorder 等异常 action。
- 设计消息遵循幂等原则。设计状态关注“可安全演进”。
TLA 只能单纯搜索，没法做到给不同的状态演进分类归纳，其实导致了 TLA 不能完美证明，不实用。
- 这个缺陷对应到本文不变量证明部分，那部分偏自然语言，也较为散乱
- 当然更严重的问题是TLA模型与实际生产代码分离，以及真正能用明白TLA的人有能力不依赖TLA分析绝大多数现实的并发问题，并简单基于乐观锁实现。
- 似乎历史上的 MaxCompute 元数据 同学分析各类并发问题使用了同样的方法（定义状态，定义不变量，穷举 各类DDL/DML 作为 action，发现问题后改进 DDL/DML 操作设计），但在证明上不够形式化，仅限于“说明”，但其强度不弱于文中不变量证明部分。
总之，paxos 算法本质是一个综合 TimeOrdering 理论（分布式系统所处世界模型） + 三阶段提交（解决活性和一致性） + FLP（给出多节点同质副本下法定集概念）+ 状态机方法（TLA并发程序证明） 而给出的一个更加泛化的 两阶段提交 算法，解决了多节点复制时外部一致性问题。
