A-A+

Basic Paxos证明

2016年09月15日 分布式系统 暂无评论 阅读 253 次
摘要:

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。

prof

因为 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\Box,使得M= D\Box

考察M(即 D\Box):

(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} = -\inftyB_{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对于b \sim v_{dec}之间的accept request不能再vote了,所以要持久化b

2. 持久化v,包括v的decree和user value。

 

给我留言