A-A+

Basic Paxos证明

2016年09月15日分布式评论 1 条阅读 1,151 次

摘要：

Basic Paxos协议的证明过程

为什么Paxos三条约束下，就可以保证一致？The Part Time Parliament论文

约束

约束1：

$B1(\mathcal{B}) \triangleq \forall B, B^{'} \in \mathcal{B} : (B \neq B^{'}) \Rightarrow (B_{bal} \neq B_{bal}^{'})$

约束2：

$B2(\mathcal{B}) \triangleq \forall B, B^{'} \in \mathcal{B} : B_{qrm} \cap B_{qrm}^{'} \neq \emptyset$

约束3：

$B3(\mathcal{B}) \triangleq \forall B \in \mathcal{B} : (MaxVote(B_{bal}, B_{qrm}, \mathcal{B})_{bal} \neq -\infty) \Rightarrow (B_{dec} = MaxVote(B_{bal}, B_{qrm}, \mathcal{B})_{dec})$

引理

如果 $B1(\mathcal{B})$ , $B2(\mathcal{B})$ , $B3(\mathcal{B})$ 三个约束成立，那么

$((B_{qrm} \subseteq B_{vot}) \land (B_{bal}^{'} > B_{bal})) \Rightarrow (B_{dec}^{'} = B_{dec})$

证明：

对于 $\mathcal{B}$ 中的任何一个ballot B，定义 $\Psi(B,\mathcal{B})$ 为 $\mathcal{B}$ 中比B的bal大且dec不等于B的ballot:

$\Psi(B,\mathcal{B}) \triangleq \{ B^{'} \in \mathcal{B} : (B_{bal}^{'} > B_{bal}) \land (B_{dec}^{'} \neq B_{dec})\}$

引理的条件表示B是一个成功的ballot。假设后续有ballot的bal更大，但是dec不等于这个成功的ballot的dec，即 $\Psi(B,\mathcal{B})\neq \emptyset$ 。下面我们用反证法。

取 $\Psi(B,\mathcal{B})$ 中bal最小的元素，设为C。

因为 $B2(\mathcal{B})$ ，所以有 $\exists B\triangle\in (C_{qrm} \cap B_{vot})$ 。

记vote $M \triangleq MaxVote(C_{bal}, C_{qrm}, \mathcal{B})$ 。由于 $B\triangle$ 这个vote存在，所以 $B\triangle$ 是M在取max时的元素之一。因为 $C_{dec} \neq B_{dec}$ ，所以vote M与vote $B\triangle$ 不是同一个vote。因此， $M_{bal} > B_{bal}$ 并且 $M_{dec} = C_{dec} \neq B_{dec}$ 。那么，就一定存在另一个vote $D\square$ ，使得M= $D\square$ 。

考察M（即 $D\square$ ）:

$(M_{bal}>B_{bal}) \land M_{dec} \neq B_{dec}$

所以 $M \in \Psi(B,\mathcal{B})$

又， $M_{bal} < C_{bal}$ ，所以M是 $\Psi(B,\mathcal{B})$ 中比C还要小的元素，这跟C的定义矛盾。因此不存在这样的C。

THEOREM 1

如果 $B1(\mathcal{B})$ , $B2(\mathcal{B})$ , $B3(\mathcal{B})$ 三个约束成立，那么，

$((B_{qrm} \subseteq B_{vot}) \land (B_{qrm}^{'} \subseteq B_{vot}^{'} \Rightarrow (B_{dec}^{'} = B_{dec}))$

证明：

如果 $B_{bal}=B_{bal}^{'}$ ，那么根据 $B1(\mathcal{B})$ ，结论是平凡的。

如果 $B_{bal}\neq B_{bal}^{'}$ ，则根据引理显然成立。

THEOREM 2

设b是一个ballot number，Q是priest集合，满足条件： $\forall B \in \mathcal{B}, b > B_{bal} \land Q \cap B_{qrm} \neq \emptyset$ 。

如果 $B1(\mathcal{B})$ , $B2(\mathcal{B})$ , $B3(\mathcal{B})$ 成立，那么，存在一个新的ballot $B^{'}$ ， $B_{bal}^{'} = b \land B_{qrm}^{'} = B_{vot}^{'} = Q$ ，使得加上这个 $B^{'}$ 之后的 $\mathcal{B}$ ，仍然保持三个约束 $B1(\mathcal{B}\cup B^{'})$ , $B2(\mathcal{B}\cup B^{'})$ , $B3\mathcal{B}\cup B^{'})$ 成立。

证明：

要证明 $B^{'}$ 存在性，构造一个 $B^{'}$ 即可：

如果 $MaxVote(b, Q, \mathcal{B})_{bal} = -\infty$ ， $B_{dec}^{'}$ 取任意值，否则取 $MaxVote(b, Q, \mathcal{B})_{dec}$

这个证明过程也表明了为什么Paxos需要prepare和accept两个阶段，因为要保持一致性，proposer就必须先得到 $MaxVote(b, Q, \mathcal{B})_{dec}$ ，然后拿这个值来发起accept请求。同时，也指明了acceptor收到prepare请求时要做哪些承诺来保持一致性。

acceptor q要持久化如下两项内容：

1. 有proposer要获得 $MaxVote(b, Q, \mathcal{B})$ , $q \in Q$ ，acceptor q在回应了该proposer response=" $MaxVote(b, q,\mathcal{B})=Vote\ v$ "之后，需要确保q对于 $v_{dec} \sim b$ 之间的accept request不能再vote了，所以要持久化 $b$ 。