基于概率模型的Raft協(xié)議形式化驗證

管金平，楊晉吉，楊成龍

（華南師范大學(xué)計算機學(xué)院，廣東 廣州 510631）

0 引 言

隨著Internet 的迅速發(fā)展，分布式系統(tǒng)應(yīng)用也越來越廣泛。它與傳統(tǒng)的集中式系統(tǒng)相比較更適合目前的大數(shù)據(jù)時代，但分布式系統(tǒng)目前也存在一些缺點亟需解決，比如在可能出現(xiàn)故障的各節(jié)點間保證同一數(shù)據(jù)的多個副本的一致性問題。在分布式系統(tǒng)中，有很多復(fù)雜的理論，從CAP理論［1］到BASE理論［2］，學(xué)者們不斷地在可用性以及一致性之間做出權(quán)衡，就分布式一致性而言，又有許多協(xié)議，如從Paxos 算法［3］到ZAB 協(xié)議［4］，再到Raft 共識協(xié)議［5］（以下簡稱Raft 協(xié)議或Raft 算法）。Raft 協(xié)議是目前分布式系統(tǒng)中常見且有效的共識算法，因此穩(wěn)定可靠的Raft算法能夠保證分布式系統(tǒng)的數(shù)據(jù)一致性以及高效運轉(zhuǎn)。概率模型檢測［6］是一種高度自動化的形式化驗證技術(shù)，基于數(shù)學(xué)理論依據(jù)和模型檢測工具對具體的計算機系統(tǒng)抽象建模并分析驗證，在軟件開發(fā)、博弈論、生物工程、通信協(xié)議和網(wǎng)絡(luò)安全等領(lǐng)域都有大量成果。概率模型檢測作為模型檢測技術(shù)里的重要分支，近年來在各形式化驗證領(lǐng)域都有了顯著的研究結(jié)果。任勝兵等人［7］設(shè)計了基于概率模型檢測的軟件缺陷定位算法，用于缺陷定位分析。Mohsin等人［8］使用概率模型檢測來評估并分析了物聯(lián)網(wǎng)中由于不同的配置部署，而帶來的不同級別的安全風險，并通過模型計算出每個配置的可能性與攻擊者的成本。王晶等人［9］使用概率模型檢測方法對Web 服務(wù)組合進行了建模，定量分析并驗證了Web服務(wù)組合的有效性和可靠性。

本文使用概率模型檢測技術(shù)對分布式系統(tǒng)中的Raft協(xié)議進行形式化建模，并用概率計算樹邏輯表達式描述要檢測的性質(zhì)，對該協(xié)議的一致性與高效性進行定量分析，最終對驗證結(jié)果進行分析與討論。

目前，已有學(xué)者對Raft算法的形式化驗證進行了一些相關(guān)的工作。Schultz 等人［10］對基于Raft 協(xié)議的復(fù)制系統(tǒng)的重新配置協(xié)議進行了形式化驗證，并使用TLA+ 和TLAPS（TLA+ 證明系統(tǒng)）來形式化和機械驗證協(xié)議中的歸納不變量和安全證明。Woos 等人［11］對Raft 協(xié)議的狀態(tài)機安全性進行形式化驗證，并提出了一種在驗證過程中證明不變量的方法。周浩洋［12］使用形式化方法對共識算法PBFT 進行形式化建模，驗證并分析了協(xié)議的安全性，并提出了改變參與協(xié)議執(zhí)行的節(jié)點數(shù)量來探究協(xié)議容錯性上限的方法。顧佳儀［13］使用概率模型檢測對動態(tài)系統(tǒng)領(lǐng)導(dǎo)者選舉協(xié)議進行分析與驗證，在模型構(gòu)建的過程中，引入了“假設(shè)-保證”的組合式驗證思想，將層次式協(xié)議進行分別處理，建立了一個具有雙層結(jié)構(gòu)的領(lǐng)導(dǎo)者選舉協(xié)議模型，并通過實驗，得出了結(jié)果，顯示了模型的有效性。Evrard［14］使用LNT 過程代數(shù)對Raft 協(xié)議進行建模，指出了Raft 算法的原始TLA+規(guī)范存在的一些問題，并討論了如何最好地使用LNT 形式語言的特性和相關(guān)的CADP 驗證工具箱來模擬分布式協(xié)議，包括網(wǎng)絡(luò)和服務(wù)器故障。

1 相關(guān)基礎(chǔ)知識

1.1 Raft協(xié)議

Raft 協(xié)議是一種用于管理狀態(tài)復(fù)制機集群的復(fù)制日志算法［15］。Raft集群包含多個服務(wù)器，在任何給定的時刻，每個服務(wù)器都處于以下3種角色之一：領(lǐng)導(dǎo)者（Leader）、候選者（Candidate）和追隨者（Follower）：

1）Follower：每個服務(wù)器的初始角色，主要負責執(zhí)行來自Leader 的指令。如果收到客戶端的操作請求會轉(zhuǎn)發(fā)給Leader。

2）Candidate：這是一個過渡角色，如果Follower在一定的時間沒有接收到Leader的心跳，此時進入領(lǐng)導(dǎo)者選舉，本節(jié)點切換為Candidate，直到選舉結(jié)束。

3）Leader：整個集群中只有一臺服務(wù)器是Leader，主要負責處理客戶端的所有請求，并發(fā)送指令給所有Follower。它們之間的轉(zhuǎn)換關(guān)系如圖1所示。

圖1 Raft協(xié)議中角色轉(zhuǎn)換

Raft 算法中是以任期（Term）為時間單位，如圖2所示，每個任期都會以領(lǐng)導(dǎo)者選舉開始，選舉成功后，領(lǐng)導(dǎo)者會管理這個任期內(nèi)的所有操作直到任期結(jié)束。在某些情況下，選舉會導(dǎo)致分裂投票。此時，任期將在沒有領(lǐng)導(dǎo)者的情況下結(jié)束，緊接著會開始下一個新的任期。Raft 算法確保在給定的任期內(nèi)最多有一個領(lǐng)導(dǎo)者。

圖2 Raft協(xié)議的任期

1.2 概率模型檢測

1.2.1 連續(xù)時間的馬爾可夫鏈

連續(xù)時間馬爾可夫鏈［16］（Continuous-Time Markov Chain，CTMC）擴展了DTMC［17］，使得CTMC可以描述狀態(tài)遷移隨時間連續(xù)變化的系統(tǒng)。

CTMC 的狀態(tài)轉(zhuǎn)換只有在R（s）＞0 的情況下發(fā)生，在這種情況下，t個單位時間內(nèi)觸發(fā)狀態(tài)轉(zhuǎn)換的概率為1-e-R（s，s'）·t。當一個狀態(tài)中有多個可能的轉(zhuǎn)換可用時，就會發(fā)生競爭狀況。引入出逃率E（s）來表示狀態(tài)遷移的概率，s∈S，如果E（s）=0，則狀態(tài)s為吸收狀態(tài)，表示狀態(tài)s沒有對外發(fā)生遷移。因此狀態(tài)s遷移到的概率為：

1.2.2 概率計算樹邏輯

概率計算樹邏輯（PCTL）［18-19］是一個著名的概率時間邏輯，也是計算樹邏輯（CTL）［20］的擴展。PCTL是能夠定量描述概率系統(tǒng)的時序命題。

定義2 PCTL語法表示如下：狀態(tài)公式：

?∶∶=true| |

a ?1∧?2| |

?? p～p(φ)

路徑公式：

ψ∶∶=X?|?1∪?2|F ?|G ?|?1W ?2|?1R ?2

其中，a是一個原子命題；p是概率界限值；X（next）表示路徑的下一個狀態(tài)；U（until）表示某狀態(tài)直到另一狀態(tài)；F（future）表示某狀態(tài)在結(jié)束時的狀態(tài)；G（globally）表示某狀態(tài)直到結(jié)束時的狀態(tài)；W（weak until）是U的變體，相當于?1U ?2|G?1，要求?1直到?2前永遠為真；R（release）相當于!(!?1U!?2)，表示?2在?1變?yōu)檎嬷耙恢睘檎妗?/p>

1.2.3 概率模型檢測工具

PRISM 是由牛津大學(xué)Kwiatkowska 教授課題組開發(fā)的概率模型檢測工具［21］，它可以對具有隨機行為的系統(tǒng)進行自動驗證。圖3 是PRISM 工具的工作過程。

圖3 PRISM工作過程

PRISM 建模語言是一種基于狀態(tài)的描述性語言，它的基本組成部分是模塊和變量。其語法結(jié)構(gòu)如下所示：

其中，guard 是模型中變量的謂詞邏輯；upi描述了一個狀態(tài)轉(zhuǎn)換，如果guard 為真，模塊可以進行狀態(tài)轉(zhuǎn)換；pi表示當前轉(zhuǎn)換的概率（或速率）；action 可以是為了對轉(zhuǎn)換進行注釋，或者可以是為了同步。

2 Raft協(xié)議建模與分析

Raft 算法中Leader 負責處理客戶端的所有請求，以及將日志分發(fā)給其他Followers，本章將詳細介紹領(lǐng)導(dǎo)者選舉過程的形式化建模與分析。

2.1 Raft協(xié)議建模

領(lǐng)導(dǎo)者選舉采用投票機制，只要某個Candidate得到大多數(shù)Follower的支持，那它就能成為Leader，并開始向客戶端提供服務(wù)。單個任期中的領(lǐng)導(dǎo)者選舉流程如圖4所示。

圖4 單個Term內(nèi)領(lǐng)導(dǎo)者選舉流程

其中，ID表示集群中某臺服務(wù)器的唯一身份碼，CID表示Candidate 的ID，LogIndex 表示最新日志的標號，Term表示當前領(lǐng)導(dǎo)者的任期，voteResult表示Follower的投票結(jié)果。當Follower 收到投票申請時，會比較自身的最新日志序號與Candidate 的日志序號，如果自身日志舊或是一樣新則投贊同票，否則投反對票，并告知當前Candidate：日志不是最新的，宣告本輪選舉失敗。最后Candidate 只有獲得大部分的贊同票才能當選成功。單輪選舉具體流程見圖5。

圖5 Raft協(xié)議領(lǐng)導(dǎo)者選舉流程

Raft協(xié)議中每個任期都是連續(xù)遞增，并且在一個任期內(nèi)所進行的操作都是領(lǐng)導(dǎo)者選舉和處理日志復(fù)制的，因此將Raft協(xié)議建模為連續(xù)時間的馬爾可夫鏈模型，其中各個模塊的變量定義見表1。

表1 領(lǐng)導(dǎo)者選舉變量定義

定義整個模型到達選舉成功（有且僅有一個領(lǐng)導(dǎo)者）的狀態(tài)如下：

label “success” = leader=true & phase=4 &state1=2 & state2=2 & state3=2 & state4=2 &state5=2

使用PRISM 語言描述跟隨者模塊如算法1 所示，其中vote 動作是模擬跟隨者進行投票表決；retry命令表示當前Candidate 沒能當選成功，需要接受新的Candidate的投票請求。

算法1 Follower模塊核心代碼

module Follower1 ［vote］ state1=1 & phase=2 -＞voteProbability ：（voteResult1'=（logIndex1<=candidateLogIndex））&（state1'=2）+（1-voteProbability）：（voteResult1'=false）&（state1'=2）；［retry］phase=3 & !leader -＞（state1'=1）；endmodule

候選者模塊的建模如算法2 所示，其中round 動作標志選舉開始，后面也會用來記錄回合數(shù)；request動作用來模擬當集群中沒有Leader時，隨機選擇一個節(jié)點發(fā)起投票請求；retry動作表示當本輪選舉的贊同票數(shù)沒有過半時，重新進行下一輪選舉；done 命令表示選舉成功，當前Candidate_ID 擔任集群的領(lǐng)導(dǎo)者；最后3 行代碼表示概率模型檢測中的獎勵機制，為每個候選者發(fā)起投票請求時分配1的獎勵。

算法2 候選者模塊核心代碼

module Candidate

…

［round］phase=0 -＞（phase'=1）&（leader'=false）；

［request］phase=1 & end_init -＞1/N ：（phase'=2）&（candidateLogIndex'=logIndex1）+ …+ 1/N ：（phase'=2）&（candidate-LogIndex'=logIndex5）；

…

［retry］phase=3 & num_ticket

［done］phase=3 & num_ticket＞=N -＞（phase'=4）&（leader'=true）；endmodule

rewards“rounds”

［round］phase=0：1；endrewards

PRISM建模結(jié)果如算法3所示。

算法3 Raft協(xié)議建模日志

Model constants：K=8，voteProbability=0.5

Computing reachable states...

Reachability（BFS）：9 iterations in 0.03 seconds （average 0.003222，setup 0.00）

Time for model construction：0.239 seconds.

Type：CTMC

States：8476782（1 initial）

Transitions：38004665

Rate matrix：58992 nodes（12 terminal），38004665 minterms，vars：38r/38c

2.2 Raft協(xié)議分析

本節(jié)將對Raft協(xié)議領(lǐng)導(dǎo)者選舉的有效性、時效性以及通過選舉的回合數(shù)對選舉所耗時間進行定量分析。

屬性1 有效性。領(lǐng)導(dǎo)者選舉的有效性是指保證能夠在一定時間內(nèi)選舉出一個領(lǐng)導(dǎo)者。本文實驗將從跟隨者回復(fù)成功率與集群節(jié)點數(shù)2 個維度驗證Raft協(xié)議中領(lǐng)導(dǎo)者選舉過程的有效性。

驗證各種回復(fù)成功率的情況下是否能達到穩(wěn)定狀態(tài)，使用PCTL表達式描述如下：

P≥1［F“success”］

從圖6可以得知，當voteProbability＞0 時，模型最終到達選舉成功的狀態(tài)概率≥1。

圖6 跟隨者回復(fù)率對有效性的影響

下面驗證集群中節(jié)點數(shù)對達到選舉成功狀態(tài)的影響；由于概率模型檢測中的狀態(tài)爆炸問題［22-23］的存在，所以本次僅模擬節(jié)點數(shù)達到7，屬性的PCTL 表達式描述如下：

P=？［F“success”］

由圖7 可知，當N=3|5|7 時，它們的概率變化曲線一樣，換言之，集群中節(jié)點個數(shù)并不影響模型達到選舉成功的狀態(tài)。

圖7 節(jié)點數(shù)對有效性的影響

綜合上述2 個驗證實驗可知，只要有跟隨者能對此次投票進行表決（voteProbability＞0），Raft 協(xié)議就能保證一定能選出唯一的領(lǐng)導(dǎo)者，即滿足有效性。

屬性2 時效性。時效性是領(lǐng)導(dǎo)者選舉過程中的衡量資源消耗的一個重要指標。如果選舉過程較長，會使整個集群的服務(wù)效率大大降低，從而影響系統(tǒng)的效率和用戶滿意度。本次實驗利用選舉的回合數(shù)（rounds）來模擬從開始選舉到選舉成功所需時間。

首先驗證前T個單位時間內(nèi)，不同的回復(fù)成功率下所需rounds的總數(shù)量，利用PCTL表達式描述如下：

R{“rounds”}=？［C≤T］

由圖8 中變化曲線可知，跟隨者回復(fù)成功率越高，模型達到success 狀態(tài)所需的單位時間越少；當T≥50 時，選舉成功率≥0.5 的所需rounds 明顯減少，且都能達到success狀態(tài)。

圖8 投票成功率對選舉回合數(shù)的影響

Raft 協(xié)議規(guī)定各節(jié)點的本地狀態(tài)機上的日志序號連續(xù)遞增，并且跟隨者的日志不會比領(lǐng)導(dǎo)者的新，因此在選舉過程中，一定是日志最新的節(jié)點當選領(lǐng)導(dǎo)者，所以本次實驗將驗證各節(jié)點最新日志的范圍對選舉回合數(shù)的影響。為了盡量排除跟隨者回復(fù)率對實驗的影響，本次實驗取voteProbability≥0.5，單位時間T∈［0，50］。屬性描述如下：

R{“rounds”}=？［F“success”］

其中，K表示最新日志范圍，即 logIndex_maxlogIndex_min；由圖9可知：K值越大，模型達到success狀態(tài)的回合數(shù)就多。

圖9 日志范圍對選舉回合數(shù)的影響

結(jié)合上述2 個實驗可知，當節(jié)點回復(fù)成功率大于或等于0.5 時，能選舉出唯一的領(lǐng)導(dǎo)者平均也需要2～3 回合，但這是不可避免的，因為分布式系統(tǒng)中單點故障是客觀存在的；而對于日志范圍較大的情況下，所需選舉的回合數(shù)還會持續(xù)增加，原因就是由于每次選舉都是隨機產(chǎn)生的，并且可能會出現(xiàn)同一選舉周期內(nèi)，候選者重復(fù)提交選舉申請。

3 結(jié)束語

隨著分布式系統(tǒng)的快速發(fā)展，使各節(jié)點在可能出現(xiàn)故障的情況下，依然能對同一數(shù)據(jù)的多個副本保持一致就成為了影響整個分布式系統(tǒng)運行的關(guān)鍵一環(huán)，本文通過概率模型檢測技術(shù)對解決分布式系統(tǒng)數(shù)據(jù)一致性問題的Raft協(xié)議進行建模與分析，發(fā)現(xiàn)Raft協(xié)議能夠有效地解決某一時間內(nèi)數(shù)據(jù)一致性，然而在投票選舉中，隨著最新日志序號的范圍不斷增大，所需的選舉回合數(shù)也會增加，即選舉時間會變長，從而影響系統(tǒng)效率。相比于何東煉等人［27］使用模型檢測技術(shù)去驗證分布式協(xié)議的研究，本文采用概率模型檢測技術(shù)可以量化地表示分布式協(xié)議的設(shè)計和運行指標，從而使得協(xié)議逐步完善，以滿足設(shè)計所需；且本文采取分階段建模方法，化繁為簡，驗證了分布式協(xié)議算法中的核心選舉階段，從而提出了Raft協(xié)議在選舉階段所需回合數(shù)較多，耗時較長。因此本文的工作可以給Raft協(xié)議選舉階段的優(yōu)化提供參考方案，通過優(yōu)化Raft 協(xié)議選舉階段的選舉回合數(shù)來提高Raft 協(xié)議的執(zhí)行效率。下一步工作可以進一步分析和優(yōu)化Raft協(xié)議選舉階段，然后進行實驗驗證。