使用模型檢測方法對Paxos算法進行驗證與改進

何東煉，楊晉吉，趙淦森，管金平

(華南師范大學 計算機學院，廣州 510631)

1 引 言

分布式是實現橫向拓展，提升系統性能和可靠性的重要技術理論.現實實現中，分布式系統難以在分區失效、通信故障情況下對特定的狀態形成全局共識和一致性，因此系統需要使用共識算法[1]來保證系統內的節點達成一致的狀態.Paxos算法[2]是Lamport提出的一種共識算法，主要用于解決基于消息傳遞通信模型的分布式系統如何就某個值達成一致的共識，由于其在數據一致性方面的優秀表現，已被應用于許多重要的分布式服務中，并且存在多種變體.

Paxos算法在工業應用中具有明顯優勢并達到良好的性能和效果，因此對其進行深度的形式化分析和證明[3]工作至關重要.由于算法問題的復雜性，非形式化的證明往往容易出錯，而形式化的驗證，能夠更好地對算法的性質進行分析與研究.模型檢測[4]是形式化驗證的主要方法之一，能夠窮舉目標模型的狀態空間，以確定目標是否滿足所需性質，常用于分布式系統的驗證[5].

本文首先對Paxos算法及其研究進展進行介紹，然后根據算法流程對其進行形式化建模，以時態邏輯對算法的安全性、活性和活鎖可能性進行描述，將模型與需要驗證的性質輸入模型檢測器進行驗證.驗證結果表明，Paxos算法滿足安全性和活性，但在運行過程中有發生活鎖的可能，通過模型檢測器重現了發生活鎖時系統的運行軌跡并對其進行分析，最后對Paxos算法進行改進，解決其活鎖問題并重新進行驗證.

2 Paxos算法及其研究進展

隨著分布式系統的迅速發展和廣泛應用，用于分布式系統保持一致性的共識算法的研究和討論也越來越多.Paxos算法最初由Lamport提出，之后學者們便不斷對該算法進行改進，較為知名的有Multi-Paxos、Fast-Paxos、EPaxos、Raft等[6].Google的spanner[7]使用Multi-Paxos作為分布式共識保證的基礎組件，PaxosStore[8]是騰訊開發的、用于支持微信核心業務的分布式存儲系統.此外，Paxos算法也經常應用于軟件定義網絡及區塊鏈研究[9，10].

目前，已有學者對Paxos算法的形式化驗證進行了一些相關的工作，近年來的相關研究有：文獻[11]使用SPIN對Paxos進行了建模，以斷言的方式驗證了算法的安全性.文獻[12]使用TLAPS驗證Multi-Paxos 的安全性.文獻[13]使用有色Petri網對Paxos算法生成自動測試用例.文獻[14]開發了一種基于有效命題邏輯的演繹驗證方法，對Paxos及其幾種變體的安全性進行了驗證.文獻[15]構建了Paxos的Heard-Of模型，使用PSync語言驗證了模型的安全性和活性.文獻[16]使用IronFleet對以Multi-Paxos為核心的狀態機復制系統進行驗證，證明了其安全性和活性.文獻[17]使用交互式定理證明系統Coq對Paxos進行了安全性的驗證.

而本文的主要工作有：

1)使用SPIN對Paxos算法進行形式化建模，以線性時序邏輯(Linear-time Temporal Logic，LTL)對算法的安全性、活性和活鎖的性質進行描述.

2)對Paxos算法性質進行驗證分析，還原算法不滿足性質時的運行軌跡.

3)對Paxos算法進行改進，使算法滿足所需的性質，并重新進行驗證.

3 對Paxos算法進行模型檢測

在模型檢測中，驗證目標是否滿足某種性質，通常包含以下3個步驟：

1)建模.將需要進行驗證的目標轉化為能被模型檢測器接受的模型.如果模型過于復雜，會發生狀態空間爆炸問題，即系統過于復雜導致狀態過多使驗證失敗，因此需要使用抽象或偏序約簡等技術對模型進行化簡.

2)規約.把目標需要驗證的性質用時態邏輯表達式來進行表述.線性時序邏輯是常用的時態邏輯.

3)驗證.將模型和時態邏輯表達式作為模型檢測器的輸入，運行檢測器并檢驗結果.如果模型不滿足性質，檢測器通?？梢蕴峁┮粋€模型不滿足性質時的運行軌跡.

3.1 Paxos算法建模

Paxos算法把系統節點主要分為proposer，acceptor，和learner這3種角色.proposer提出提案，提案包括提案編號和提議的值.acceptor接收提案，若提案獲得多數的acceptor接受，則稱該提案被批準.learner學習提案，從acceptor學習最新被批準的提案值.傳遞消息的類型包括prepare，promise，propose，accept.在消息傳遞的過程中，不考慮消息遭到篡改的情況.

由圖1的算法執行流程可知，proposer的工作流程如下：

圖1 Paxos算法執行一次的流程

1)proposer發起一個編號N的提案，N全局唯一且單調遞增.然后向多數派的acceptor發送包含N的prepare消息，多數派即超過acceptor數量的一半.消息還會攜帶發送者的ID以確定消息的來源，以下不再贅述.

Proposer→Acceptor：prepare(N)

2)proposer發送prepare消息后等待接收promise消息，用num1記下收到的消息數，記下收到的promise消息中編號最大的提案為Nmax.如果等待超時，proposer收到的promise消息數量不滿足多數派，則提高提案編號N并重新發送prepare消息.如果proposer收到多數派的promise消息，則發送包含Nmax，V的propose消息給所有回復promise的acceptor.Nmax，V分別為收到的promise消息中編號最大提案的編號及對應的提案值，如果V為null，則由proposer自行設定(實驗中令V等于proposer自身的ID).

Acceptor→Proposer：propose(Nmax，V)

3)由于Paxos算法中一個進程可以擔任多種角色，為了減少模型的狀態空間，實驗中讓proposer同時擔任learner.因此，proposer等待接收accept消息，用num2記下收到的消息數.如果等待超時，proposer收到的accept消息數量不滿足多數派，則提高提案編號N并重新發送prepare消息.如果proposer收到的accept消息滿足多數派，則令voteEnd等于true，Value等于V，proposer進程結束.

定義proposer的結構體：

typedef ProposerMachine {

int ID，Value;

chan ch=[chanSize]of{mtype，int，int，int};

bool voteEnd=false;

};

其中ID為機器編號，Value為該機器的值，ch為消息信道，能夠存儲的消息量為chanSize，mtype為消息類型，voteEnd為結束標記.

算法中的事件則可用有限狀態機的輸入來表示，依據進程與事件之間的關系，可以得到狀態和輸入之間的轉移關系.根據工作流程可得圖2的proposer狀態轉移模型，其中!表示系統發送消息，而?表示系統接收消息.

圖2 proposer狀態轉移模型

acceptor的工作流程如下：

1)當acceptor收到一個prepare消息后，檢查消息中的N，若N大于ResN(初始為0)，則令ResN等于N，發送promise消息，消息包含AccN(初始為0)和AccV(初始為null).若N不大于ResN，則忽略該消息.

Acceptor→Proposer：promise(AccN，AccV)

2)當acceptor收到一個propose消息后，若消息中攜帶的編號N大于或等于ResN，則令AccN等于N，AccV等于V，并發送包含AccV的accept消息給propose以及learner.若N小于ResN，則忽略該消息.

Acceptor→Proposer，Learner：accept(AccV)

acceptor的結構體如下：

typedef AcceptorMachine {

int ID，ResN，AccN，AccV;

chan ch=[chanSize]of{mtype，int，int，int};

};

其中ID為機器編號，ResN為該機器收到的prepare消息的最高提案編號，AccN和AccV為該機器的收到的propose消息的編號最大的提案編號與提案值，ch為消息信道，可以存儲的消息量為chanSize，mtype為消息類型.acceptor狀態轉移結構模型如圖3所示.

圖3 acceptor狀態轉移模型

3.2 驗證屬性的描述及其驗證結果

由于需要就某個值達成一致的共識，分布式共識算法一般需要滿足4個基本性質：有效性、一致性、完整性、可終止性.這4個性質可以總結為安全性和活性，安全性即有效性、一致性以及完整性，活性即可終止性.

首先定義全局變量，實驗中proposer的數量為2，acceptor的數量為3，則多數派major的數量應為2，設置每個信道能夠存儲的最大消息量為4，初始輪次round為0.

定義實驗狀態及其含義如表1所示.

表1 實驗狀態

1)有效性的驗證

有效性即進程只能選擇已提出的值，其LTL表達式為：

validity {(true U(End0 && End1))→(true U [](Goal0 && Goal1))}

檢測結果如下：

State-vector 596 byte，depth reached 9999，errors：0

2)一致性的驗證

一致性即所有進程最終選擇的值都相同，其LTL表達式為：

agreement{(trueU(End0 && End1))→(trueU[]Goal)}

檢測結果如下：

State-vector 596 byte，depth reached 9999，errors：0

3)完整性的驗證

完整即進程一旦選取了某個值，這個值就不會再改變.該性質可以轉化了選取了某個值后就不會再次發起提案，其LTL表達式為：

integrity {(End0→[]End0)&&(End1→[]End1)}

檢測結果如下：

State-vector 596 byte，depth reached 9999，errors：0

4)可終止性的驗證

可終止性即系統中的所有進程最終都能夠選擇到某個值，其LTL表達式為：

termination{[](trueU(End0&& End1))}

檢測結果如下：

State-vector 596 byte，depth reached 9999，errors：0

5)發生活鎖可能性的驗證

檢測Paxos算法發生活鎖可能性，即檢測在有限的次數內Paxos算法是否能得到終止.假設發起提案的最大次數maxRound為50，LTL表達式為：

livelock{!((!End0&& !End1)Uround>maxRound)}

檢測結果如下：

State-vector 596 byte，depth reached 3536，errors：1

檢測表明算法并不能在限定的最大次數內結束.圖4為檢測器還原的算法不滿足驗證性質時的運行軌跡.

圖4 發生活鎖時的運行軌跡(部分)

由圖4可知，Paxos算法運行過程中，當acceptor對一個提案A發送promise消息后，如果再接到另一個編號更高的提案B的prepare請求，將再次進行promise，此時，提案A的propose請求將被忽略，然后發送的提案A的proposer再次提高編號進行prepare請求，這樣兩個proposer會交替提高編號進行prepare請求，導致產生活鎖.

4 改進Paxos算法以解決活鎖問題

分布式系統應用一般需要連續確定多個值，由于Paxos算法有產生活鎖的可能，直接使用會造成效率低下，因此在實際的應用中一般采用Multi-Paxos算法.

Multi-Paxos算法即使用一系列的Paxos算法實例來確定一系列的值.由于Paxos算法存在活鎖問題的主要原因是各個進程可以公平地發起提案請求，導致各個進程可以交替地提高編號發起提案，于是Multi-Paxos算法通過選舉leader的方式，讓proposer提案請求發送給leader，然后leader充當原來proposer的職能執行Paxos算法.這樣沒有proposer競爭發起提案，因此可以解決活鎖問題.

Multi-Paxos算法并沒有詳細說明如何進行選舉，本文使用一種基于優先級的選舉算法對Paxos進行類Multi-Paxos改進并重新進行驗證.設置proposer使其擁有各自的優先級，在proposer發起提案請求之前，先向其他所有的proposer發送hello消息查找自己的leader，其他proposer收到hello消息后，回應ack消息，消息包含自己的優先級.當proposer收到ack消息后將優先級最大的proposer作為自己的leader，然后讓leader代替自己發起提案.算法改進后的流程如圖5所示.

圖5 改進Paxos算法執行一次的流程(選舉后)

算法改進后的proposer的工作流程如下：

1)proposer進程運行后將啟動兩個線程：listener與leader.

2)proposer準備發起請求.若此時沒有確定leader，將向其他proposer的listener線程發送hello消息，收到ack消息后將最高優先級的proposer(可以為自身)作為leader.

Proposer→Listener：hello()

若已確定leader，則向leader發送request消息.

Proposer→Leader：request()

3)proposer等待接收accept消息，用num2記下收到的消息數.如果等待超時，proposer收到的accept消息數量不滿足多數派，則認為leader狀態不佳.重新確定leader后再次發送request消息.如果proposer收到的accept消息滿足多數派，則表明提案被選定，令Value等于V，proposer進程結束.

listener的工作流程如下：

listener線程等待接收其他proposer的hello消息，收到消息后會回復帶有proposer優先級的ack消息.

Listener→Proposer：ack(priority)

leader的工作流程如下：

1)leader線程等待接收到request消息，收到消息后發起一個編號N的提案，N為全局唯一且單調遞增.然后向多數派的acceptor發送包含N的prepare消息.

Leader→Acceptor：prepare(N)

2)leader等待接收promise消息.收到promise消息后，用num1記下收到的消息數，記下收到的promise消息中編號最大的提案為Nmax.如果等待超時，leader收到的promise消息數量不滿足多數派，則提高提案編號N并重新發送prepare消息.如果leader收到多數派的promise消息，則發送propose消息給所有回復promise的acceptor，消息包含Nmax，V及發起request消息的proposer的ID.Nmax，V分別為收到的promise消息中編號最大提案的編號及其對應的提案值，如果V為null，則由leader自行設定(實驗中令V等于leader自身的ID).

Leader→Acceptor：propose(Nmax，V，IDproposer)

修改proposer的結構體如下：

typedef ProposerMachine {

int ID，Value，priority;

chan ch=[chanSize] of { mtype，int，int，int };

bool voteEnd=false;

};

圖6為子線程listener與leader的狀態轉移模型.

圖6 listener和leader狀態轉移模型

改進后proposer的狀態轉移模型如圖7所示.

圖7 改進后的proposer狀態轉移模型

acceptor的工作流程如下：

1)當acceptor收到一個prepare消息后，檢查消息中的N，若N大于ResN(初始為0)，則令ResN等于N，發送promise消息，消息包含AccN(初始為0)和AccV(初始為null).若N不大于ResN，則忽略該消息.

Acceptor→Leader：promise(AccN，AccV)

2)當acceptor收到一個propose消息后，若消息中攜帶的編號N大于或等于ResN，則令AccN等于N，AccV等于V，并直接發送包含AccV的accept消息給發起request消息的proposer.若N小于ResN，則忽略該消息.

Acceptor→Proposer：accept(AccV)

改進后的acceptor狀態轉移模型基本沒有變化.

設置proposer的優先級等于其ID值，重新將模型輸入，檢測Paxos算法發生活鎖可能性.

檢測結果如下：

State-vector 988 byte，depth reached 1049，errors：0

模型檢測器沒有發現錯誤，即沒有發生活鎖問題.

5 結 語

本文以Paxos算法作為研究對象，基于模型檢測工具SPIN，對算法進行了形式化建模，并對該算法的安全性、活性、發生活鎖可能性使用LTL語言進行了描述，經過分析驗證，結果表明Paxos算法滿足安全性和活性，但存在發生活鎖的可能，并重現了活鎖發生時模型的運行軌跡.為了解決Paxos算法發生的活鎖問題，本文使用了一種為proposer添加優先級的類Multi-Paxos改進算法，通過選舉leader的方式，讓leader代替proposer提交提案.該方法優點是增加了算法的靈活性，可以指定不同proposer的優先級，在實際應用中，優先級可以根據相應的權重算法進行動態調整，從而實現proposer的負載均衡，經驗證，當leader單一存在時，可以解決Paxos算法中發生的活鎖現象.由于可能存在優先級相同及網絡不佳等問題，可能會發生同時存在多leader情況，然而即便如此也能大幅降低可能發生的活鎖現象，當所有proposer的優先級一樣時，改進后的算法會退化為普通的paxos算法，即每個proposer成為自身的leader.

Paxos算法可以應用在許多場景中，由于Paxos算法的復雜性，對其進行形式化建模與驗證后，可以使Paxos算法獲得更高的可信度，以及更好地研究該算法在不同場景與范圍中的應用情況.同時，Paxos存在很多變種算法，今后的工作可以以本文的Paxos算法模型為基礎或參考，對Paxos的改進算法進行驗證與分析.