何東煉,楊晉吉,趙淦森,管金平
(華南師范大學(xué) 計(jì)算機(jī)學(xué)院,廣州 510631)
分布式是實(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)證.
隨著分布式系統(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)證.
在模型檢測(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)行軌跡.
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)移模型
由于需要就某個(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)生活鎖.
分布式系統(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)題.
本文以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)證與分析.