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

(華南師范大學(xué) 計(jì)算機(jī)學(xué)院，廣州 510631)

1 引 言

分布式是實(shí)現(xiàn)橫向拓展，提升系統(tǒng)性能和可靠性的重要技術(shù)理論.現(xiàn)實(shí)實(shí)現(xiàn)中，分布式系統(tǒng)難以在分區(qū)失效、通信故障情況下對(duì)特定的狀態(tài)形成全局共識(shí)和一致性，因此系統(tǒng)需要使用共識(shí)算法[1]來(lái)保證系統(tǒng)內(nèi)的節(jié)點(diǎn)達(dá)成一致的狀態(tài).Paxos算法[2]是Lamport提出的一種共識(shí)算法，主要用于解決基于消息傳遞通信模型的分布式系統(tǒng)如何就某個(gè)值達(dá)成一致的共識(shí)，由于其在數(shù)據(jù)一致性方面的優(yōu)秀表現(xiàn)，已被應(yīng)用于許多重要的分布式服務(wù)中，并且存在多種變體.

Paxos算法在工業(yè)應(yīng)用中具有明顯優(yōu)勢(shì)并達(dá)到良好的性能和效果，因此對(duì)其進(jìn)行深度的形式化分析和證明[3]工作至關(guān)重要.由于算法問(wèn)題的復(fù)雜性，非形式化的證明往往容易出錯(cuò)，而形式化的驗(yàn)證，能夠更好地對(duì)算法的性質(zhì)進(jìn)行分析與研究.模型檢測(cè)[4]是形式化驗(yàn)證的主要方法之一，能夠窮舉目標(biāo)模型的狀態(tài)空間，以確定目標(biāo)是否滿足所需性質(zhì)，常用于分布式系統(tǒng)的驗(yàn)證[5].

本文首先對(duì)Paxos算法及其研究進(jìn)展進(jìn)行介紹，然后根據(jù)算法流程對(duì)其進(jìn)行形式化建模，以時(shí)態(tài)邏輯對(duì)算法的安全性、活性和活鎖可能性進(jìn)行描述，將模型與需要驗(yàn)證的性質(zhì)輸入模型檢測(cè)器進(jìn)行驗(yàn)證.驗(yàn)證結(jié)果表明，Paxos算法滿足安全性和活性，但在運(yùn)行過(guò)程中有發(fā)生活鎖的可能，通過(guò)模型檢測(cè)器重現(xiàn)了發(fā)生活鎖時(shí)系統(tǒng)的運(yùn)行軌跡并對(duì)其進(jìn)行分析，最后對(duì)Paxos算法進(jìn)行改進(jìn)，解決其活鎖問(wèn)題并重新進(jìn)行驗(yàn)證.

2 Paxos算法及其研究進(jìn)展

隨著分布式系統(tǒng)的迅速發(fā)展和廣泛應(yīng)用，用于分布式系統(tǒng)保持一致性的共識(shí)算法的研究和討論也越來(lái)越多.Paxos算法最初由Lamport提出，之后學(xué)者們便不斷對(duì)該算法進(jìn)行改進(jìn)，較為知名的有Multi-Paxos、Fast-Paxos、EPaxos、Raft等[6].Google的spanner[7]使用Multi-Paxos作為分布式共識(shí)保證的基礎(chǔ)組件，PaxosStore[8]是騰訊開發(fā)的、用于支持微信核心業(yè)務(wù)的分布式存儲(chǔ)系統(tǒng).此外，Paxos算法也經(jīng)常應(yīng)用于軟件定義網(wǎng)絡(luò)及區(qū)塊鏈研究[9，10].

目前，已有學(xué)者對(duì)Paxos算法的形式化驗(yàn)證進(jìn)行了一些相關(guān)的工作，近年來(lái)的相關(guān)研究有：文獻(xiàn)[11]使用SPIN對(duì)Paxos進(jìn)行了建模，以斷言的方式驗(yàn)證了算法的安全性.文獻(xiàn)[12]使用TLAPS驗(yàn)證Multi-Paxos 的安全性.文獻(xiàn)[13]使用有色Petri網(wǎng)對(duì)Paxos算法生成自動(dòng)測(cè)試用例.文獻(xiàn)[14]開發(fā)了一種基于有效命題邏輯的演繹驗(yàn)證方法，對(duì)Paxos及其幾種變體的安全性進(jìn)行了驗(yàn)證.文獻(xiàn)[15]構(gòu)建了Paxos的Heard-Of模型，使用PSync語(yǔ)言驗(yàn)證了模型的安全性和活性.文獻(xiàn)[16]使用IronFleet對(duì)以Multi-Paxos為核心的狀態(tài)機(jī)復(fù)制系統(tǒng)進(jìn)行驗(yàn)證，證明了其安全性和活性.文獻(xiàn)[17]使用交互式定理證明系統(tǒng)Coq對(duì)Paxos進(jìn)行了安全性的驗(yàn)證.

而本文的主要工作有：

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

2)對(duì)Paxos算法性質(zhì)進(jìn)行驗(yàn)證分析，還原算法不滿足性質(zhì)時(shí)的運(yùn)行軌跡.

3)對(duì)Paxos算法進(jìn)行改進(jìn)，使算法滿足所需的性質(zhì)，并重新進(jìn)行驗(yàn)證.

3 對(duì)Paxos算法進(jìn)行模型檢測(cè)

在模型檢測(cè)中，驗(yàn)證目標(biāo)是否滿足某種性質(zhì)，通常包含以下3個(gè)步驟：

1)建模.將需要進(jìn)行驗(yàn)證的目標(biāo)轉(zhuǎn)化為能被模型檢測(cè)器接受的模型.如果模型過(guò)于復(fù)雜，會(huì)發(fā)生狀態(tài)空間爆炸問(wèn)題，即系統(tǒng)過(guò)于復(fù)雜導(dǎo)致狀態(tài)過(guò)多使驗(yàn)證失敗，因此需要使用抽象或偏序約簡(jiǎn)等技術(shù)對(duì)模型進(jìn)行化簡(jiǎn).

2)規(guī)約.把目標(biāo)需要驗(yàn)證的性質(zhì)用時(shí)態(tài)邏輯表達(dá)式來(lái)進(jìn)行表述.線性時(shí)序邏輯是常用的時(shí)態(tài)邏輯.

3)驗(yàn)證.將模型和時(shí)態(tài)邏輯表達(dá)式作為模型檢測(cè)器的輸入，運(yùn)行檢測(cè)器并檢驗(yàn)結(jié)果.如果模型不滿足性質(zhì)，檢測(cè)器通?？梢蕴峁┮粋€(gè)模型不滿足性質(zhì)時(shí)的運(yùn)行軌跡.

3.1 Paxos算法建模

Paxos算法把系統(tǒng)節(jié)點(diǎn)主要分為proposer，acceptor，和learner這3種角色.proposer提出提案，提案包括提案編號(hào)和提議的值.acceptor接收提案，若提案獲得多數(shù)的acceptor接受，則稱該提案被批準(zhǔn).learner學(xué)習(xí)提案，從acceptor學(xué)習(xí)最新被批準(zhǔn)的提案值.傳遞消息的類型包括prepare，promise，propose，accept.在消息傳遞的過(guò)程中，不考慮消息遭到篡改的情況.

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

圖1 Paxos算法執(zhí)行一次的流程

1)proposer發(fā)起一個(gè)編號(hào)N的提案，N全局唯一且單調(diào)遞增.然后向多數(shù)派的acceptor發(fā)送包含N的prepare消息，多數(shù)派即超過(guò)acceptor數(shù)量的一半.消息還會(huì)攜帶發(fā)送者的ID以確定消息的來(lái)源，以下不再贅述.

Proposer→Acceptor：prepare(N)

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

Acceptor→Proposer：propose(Nmax，V)

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

定義proposer的結(jié)構(gòu)體：

typedef ProposerMachine {

int ID，Value;

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

bool voteEnd=false;

};

其中ID為機(jī)器編號(hào)，Value為該機(jī)器的值，ch為消息信道，能夠存儲(chǔ)的消息量為chanSize，mtype為消息類型，voteEnd為結(jié)束標(biāo)記.

算法中的事件則可用有限狀態(tài)機(jī)的輸入來(lái)表示，依據(jù)進(jìn)程與事件之間的關(guān)系，可以得到狀態(tài)和輸入之間的轉(zhuǎn)移關(guān)系.根據(jù)工作流程可得圖2的proposer狀態(tài)轉(zhuǎn)移模型，其中!表示系統(tǒng)發(fā)送消息，而?表示系統(tǒng)接收消息.

圖2 proposer狀態(tài)轉(zhuǎn)移模型

acceptor的工作流程如下：

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

Acceptor→Proposer：promise(AccN，AccV)

2)當(dāng)acceptor收到一個(gè)propose消息后，若消息中攜帶的編號(hào)N大于或等于ResN，則令A(yù)ccN等于N，AccV等于V，并發(fā)送包含AccV的accept消息給propose以及l(fā)earner.若N小于ResN，則忽略該消息.

Acceptor→Proposer，Learner：accept(AccV)

acceptor的結(jié)構(gòu)體如下：

typedef AcceptorMachine {

int ID，ResN，AccN，AccV;

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

};

其中ID為機(jī)器編號(hào)，ResN為該機(jī)器收到的prepare消息的最高提案編號(hào)，AccN和AccV為該機(jī)器的收到的propose消息的編號(hào)最大的提案編號(hào)與提案值，ch為消息信道，可以存儲(chǔ)的消息量為chanSize，mtype為消息類型.acceptor狀態(tài)轉(zhuǎn)移結(jié)構(gòu)模型如圖3所示.

圖3 acceptor狀態(tài)轉(zhuǎn)移模型

3.2 驗(yàn)證屬性的描述及其驗(yàn)證結(jié)果

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

首先定義全局變量，實(shí)驗(yàn)中proposer的數(shù)量為2，acceptor的數(shù)量為3，則多數(shù)派major的數(shù)量應(yīng)為2，設(shè)置每個(gè)信道能夠存儲(chǔ)的最大消息量為4，初始輪次round為0.

定義實(shí)驗(yàn)狀態(tài)及其含義如表1所示.

表1 實(shí)驗(yàn)狀態(tài)

1)有效性的驗(yàn)證

有效性即進(jìn)程只能選擇已提出的值，其LTL表達(dá)式為：

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

檢測(cè)結(jié)果如下：

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

2)一致性的驗(yàn)證

一致性即所有進(jìn)程最終選擇的值都相同，其LTL表達(dá)式為：

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

檢測(cè)結(jié)果如下：

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

3)完整性的驗(yàn)證

完整即進(jìn)程一旦選取了某個(gè)值，這個(gè)值就不會(huì)再改變.該性質(zhì)可以轉(zhuǎn)化了選取了某個(gè)值后就不會(huì)再次發(fā)起提案，其LTL表達(dá)式為：

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

檢測(cè)結(jié)果如下：

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

4)可終止性的驗(yàn)證

可終止性即系統(tǒng)中的所有進(jìn)程最終都能夠選擇到某個(gè)值，其LTL表達(dá)式為：

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

檢測(cè)結(jié)果如下：

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

5)發(fā)生活鎖可能性的驗(yàn)證

檢測(cè)Paxos算法發(fā)生活鎖可能性，即檢測(cè)在有限的次數(shù)內(nèi)Paxos算法是否能得到終止.假設(shè)發(fā)起提案的最大次數(shù)maxRound為50，LTL表達(dá)式為：

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

檢測(cè)結(jié)果如下：

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

檢測(cè)表明算法并不能在限定的最大次數(shù)內(nèi)結(jié)束.圖4為檢測(cè)器還原的算法不滿足驗(yàn)證性質(zhì)時(shí)的運(yùn)行軌跡.

圖4 發(fā)生活鎖時(shí)的運(yùn)行軌跡(部分)

由圖4可知，Paxos算法運(yùn)行過(guò)程中，當(dāng)acceptor對(duì)一個(gè)提案A發(fā)送promise消息后，如果再接到另一個(gè)編號(hào)更高的提案B的prepare請(qǐng)求，將再次進(jìn)行promise，此時(shí)，提案A的propose請(qǐng)求將被忽略，然后發(fā)送的提案A的proposer再次提高編號(hào)進(jìn)行prepare請(qǐng)求，這樣兩個(gè)proposer會(huì)交替提高編號(hào)進(jìn)行prepare請(qǐng)求，導(dǎo)致產(chǎn)生活鎖.

4 改進(jìn)Paxos算法以解決活鎖問(wèn)題

分布式系統(tǒng)應(yīng)用一般需要連續(xù)確定多個(gè)值，由于Paxos算法有產(chǎn)生活鎖的可能，直接使用會(huì)造成效率低下，因此在實(shí)際的應(yīng)用中一般采用Multi-Paxos算法.

Multi-Paxos算法即使用一系列的Paxos算法實(shí)例來(lái)確定一系列的值.由于Paxos算法存在活鎖問(wèn)題的主要原因是各個(gè)進(jìn)程可以公平地發(fā)起提案請(qǐng)求，導(dǎo)致各個(gè)進(jìn)程可以交替地提高編號(hào)發(fā)起提案，于是Multi-Paxos算法通過(guò)選舉leader的方式，讓proposer提案請(qǐng)求發(fā)送給leader，然后leader充當(dāng)原來(lái)proposer的職能執(zhí)行Paxos算法.這樣沒(méi)有proposer競(jìng)爭(zhēng)發(fā)起提案，因此可以解決活鎖問(wèn)題.

Multi-Paxos算法并沒(méi)有詳細(xì)說(shuō)明如何進(jìn)行選舉，本文使用一種基于優(yōu)先級(jí)的選舉算法對(duì)Paxos進(jìn)行類Multi-Paxos改進(jìn)并重新進(jìn)行驗(yàn)證.設(shè)置proposer使其擁有各自的優(yōu)先級(jí)，在proposer發(fā)起提案請(qǐng)求之前，先向其他所有的proposer發(fā)送hello消息查找自己的leader，其他proposer收到hello消息后，回應(yīng)ack消息，消息包含自己的優(yōu)先級(jí).當(dāng)proposer收到ack消息后將優(yōu)先級(jí)最大的proposer作為自己的leader，然后讓leader代替自己發(fā)起提案.算法改進(jìn)后的流程如圖5所示.

圖5 改進(jìn)Paxos算法執(zhí)行一次的流程(選舉后)

算法改進(jìn)后的proposer的工作流程如下：

1)proposer進(jìn)程運(yùn)行后將啟動(dòng)兩個(gè)線程：listener與leader.

2)proposer準(zhǔn)備發(fā)起請(qǐng)求.若此時(shí)沒(méi)有確定leader，將向其他proposer的listener線程發(fā)送hello消息，收到ack消息后將最高優(yōu)先級(jí)的proposer(可以為自身)作為leader.

Proposer→Listener：hello()

若已確定leader，則向leader發(fā)送request消息.

Proposer→Leader：request()

3)proposer等待接收accept消息，用num2記下收到的消息數(shù).如果等待超時(shí)，proposer收到的accept消息數(shù)量不滿足多數(shù)派，則認(rèn)為leader狀態(tài)不佳.重新確定leader后再次發(fā)送request消息.如果proposer收到的accept消息滿足多數(shù)派，則表明提案被選定，令Value等于V，proposer進(jìn)程結(jié)束.

listener的工作流程如下：

listener線程等待接收其他proposer的hello消息，收到消息后會(huì)回復(fù)帶有proposer優(yōu)先級(jí)的ack消息.

Listener→Proposer：ack(priority)

leader的工作流程如下：

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

Leader→Acceptor：prepare(N)

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

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

修改proposer的結(jié)構(gòu)體如下：

typedef ProposerMachine {

int ID，Value，priority;

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

bool voteEnd=false;

};

圖6為子線程listener與leader的狀態(tài)轉(zhuǎn)移模型.

圖6 listener和leader狀態(tài)轉(zhuǎn)移模型

改進(jìn)后proposer的狀態(tài)轉(zhuǎn)移模型如圖7所示.

圖7 改進(jìn)后的proposer狀態(tài)轉(zhuǎn)移模型

acceptor的工作流程如下：

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

Acceptor→Leader：promise(AccN，AccV)

2)當(dāng)acceptor收到一個(gè)propose消息后，若消息中攜帶的編號(hào)N大于或等于ResN，則令A(yù)ccN等于N，AccV等于V，并直接發(fā)送包含AccV的accept消息給發(fā)起request消息的proposer.若N小于ResN，則忽略該消息.

Acceptor→Proposer：accept(AccV)

改進(jìn)后的acceptor狀態(tài)轉(zhuǎn)移模型基本沒(méi)有變化.

設(shè)置proposer的優(yōu)先級(jí)等于其ID值，重新將模型輸入，檢測(cè)Paxos算法發(fā)生活鎖可能性.

檢測(cè)結(jié)果如下：

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

模型檢測(cè)器沒(méi)有發(fā)現(xiàn)錯(cuò)誤，即沒(méi)有發(fā)生活鎖問(wèn)題.

5 結(jié) 語(yǔ)

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

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