The Part-Time Parliament（四）：Paxos一致性證明

04-21

基本協議證明

首先定義如下符號：

$outcome[p]$ ：法律簿上記錄的所有法令，如果尚未有任何法令，為 $null$ ；
$lastTried[p]$ ：上一次發起的表決的編號，如果沒有發起任何錶決，為 $-infty$ ；
$prevBal[p]$ ：最近一次投票的表決編號，如果未投票，為 $- infty$ ；
$prevDec[p]$ ：最近一次投票的表決法令，如果未投票，為 $null_p$ ；

$nextBal[p]$ ：由 $p$ 發出的所有 $LastVote(b, v)$ 投票中，編號最大的那個投票

接下來還有一些在表決過程中需要的臨時符號定義（可能會記錄在臨時小卡片上）：

$status[p]$ ：為以下狀態中的一種。 $idle$ ：未發起任何錶決； $trying$ ：嘗試發起新一輪的表決，編號為 $lastTried[p]$ ； $polling$ ：已經發起表決，尚處在表決過程中；
$quorum[p]$ ：如果 $status[p]=polling$ ，表示當前參與投票的牧師集合，否則無意義；
$preVotes[p]$ ：如果 $status[p]=polling$ ，表示收到的來自 $quorum$ 中牧師的對應與當前輪投票的 $LastVote$ 集合，否則無意義；
$voters[p]$ ：如果 $status[p]=polling$ ，表示收到的來自 $quorum$ 中牧師的對應與當前輪投票的投票消息集合，否則無意義；
$decree[p]$ ：如果 $status[p]=polling$ ，表示本輪投票的法令，否則無意義

如果 $p$ 不慎丟失了小卡片，那麼其狀態又會被歸零為 $idle$ 。

接下來分析基本協議中的每個過程極其產生的影響（對應上面的變數值的影響）

發起表決

選取新的表決編號 $b$ ，只要 $b > lastTried[p]$ 即可，並設置 $lastTried[p] = b$ ，且 $owner[b] = p$ ;
$status[p] = trying$ ;
$preVotes=phi$

發起 $NextBallot$ 消息

條件： $status[p]=trying$
動作：向其他牧師發起消息 $NextBallot(lastTried[p])$
說明：發起該消息的目的是獲得本次表決的法令信息。

收到 $NextBallot$ 消息

動作：如果 $bgeq nextBal[p]$ ，令 $nextBal[p]=b$
說明：該動作是由參與投票的牧師執行

發送 $LastVote$ 消息

條件： $nextBal[p] > prevBal[p]$
動作：發送 $LastVote(nextBall(p), v)$ 給 $owner(nextBall(p))$ ，其中 $v_{pst} = p, v_{bal} = prevBal[p], v_{dec}=prevDec[p]$
說明：

$nextBal[p] > prevBal[p]$ 是因為 $p$ 根據自己本地記錄的信息，無法再追溯到 $prevBal[p]$ 之前的投票信息了 ( $prevBal[p]$ 記錄的是 $p$ 最近一次的投票編號信息，例如是10，如果本次的投票編號小於10，為8，則不可能再找到距離8最近的那一次投票信息了)；
為什麼能保證 $prevBal[p]$ 就一定是距離 $nextBal[p]$ 最近的一次投票呢？這是因為協議後面保證了如果收到的 $BeginBallot(b, d)$ 中的 $b ot = nextBal[p]$ 的話是不會投票的，即不會為介於 $prevBal[p]$ 和 $nextBal[p]$ 之間表決而投票，這是其一。其二，我們可以證明，假如出現下面這種情況，也可以正確處理：

$p$ 當前的 $prevBal[p]=10$ ；
$q$ 發起了 $NextBallot(b), b=20$ 請求，於是 $p$ 設置 $nextBal[p]=20$ ，並返回 $LastVote(b, v)$ ，其中 $b=20, v_{bal}=10$ ；
$m$ 發起了 $NextBallot(b), b=30$ 請求，於是 $p$ 設置 $nextBal[p]=30$ ，並返回 $LastVote(b, v)$ ，其中 $b=30, v_{bal}=10$ ；
好，到這裡我們繼續推演，如果接下來 $q$ 先發起了 $BeginBallot(b, d), b=20$ 請求，由於 $20 < nextBal[p]=30$ ，於是， $p$ 拒絕投票；接下來， $m$ 發起了 $BeginBallot(b, d), b=30$ 請求，由於 $30 = nextBal[p]$ ，於是，投票，且 $prevBal[p]$ 在該過程中始終未變，條件 $B3(eta)$ 依然成立；
如果 $m$ 先發起了 $BeginBallot(b, d), b=30$ 請求，由於 $30 = nextBal[p]$ ，於是，投票；接下來， $q$ 發起了 $BeginBallot(b, d), b=20$ 請求，由於 $20 < nextBal[p]=30$ ，於是，拒絕投票；且觀察到 $prevBal[p]$ 在該過程中始終未變，條件 $B3(eta)$ 依然成立；

接受到消息 $LastVote(b, v)$

條件： $b=lastTried[p]$ 且 $status[p]=trying$
動作：令 $prevVotes[p] = prevVotes[p]cup{v}$

構造新一輪的表決信息

條件： $status[p]=trying$
動作：

令 $Qsubseteq {v_{pst}: v in preVotes[p]}$ ，且 $Q$ 包含大多數牧師
令 $status[p]=polling$
令 $quorum[p]=Q$
令 $voters[p]=phi$
選擇 $decree[p]$ 。從 $prevVotes[p]$ 中選擇最大的 $v$ （ $Max(forall v in prevVotes[p]))$ ），令 $decree[p]=v_{dec}$ ；
令 $eta = eta cup B$ ，其中： $B_{bal} = lastTried[p], B_{qrm} = Q, B_{dec} = decree[p], B_{vot}=phi$

發起表決：發送 $BeginBallot$ 消息

條件： $status[p]=polling$
動作：向 $quorum[p]$ 中的所有成員發起 $BeginBallot(lastTried[p], decree[p])$ 消息

處理表決：接受到 $BeginBallot(b, d)$ 消息

條件： $b = nextBal[p] > prevBal[p]$
動作：

設置 $prevBal[p]=b$
設置 $prevDec[p]=d$
更新 $eta$ 中表決編號為 $b$ 的表決輪 $B$ 信息，將當前牧師為其投票的信息更新至 $B$ 中

發送投票： $Voted$ 消息

條件： $prevBal[p] ot = - infty$
動作：發送消息 $Voted(prevBal[p], p)$ 消息至 $owner(prevBal[p])$

收到投票： $Voted(b, q)$ 消息

條件： $status[p] = polling$ 且 $b=lastTried[p]$
動作：令 $voters[p]=voters[p] cup {q}$

成功

條件： $status[p]=polling$ 並且 $quorum[p] subseteq voters[p]$ 和 $outcome[p]=null$
動作：設置 $outcome[p]=decree[p]$

發送成功 $Success$ 消息

條件： $outcome[p] ot =null$
動作：發送消息 $Success(outcome[p])$ 至其他牧師

接收到 $Success(d)$ 消息

條件： $outcome[p]=null$
動作：令 $outcome[p] = d$

說明：上面的某些步驟中會涉及到更新 $eta$ ，這個只是為了數學說明的完整性，在實際實踐的過程中是不需要這個步驟的。

一致性證明

一致性證明的目標是：

對於一輪成功的投票，所有的牧師得到的成功的表決結果（即被大多數人所認同的法令）是相同的。

$I1(p)$

$(outcome[p] ot = BLANK)Rightarrow exists B in eta: (B_{qrm} subseteq B_{vot}) land (B_{dec} = outcome[p])$

首先，在表決過程中， $eta$ 只增不減，而 $eta$ 的增加並不影響表達式結果的成立與否（如果 $exists B in eta$ ，那麼一定 $exists B in eta cup {B}$ ）；
其次，在表決過程中， $eta$ 內的 $B$ 可能的變化是 $B_{vot}$ 增加一個投票者，而這同樣不影響表達式結果的成立與否（如果 $B_{qrm} subseteq B_{vot}$ ，那麼 $B_{qrm} subseteq (B_{vot} cup {q})$ 也必然成立）；
最後，要使得 $outcome[p] ot = BLANK$ 成立，只存在以下兩種可能：

a). 如果 $p$ 是表決發起者，必須要滿足 $status[p]=polling, quorum[p] subseteq voters[p], outcome[p]=BLANK$ ，然後設置了 $outcome[p]=decree[p]$ 。而滿足該條件後，根據 $I5(p)$ ，必 $exists B in eta, quorum[p] = B_{qrm}, decree[p]=B_{dec}, voters[p] subseteq B_{vot}, lastTried[p] = B_{bal}$ ，則有 $B_{qrm} subseteq B_{vot}$ 成立，最終得出 $exists B in eta: (B_{qrm} subseteq B_{vot}) land (B_{dec} = outcome[p])$
b). 如果 $p$ 是投票者，那要滿足 $outcome[p] ot = BLANK$ ，必有對於消息的發起者 $q$ 滿足上面a)的條件。

$I2(p)$

$land owner(lastTried[p]) = p$
$land forall B in eta:(owner(B_{bal}) = p) Rightarrow$
$land B_{bal} <= lastTried[p] land (status[p] = trying) Rightarrow$
$B_{bal} < lastTried[p]$

因為只會在發起表決的時候改變 $lastTried[p]$ 和設置 $status[p]=trying$ ，而且在設置 $lastTried[p]=b$ 的時候有 $owner[b]=p$ ，因此，必然有 $owner(lastTried[p]) = p$ 成立；
因為 $eta$ 中的成員只有在 $BeginBallot$ 的時候才會增加，因此，這不會改變 $I2(p)$ ，而 $eta$ 中的成員 $B$ 另一個可能的改變是 $B$ 中增加一個投票者，這同樣也不會改變 $I2(p)$ ；
老實說，我沒太理解 $I2(p)$ 作者想表達什麼

$I3(p)$

$∧ prevBal[p] = MaxVote(infty, p, eta)_{bal}$
$∧ prevDec[p] = MaxVote(infty, p, eta)_{dec}$

$∧ nextBal[p] ≥ prevBal[p]$

因為 $MaxVote(infty, p, eta)$ 的值僅僅在 $eta$ 裡面增加一個由 $p$ 發出的投票後才會發生改變。而 $p$ 只有在收到 $BeginBallot$ 消息後才會進行投票，也只有在投票後才會修改 $prevBal[p]、prevDec[p]$ 的值，而根據 $MaxVote(infty, p, eta)$ 的定義，可以知道 $I3(p)$ 的1和2均成立；
而 $nextBal[p]$ 的值被設置是在判斷進來的 $NextBallot(b, p)$ 中的 $b >prevBal[p]$ 才會執行，而且 $prevBal[p]$ 是在收到 $BeginBallot$ 消息後被設置為 $nextBal[p]$ ，而且 $nextBal[p]$ 單調增，因此必有 $nextBal[p] ge prevBal[p]$ 。

$I4(p)$

$(status[p] = idle) ?$
$forall v ∈ prevVotes[p] : ∧ v = MaxVote(lastTried[p], v_{pst}, eta)$
$∧ nextBal[v_{pst}] ≥ lastTried[p]$

首先以人類語言理解下該表達式的含義：

$preVotes[p]$ ：記錄了 $p$ 收到的議會中其他牧師的距離 $lastTried[p]$ 最近的一次投票信息 $v$ 的集合；
$preVotes[p]$ 中的每個 $v$ 各個欄位的含義：

$v_{bal}$ ：表示投票所在的表決輪次的編號；
$v_{dec}$ ：表示投票的法令；
$v_{pst}$ ：表示投票者，注意，這裡並非指為 $v_{dec}$ 投票的所有牧師的集合，而只表示某一個投票的牧師，如 $v_{pst}=q$ 表示的是投票 $v$ 是從牧師 $q$ 那裡獲得的（還記得 $preVotes[p]$ 記錄的是所有其他牧師的 $LastVote$ 信息集合）

對於 $forall v in preVotes[p]$ ，假如 $v$ 來自牧師 $q$ 的 $LastVote(lastTried[p])$ ，根據其定義知道 $v$ 是表決編號最接近 $lastTried[p]$ 的一次表決中 $q$ 的投票，因此有 $v=MaxVote(lastTried[p], v_{pst}, eta)$ （ $q=v_{pst}$ ）;
$nextBal[q]$ 的含義知道其值變化是隨著 $lastTried[p]$ 而改變，且 $nextBal[q]$ 遞增，必然有 $nextBal[q] geq lastTried[p]$ 。

證明過程：

$status[p]$ 僅僅在發起表決的時候才會從 $idle$ 轉變為 $trying$ ，而此時會將 $preVotes[p]$ 設置為 $phi$ ，因此，後面的結論必然成立；
$preVotes[p]$ 的值只會在下面兩種情況下發生改變：

$Forget$ ：此時對應的是 $p$ 遺失了小紙條，於是 $status[p]$ 也會被變成 $idle$ ， $I4(p)$ 的條件都不成立；
$Receive$ $LastVote$ 消息：根據上面的解釋我們知道必然成立；

$lastTried[p]$ 只會在 $Try New Ballot$

$I5(p)$

$(status[p] = polling) ?$
$∧ quorum[p] ? {v_{pst} : v in prevVotes[p]}$
$∧ ?B ∈ eta : ∧ quorum[p] = B_{qrm}$
$∧ decree[p] = B_{dec}$

$∧ voters[p] ? B_{vot}$
$∧ lastTried[p] = B_{bal}$

證明：

只有在 $Start Poolling$ 動作發起後才會將 $status[p]$ 設置為 $polling$ 。而發起這個動作的先決條件便是收到了多數牧師的 $prevVote$ 信息，即 $∧ quorum[p] ? {v_{pst} : v in prevVotes[p]}$ 成立；
在 $Start Poolling$ 動作中，會向 $eta$ 中添加表決 $B:B_{dec} = decree[p], B_{bal} = lastTried[p], B_{qrm}=quorum[p]$ ，因此存在性得到滿足：即 $?B ∈ eta : ......$ ；
當 $status[p]=polling$ 後， $B_{bal}、B_{dec}、B_{qrm}$ 等不會再發生改變，因此，上面滿足的存在性也一定隨著表決的運行一直滿足；而唯一發生變化的是 $voters[p]$ ：一旦收到牧師 $q$ 的投票，便會將 $voters[p] = voters[p] cup {q}$ ，而這個 $q$ 也一定已經被添加至 $eta$ 中本輪表決 $B_{vot}$ 了，參考上面的「處理表決：接受到 $BeginBallot(b, d)$ 消息」的最後一個動作。

$I6(p)$

$∧ B1(eta) ∧ B2(eta) ∧ B3(eta)$
$∧ ?B ∈ eta : B_{qrm}$ is a majority set

$I6(p)$ 主要探討 $B1(eta)、B2(eta)、B3(eta)$ 滿足性問題；
$B1(eta)$ 要求任意的兩個 $B$ 不使用相同的表決編號 $B_{bal}$ ，這個在流程中得到滿足，而且 $B_{bal}$ 在協議運行過程中不變，因此， $B1(eta)$ 成立；
$B2(eta)$ 要求任意的兩個 $B$ 的 $B_{qrm}$ 存在交集，根據 $B_{qrm}$ 的選取規則，該條件滿足，而且 $B_{qrm}$ 一旦確定，在協議運行過程中也就不再改變，因此， $B2(eta)$ 成立；
$B3(eta)$ 要求每個牧師的投票要滿足這樣條件：其在某一輪 $B$ 的投票法令要與本表決輪所有投票者中為最近的那一輪投票的法令一致。針對 $p$ 發起的表決輪次 $B$ ，其表決法令 $B_{dec}$ 是由 $preVotes[p]$ 中最大的那一輪投票所決定，假定為 $alpha$ 。接下來 $p$ 向所有的 $Q subseteq preVotes[p]$ 且 $Q$ 包含多數牧師（注意這裡 $preVotes[p]$ 不必包含所有的牧師）發起投票請求， $Q$ 中的牧師有兩種選擇：

投票：那麼投票的法令必然是 $alpha$ ；
拒絕投票：這可能是因為有其他牧師 $q$ 在牧師 $p$ 的表決 $B$ 的 $BeginBallot$ 之前發起了新的表決 $B$ 的 $NextBallot$ 消息，這裡 $B_{bal} > B_{bal}$ ，雖然拒絕投票，但是在表決輪 $B$ 中也沒有為別的表決法令投票。
綜上，無論是那種選擇，都不會改變 $B$ 的表決法令 $alpha$ 。

$I7(p)$

$∧ ?NextBallot(b) ∈ M : (b ≤ lastTried[owner(b)])$
$∧ ?LastVote(b, v) ∈ M : ∧ v = MaxVote(b, v_{pst}, eta)$
$∧ nextBal[v_{pst}] ≥ b$
$∧ ?BeginBallot(b, d) ∈ M : ?B ∈ eta : (B_{bal} = b) ∧ (B_{dec} = d)$
$∧ ?Voted(b, p) ∈ M : ?B ∈ eta : (B_{bal} = b) ∧ (p ∈ B_{vot})$
$∧ ?Success(d) ∈ M : ?p : outcome[p] = d ot = blank$

這些根據其定義就能很顯然地看出來，無需贅述。

總結

梳理上面的證明過程，我們可以得到以下結論：

對於每一輪投票，無論成功與否，記錄在 $eta$ 中的 $B$ 的表決法令不會變（參考 $I6(p)$ ）;
如果某一輪表決 $B$ 成功，那麼在此之後的所有表決輪必然與 $B$ 法令相同；
結合上面兩點，可以得出，只要表決成功，那麼所有牧師最終會得到一致的法令，這就是我們一致性要證明的目標。