Symbols And Structure

  • 表决 $B$
    struct Ballot {
      dec: Decree,      // 表决的内容
      vot: Set<Node>,   // 表决投票通过的节点
      qrm: Set<Node>,   // 表决参与的节点
      bal: u64,         // 表决编号
    }
    
    A ballot is said to be successful, if every quorum member voted. In math: $$ B_{qrm} \subseteq B_{vot} $$
  • 投票 $v$
    struct Vote {
      pst: Node,        // 本投票的节点
      bal: u64,         // 本投票的表决编号
      dec: Decree,      // 本投票表决的内容
    }
    
  • 表决的集合 $\beta$

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} $

Lemma 1

如果 $\beta$ 中的表决 $B$ 是成功的,那么 $\beta$ 中更大编号的表决和 $B$ 的表决内容相同。 $$ ((B_{qrm} \subseteq B_{vot})\land(B'_{bal}>B_{bal})) \implies (B'_{dec}=B_{dec}) $$

Proof

定义集合 $\Psi(B, \beta)$: $\Psi(B, \beta) \triangleq \{B'\in \beta:(B'_{bal}>B_{bal})\land(B'_{dec}\ne B_{dec}) \}$,表示 $\beta$ 中编号比 $B$ 大并且表决内容不相同的表决的集合。

  1. $ C = min\{B':B'\in \Psi(B, \beta)\} $
  2. $ C_{bal} < B_{bal} $
  3. $ C_{qrm} \cap B_{bot} \ne \emptyset $ 因为 $B2$ 和 假设中的 $B$ 表决是成功的,也就是 $ B_{qrm} \subseteq B_{vot} $
  4. $ MaxVote(C_{bal},C_{qrm},\beta)_{bal} \ge B_{bal} $ 因为 $C_{qrm}$ 和 $B$ 的投票者一定有交集
  5. $ MaxVote(C_{bal}, C_{qrm}, \beta)\in Votes(\beta)$
  6. $ MaxVote(C_{bal}, C_{qrm}, \beta)_{dec} = C_{dec} $
  7. $ MaxVote(C_{bal}, C_{qrm}, \beta)_{dec} \ne B_{dec} $
  8. $ MaxVote(C_{bal}, C_{qrm}, \beta)_{bal} > B_{bal} $
  9. $ MaxVote(C_{bal}, C_{qrm}, \beta) \in Votes(\Psi(B, \beta)) $
  10. $ MaxVote(C_{bal}, C_{qrm}, \beta)_{bal} < C_{bal} $
  11. 9, 10 和 1 矛盾。

定理 1

在满足 $B1(\beta)$,$B2(\beta)$,$B3(\beta)$ 的情况下, $$((B_{qrm} \subseteq B_{vot})\land(B'_{qrm}\subseteq B'_{vot})) \implies (B'_{dec} = B_{dec}) $$

定理 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'\})$ 成立。