Paxos Note
Hawtian Wang
Contents
0.1 Symbols And Structure
- 表决 $B$A ballot is said to be successful, if every quorum member voted. In math: $$ B_{qrm} \subseteq B_{vot} $$
struct Ballot { dec: Decree, // 表决的内容 vot: Set<Node>, // 表决投票通过的节点 qrm: Set<Node>, // 表决参与的节点 bal: u64, // 表决编号 } - 投票 $v$
struct Vote { pst: Node, // 本投票的节点 bal: u64, // 本投票的表决编号 dec: Decree, // 本投票表决的内容 } - 表决的集合 $\beta$
0.2 Define Some Useful functions
- $Votes(\beta)$：所有在 $\beta$ 中的表决的投票的集合 $$Votes(\beta) = \{v:(v_{pst}\in B_{vot})\cap(v_{bal}=B_{bal}), B \in \beta\}$$
- $Max(b, p, \beta)$：在由节点 $p$ 投给 $\beta$ 中的表决的投票中，编号小与等于 $b$ 的最大投票 $$Max(b, p,\beta)=max\{v \in Votes(\beta):(v_{pst}=p)\land(v_{bal}<b)\}\cup\{null_{p}\}$$
- $MaxVote(b, Q, \beta)$：在集合 $Q$ 中的任意一个节点投给 $\beta$ 中的表决的投票中，编号小于等于 $b$ 的最大投票 $$MaxVote(b,Q,\beta)=max\{v\in Votes(\beta):(v_{pst}\in Q)\cap(v_{val}<b)\}\cup\{null_p\}$$
那么如果条件$B1(\beta)-B3(\beta)$满足的情况下，那么系统将满足一致性，并且是可进展的。
- $B1(\beta) \triangleq \forall B,B’ \in \beta:(B \ne B’) \implies (B_{bal} \ne B’_{bal})$
- $B2(\beta) \triangleq \forall B,B’ \in \beta:B_{qrm}\cap B’_{qrm} \ne \emptyset $
- $B3(\beta) \triangleq \forall B \in \beta: (MaxVote(B_{bal},B_{qrm},\beta)_{bal}\ne - \infty) \implies B_{dec} = MaxVote(B_{bal}, B_{qrm}, \beta)_{dec} $
0.2.1 Lemma 1
如果 $\beta$ 中的表决 $B$ 是成功的，那么 $\beta$ 中更大编号的表决和 $B$ 的表决内容相同。 $$ ((B_{qrm} \subseteq B_{vot})\land(B’_{bal}>B_{bal})) \implies (B’_{dec}=B_{dec}) $$
0.2.2 Proof
定义集合 $\Psi(B, \beta)$: $\Psi(B, \beta) \triangleq \{B’\in \beta:(B’_{bal}>B_{bal})\land(B’_{dec}\ne B_{dec}) \}$，表示 $\beta$ 中编号比 $B$ 大并且表决内容不相同的表决的集合。
- $ C = min\{B’:B’\in \Psi(B, \beta)\} $
- $ C_{bal} < B_{bal} $
- $ C_{qrm} \cap B_{bot} \ne \emptyset $ 因为 $B2$ 和 假设中的 $B$ 表决是成功的，也就是 $ B_{qrm} \subseteq B_{vot} $
- $ MaxVote(C_{bal},C_{qrm},\beta)_{bal} \ge B_{bal} $ 因为 $C_{qrm}$ 和 $B$ 的投票者一定有交集
- $ MaxVote(C_{bal}, C_{qrm}, \beta)\in Votes(\beta)$
- $ MaxVote(C_{bal}, C_{qrm}, \beta)_{dec} = C_{dec} $
- $ MaxVote(C_{bal}, C_{qrm}, \beta)_{dec} \ne B_{dec} $
- $ MaxVote(C_{bal}, C_{qrm}, \beta)_{bal} > B_{bal} $
- $ MaxVote(C_{bal}, C_{qrm}, \beta) \in Votes(\Psi(B, \beta)) $
- $ MaxVote(C_{bal}, C_{qrm}, \beta)_{bal} < C_{bal} $
- 9, 10 和 1 矛盾。
0.2.3 定理 1
在满足 $B1(\beta)$，$B2(\beta)$，$B3(\beta)$ 的情况下， $$((B_{qrm} \subseteq B_{vot})\land(B’_{qrm}\subseteq B’_{vot})) \implies (B’_{dec} = B_{dec}) $$
0.2.4 定理 2
$$ \forall B\in\beta, b > B_{bal}, Q \cap B_{qrm} \ne \emptyset $$ 如果 $B1(\beta)$，$B2(\beta)$，$B3(\beta)$ 满足，那么存在一个 $ B’, B’_{bal}=b, B’_{qrm}=B’_{vot}=Q $ 使得 $B1(\beta\cup\{B’\})$，$B2(\beta\cup\{B’\})$，$B3(\beta\cup\{B’\})$ 成立。