設計出一套演算法，當然必須能夠證明他的正確性，且要滿足Consensus Problem的三個要求Termination、Agreement與Validity

Lamport 在他的論文 Paxos Made Simple 有更為嚴僅的數學證明，這邊僅簡易的說明。

Why does it work?

Validity

最終的決議一定是來自某一個參與的節點

這個說明非常簡單直觀，

從phase1和phase2的過程我們可以發現最後accept的v值，只來自:

1. Proposer提議的自己的值
2. Proposer復述來自Acceptor ack(n, (nx, vx)) 的vx值，而這個vx值也是來自別的Proposer發送的accept(n,vx)

因此最後達成共識的結果一定來自某一個系統裡的Proposer。

Agreement

當演算法完成時，所有節點都會做相同的決定，不會再變動，也稱為Safety

這個證明比較複雜

我們首先假設，
有過半數的Acceptors最後接受accept(n1, v1) 與 accept(n2,v2)
也就是說有一個Proposer1發送accept(n1, v1)，另一個Proposer2發送accept(n2, v2)

if (n1==n2):

過半數的Acceptors在phase1均回覆ack n1(=n2) 給 P1與P2
當n1等於n2可以說明P1等於P2，因為Proposal Number只會被回覆一次，要不是回覆要不是被忽略。

phase2

• Acceptors: 收到 accept(n,v)，但是你想想，此時有可能又有別的Proposer發出邀請或是提議，因此還要判斷
  * 他可能收到prepare(n') n'>n 或是 accept(n',vy) n'>n:
  => 直接忽略
  * 否則:
  => 接受該Proposer的提議v，令此時的N=n且nx=n, vx=v

所以如果整個系統接受 accept(n1, v1)與accept(n2, v2)且n1等於n2，可以知道這兩個accept訊息來自同一個Proposer

if (n1 < n2):

Proposer P1 從過半數的Acceptors收到 ack n1
Proposer P2 從過半數的Acceptors收到 ack n2

則Proposer P1 能夠至少傳送一個 accept(n1, v1) 給某個Acceptor A1是兩個Proposer過半數的Acceptors重疊的那一個，使得Proposer P2:

• 收到來自Acceptor A1 的ack，且該A1已經收到Proposer P1 的 accept(n1, v1)。
• Acceptor A1 會回覆 ack(n2,(nx,v1))

因為已經有了v1值，因此即使n2 > n1，Proposer P2也必須復述v1回去給他自己過半數的那些Acceptors。最終系統會達成共識。

Termination

保證所有參與決策且無故障的節點最終會做一個決定，執行的演算法不會無法終止，也稱為Liveness。

這裡就是問題出現的地方了，這個演算法居然有可能無法終止？

1. 還記得現實世界中的Network Model是Asynchronous的嗎
2. 除此之外分散式系統中，也有發生錯誤的可能。
3. 請看共識演算法前言

而Paxos只能處理Network Model是「訊息的傳遞會延遲，且延遲無上限，但是可以保證最終一定會傳到且無Byzantine failures」

如果有看過FLP的證明，且回想一下昨天最後的例子2討論，應該會有一點感覺，問題在哪。我們直接看例子:

1. 首先P發送prepare(3)給過半數的Acceptors R,S
2. Acceptors R,S也回覆ack(3)
3. 此時P來不及發送accept(3, v="joy")或是網路封包延遲！
4. Q趁虛而入發送prepare(4)給過半數的Acceptors R,S
5. 因為Acceptors R,S還沒接收P的accept訊息，因此將自身的N改為4，回覆ack(4)給Q
6. 但是Q也來不及發送accept(4, v="no_joy")或是網路封包延遲！
7. 此時P發送的accept(3, v="joy")傳到Acceptors R,S便會被忽略，因為3<4
8. Ｐ只好重新發送prepare(5)給過半數的Acceptors R,S
9. Acceptors R,S還沒接收Q的accept訊息，因此將自身的N改為5，回覆ack(5)給P

看出來了嗎，只要ack和accept之間有延遲，隨時會被另一個新的Proposer給插隊，而因為是分散式系統且Leaderless，所以本來就可能有多個Proposer且網路可能有封包延遲。
最終的結果就是Paxos是有機會沒辦法結束的，因此無法滿足Termination！

一種調整解決辦法就是選出Leader或是直接指定一個王牌id，沒有一個人的Proposal Number可以贏過該王牌id，當然這裡已經偏向實作的解決方法了，我們先專注在論文的scope本身。

討論

Paxos是一個可以讓分散式系統達成Strong Consistency的共識演算法。

但是面對網路的環境，系統可能因為封包不斷延遲導致無法達成共識，甚至當有server故障失效時，對其他的server來說他無法分辨該server是故障還是訊息延遲而已。

然而Paxos的保證是

「只要過半數的servers先達成共識，我可以保證該共識不會被破壞，且該結果會被傳遞，最終整個系統所有servers皆會達成共識」

以上就是Paxos的介紹啦～

Reference
All the pictures and contents are from "System EngineerI&II" Lectures from TU Dresden.