引言

早在1990年，Leslie Lamport（即 LaTeX 中的"La"，微軟研究院科學家，獲得2013年圖靈獎）向ACM Transactions on Computer Systems (TOCS)提交了關于Paxos算法的論文The Part-Time Parliament。幾位審閱人表示，雖然論文沒什么特別的用處，但還是有點意思，只是要把Paxos相關的故事背景全部刪掉。Leslie Lamport心高氣傲，覺得審閱人沒有絲毫的幽默感，于是撤回文章不再發表。直到1998年，用戶開始支持Paxos，Leslie Lamport重新發表文章，但相比1990年的版本，文章沒有太大的修改，所以還是不好理解。于是在2001年，為了通俗性，Leslie Lamport簡化文章發表了Paxos Made Simple，這次文中沒有一個公式。

但事實如何？大家不妨讀一讀Paxos Made Simple。Leslie Lamport在文中漸進式地、從零開始推導出了Paxos協議，中間用數學歸納法進行了證明。可能是因為表述順序的問題，導致這篇文章似乎還是不好理解。

于是，基于此背景，本文根據Paxos Made Simple，重新描述Paxos協議，提供兩種證明方法，給出常見的理解誤區。期望讀者通過閱讀本文，再結合Paxos Made Simple，就可以深入理解基本的Paxos協議理論。

基本概念

• Proposal Value：提議的值；
• Proposal Number：提議編號，要求提議編號不能沖突；
• Proposal：提議 = 提議的值 + 提議編號；
• Proposer：提議發起者；
• Acceptor：提議接受者；
• Learner：提議學習者。

注意，提議跟提議的值是有區別的，后面會具體說明。協議中Proposer有兩個行為，一個是向Acceptor發Prepare請求，另一個是向Acceptor發Accept請求；Acceptor則根據協議規則，對Proposer的請求作出應答；最后Learner可以根據Acceptor的狀態，學習最終被確定的值。

方便討論，在本文中，記{n，v}為提議編號為n，提議的值為v的提議，記(m，{n，v})為承諾了Prepare（m）請求，并接受了提議{n，v}。

協議過程

第一階段A

Proposer選擇一個提議編號n，向所有的Acceptor廣播Prepare（n）請求。

第一階段B

Acceptor接收到Prepare（n）請求，若提議編號n比之前接收的Prepare請求都要大，則承諾將不會接收提議編號比n小的提議，并且帶上之前Accept的提議中編號小于n的最大的提議，否則不予理會。

第二階段A

Proposer得到了多數Acceptor的承諾后，如果沒有發現有一個Acceptor接受過一個值，那么向所有的Acceptor發起自己的值和提議編號n，否則，從所有接受過的值中選擇對應的提議編號最大的，作為提議的值，提議編號仍然為n。

第二階段B

Acceptor接收到提議后，如果該提議編號不違反自己做過的承諾，則接受該提議。

需要注意的是，Proposer發出Prepare（n）請求后，得到多數派的應答，然后可以隨便再選擇一個多數派廣播Accept請求，而不一定要將Accept請求發給有應答的Acceptor，這是常見的Paxos理解誤區。

小結

上面的圖例中，P1廣播了Prepare請求，但是給A3的丟失，不過A1、A2成功返回了，即該Prepare請求得到多數派的應答，然后它可以廣播Accept請求，但是給A1的丟了，不過A2，A3成功接受了這個提議。因為這個提議被多數派（A2，A3形成多數派）接受，我們稱被多數派接受的提議對應的值被Chosen。

三個Acceptor之前都沒有接受過Accept請求，所以不用返回接受過的提議，但是如果接受過提議，則根據第一階段B，要帶上之前Accept的提議中編號小于n的最大的提議。

Proposer廣播Prepare請求之后，收到了A1和A2的應答，應答中攜帶了它們之前接受過的{n1, v1}和{n2, v2}，Proposer則根據n1，n2的大小關系，選擇較大的那個提議對應的值，比如n1 > n2，那么就選擇v1作為提議的值，最后它向Acceptor廣播提議{n, v1}。

Paxos協議最終解決什么問題

當一個提議被多數派接受后，這個提議對應的值被Chosen（選定），一旦有一個值被Chosen，那么只要按照協議的規則繼續交互，后續被Chosen的值都是同一個值，也就是這個Chosen值的一致性問題。

協議證明

上文就是基本Paxos協議的全部內容，其實是一個非常確定的數學問題。下面用數學語言表達，進而用嚴謹的數學語言加以證明。

Paxos原命題

如果一個提議｛n0，v0｝被大多數Acceptor接受，那么不存在提議｛n1，v1｝被大多數Acceptor接受，其中n0 < n1，v0 != v1。

Paxos原命題加強

如果一個提議｛n0，v0｝被大多數Acceptor接受，那么不存在Acceptor接受提議｛n1，v1｝，其中n0 < n1，v0 != v1。

Paxos原命題進一步加強

如果一個提議｛n0，v0｝被大多數Acceptor接受，那么不存在Proposer發出提議｛n1，v1｝，其中n0 < n1，v0 != v1。

如果“Paxos原命題進一步加強”成立，那么“Paxos原命題”顯然成立。下面我們通過證明“Paxos原命題進一步加強”，從而證明“Paxos原命題”。論文中是使用數學歸納法進行證明的，這里用比較緊湊的語言重新表述證明過程。

歸納法證明

假設，提議｛m，v｝（簡稱提議m）被多數派接受，那么提議m到n（如果存在）對應的值都為v，其中n不小于m。

這里對n進行歸納假設，當n = m時，結論顯然成立。

設n = k時結論成立，即如果提議｛m，v｝被多數派接受，

那么提議m到k對應的值都為v，其中k不小于m。

當n = k+1時，若提議k+1不存在，那么結論成立。

若提議k+1存在，對應的值為v1，

因為提議m已經被多數派接受，又k+1的Prepare被多數派承諾并返回結果。

基于兩個多數派必有交集，易知提議k+1的第一階段B有帶提議回來。

那么v1是從返回的提議中選出來的，不妨設這個值是選自提議｛t，v1｝。

根據第二階段B，因為t是返回的提議中編號最大，所以t >= m。

又由第一階段A，知道t < n。所以根據假設t對應的值為v。

即有v1 = v。所以由n = k結論成立，可以推出n = k+1成立。

于是對于任意的提議編號不小于m的提議n，對應的值都為v。

所以命題成立。

反證法證明

假設存在，不妨設n1是滿足條件的最小提議編號。

即存在提議｛n1，v1｝，其中n0 < n1，v0 != v1。-------------（A）

那么提議n0，n0+1，n0+2，...，n1-1對應的值為v0。-------------（B）

由于存在提議｛n1，v1｝，則說明大多數Acceptor已經接收n1的Prepare，并承諾將不會接受提議編號比n1小的提議。

又因為｛n0，v0｝被大多數Acceptor接受，?

所以存在一個Acceptor既對n1的Prepare進行了承諾，又接受了提議n0。

由協議的第二階段B知，這個Acceptor先接受了｛n0，v0｝。

所以發出｛n1，v1｝提議的Proposer會從大多數的Acceptor返回中得知，

至少某個編號不小于n0而且值為v0的提議已經被接受。-------------（C）

由協議的第二階段A知，

該Proposer會從已經被接受的值中選擇一個提議編號最大的，作為提議的值。

由（C）知該提議編號不小于n0，由協議第二階段B知，該提議編號小于n1，

于是由（B）知v1 == v0，與（A）矛盾。

所以命題成立。

通過上面的證明過程，我們反過來回味一下協議中的細節。

• 為什么要被多數派接受？

  因為兩個多數派之間必有交集，所以Paxos協議一般是2F+1個Acceptor，然后允許最多F個Acceptor停機，而保證協議依然能夠正常進行，最終得到一個確定的值。

• 為什么需要做一個承諾？

  可以保證第二階段A中Proposer的選擇不會受到未來變化的干擾。另外，對于一個Acceptor而言，這個承諾決定了它回應提議編號較大的Prepare請求，和接受提議編號較小的Accept請求的先后順序。

• 為什么第二階段A要從返回的協議中選擇一個編號最大的？

  這樣選出來的提議編號一定不小于已經被多數派接受的提議編號，進而可以根據假設得到該提議編號對應的值是Chosen的那個值。

原文的第一階段B

Acceptor接收到Prepare（n）請求，若提議編號n比之前接收的Prepare請求都要大，則承諾將不會接收提議編號比n小的提議，并且帶上之前Accept的提議中編號最大的提議，否則不予理會。

相對上面的表達少了“比n小的”，通過郵件向Leslie Lamport請教了這個問題，他表示接受一個提議，包含回應了一個Prepare請求。這個有點隱晦，但也完全合理，有了這個條件，上面的證明也就通順了。就是說Acceptor接受過的提議的編號總是不大于承諾過的提議編號，于是可以將這個“比n小的”去掉，在實際工程實踐中我們往往只保存接受過的提議中編號最大的，以及承諾過的Prepare請求編號最大的。

Leslie Lamport也表示在去掉“比n小的”的情況下，就算接受一個提議不包含回應一個Prepare請求，最終結論也是對的，因為前者明顯可以推導出后者，去掉反而把條件加強了。

假如返回的提議中有編號大于n的，比如{m，v}，那么肯定存在多數派承諾拒絕小于m的Accept請求，所以提議{n，v}不可能被多數派接受。

學習過程

如果一個提議被多數Acceptor接受，則這個提議對應的值被選定。

一個簡單直接的學習方法就是，獲取所有Acceptor接受過的提議，然后看哪個提議被多數的Acceptor接受，那么該提議對應的值就是被選定的。

另外，也可以把Learner看作一個Proposer，根據協議流程，發起一個正常的提議，然后看這個提議是否被多數Acceptor接受。

這里強調“一個提議被多數Acceptor接受”，而不是“一個值被多數Acceptor”接受，如果是后者會有什么問題？

提議{3，v3}，{5，v3}分別被B、C接受，即有v3被多數派接受，但不能說明v3被選定（Chosen），只有提議{7，v1}被多數派（A和C組成）接受，我們才能說v1被選定，而這個選定的值隨著協議繼續進行不會改變。

總結

“與其預測未來，不如限制未來”，這應該是Paxos協議的核心思想。如果你在閱讀Paxos的這篇論文時感到困惑，不妨找到“限制”的段落回味一番。Paxos協議本身是比較簡單的，如何將Paxos協議工程化，才是真正的難題。

目前在微信核心存儲PaxosStore中，每分鐘調用Paxos協議過程數十億次量級，而《微信PaxosStore內存云揭秘：十億Paxos/分鐘的挑戰》一文， 則對內存云子系統做了展開。

后續我們將發表更多的實踐方案，包括萬億級別的海量閃存存儲，支持單表億行的NewSQL解決方案，以及有別于業界的開源實現，PaxosStore架構方案基于非租約的Paxos實現等內容。

作者介紹

鄭建軍，微信工程師，目前負責微信基礎存儲服務，致力于強一致、高可用的大規模分布式存儲系統的設計與研發。

總結

以上是生活随笔為你收集整理的微信PaxosStore：深入浅出Paxos算法协议的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。