基于概率模型的Raft协议形式化验证

管金平，杨晋吉，杨成龙

（华南师范大学计算机学院，广东 广州 510631）

0 引 言

随着Internet 的迅速发展，分布式系统应用也越来越广泛。它与传统的集中式系统相比较更适合目前的大数据时代，但分布式系统目前也存在一些缺点亟需解决，比如在可能出现故障的各节点间保证同一数据的多个副本的一致性问题。在分布式系统中，有很多复杂的理论，从CAP理论［1］到BASE理论［2］，学者们不断地在可用性以及一致性之间做出权衡，就分布式一致性而言，又有许多协议，如从Paxos 算法［3］到ZAB 协议［4］，再到Raft 共识协议［5］（以下简称Raft 协议或Raft 算法）。Raft 协议是目前分布式系统中常见且有效的共识算法，因此稳定可靠的Raft算法能够保证分布式系统的数据一致性以及高效运转。概率模型检测［6］是一种高度自动化的形式化验证技术，基于数学理论依据和模型检测工具对具体的计算机系统抽象建模并分析验证，在软件开发、博弈论、生物工程、通信协议和网络安全等领域都有大量成果。概率模型检测作为模型检测技术里的重要分支，近年来在各形式化验证领域都有了显著的研究结果。任胜兵等人［7］设计了基于概率模型检测的软件缺陷定位算法，用于缺陷定位分析。Mohsin等人［8］使用概率模型检测来评估并分析了物联网中由于不同的配置部署，而带来的不同级别的安全风险，并通过模型计算出每个配置的可能性与攻击者的成本。王晶等人［9］使用概率模型检测方法对Web 服务组合进行了建模，定量分析并验证了Web服务组合的有效性和可靠性。

本文使用概率模型检测技术对分布式系统中的Raft协议进行形式化建模，并用概率计算树逻辑表达式描述要检测的性质，对该协议的一致性与高效性进行定量分析，最终对验证结果进行分析与讨论。

目前，已有学者对Raft算法的形式化验证进行了一些相关的工作。Schultz 等人［10］对基于Raft 协议的复制系统的重新配置协议进行了形式化验证，并使用TLA+ 和TLAPS（TLA+ 证明系统）来形式化和机械验证协议中的归纳不变量和安全证明。Woos 等人［11］对Raft 协议的状态机安全性进行形式化验证，并提出了一种在验证过程中证明不变量的方法。周浩洋［12］使用形式化方法对共识算法PBFT 进行形式化建模，验证并分析了协议的安全性，并提出了改变参与协议执行的节点数量来探究协议容错性上限的方法。顾佳仪［13］使用概率模型检测对动态系统领导者选举协议进行分析与验证，在模型构建的过程中，引入了“假设-保证”的组合式验证思想，将层次式协议进行分别处理，建立了一个具有双层结构的领导者选举协议模型，并通过实验，得出了结果，显示了模型的有效性。Evrard［14］使用LNT 过程代数对Raft 协议进行建模，指出了Raft 算法的原始TLA+规范存在的一些问题，并讨论了如何最好地使用LNT 形式语言的特性和相关的CADP 验证工具箱来模拟分布式协议，包括网络和服务器故障。

1 相关基础知识

1.1 Raft协议

Raft 协议是一种用于管理状态复制机集群的复制日志算法［15］。Raft集群包含多个服务器，在任何给定的时刻，每个服务器都处于以下3种角色之一：领导者（Leader）、候选者（Candidate）和追随者（Follower）：

1）Follower：每个服务器的初始角色，主要负责执行来自Leader 的指令。如果收到客户端的操作请求会转发给Leader。

2）Candidate：这是一个过渡角色，如果Follower在一定的时间没有接收到Leader的心跳，此时进入领导者选举，本节点切换为Candidate，直到选举结束。

3）Leader：整个集群中只有一台服务器是Leader，主要负责处理客户端的所有请求，并发送指令给所有Follower。它们之间的转换关系如图1所示。

图1 Raft协议中角色转换

Raft 算法中是以任期（Term）为时间单位，如图2所示，每个任期都会以领导者选举开始，选举成功后，领导者会管理这个任期内的所有操作直到任期结束。在某些情况下，选举会导致分裂投票。此时，任期将在没有领导者的情况下结束，紧接着会开始下一个新的任期。Raft 算法确保在给定的任期内最多有一个领导者。

图2 Raft协议的任期

1.2 概率模型检测

1.2.1 连续时间的马尔可夫链

连续时间马尔可夫链［16］（Continuous-Time Markov Chain，CTMC）扩展了DTMC［17］，使得CTMC可以描述状态迁移随时间连续变化的系统。

CTMC 的状态转换只有在R（s）＞0 的情况下发生，在这种情况下，t个单位时间内触发状态转换的概率为1-e-R（s，s'）·t。当一个状态中有多个可能的转换可用时，就会发生竞争状况。引入出逃率E（s）来表示状态迁移的概率，s∈S，如果E（s）=0，则状态s为吸收状态，表示状态s没有对外发生迁移。因此状态s迁移到的概率为：

1.2.2 概率计算树逻辑

概率计算树逻辑（PCTL）［18-19］是一个著名的概率时间逻辑，也是计算树逻辑（CTL）［20］的扩展。PCTL是能够定量描述概率系统的时序命题。

定义2 PCTL语法表示如下：状态公式：

ϕ∶∶=true| |

a ϕ1∧ϕ2| |

¬ϕ p～p(φ)

路径公式：

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

其中，a是一个原子命题；p是概率界限值；X（next）表示路径的下一个状态；U（until）表示某状态直到另一状态；F（future）表示某状态在结束时的状态；G（globally）表示某状态直到结束时的状态；W（weak until）是U的变体，相当于ϕ1U ϕ2|Gϕ1，要求ϕ1直到ϕ2前永远为真；R（release）相当于!(!ϕ1U!ϕ2)，表示ϕ2在ϕ1变为真之前一直为真。

1.2.3 概率模型检测工具

PRISM 是由牛津大学Kwiatkowska 教授课题组开发的概率模型检测工具［21］，它可以对具有随机行为的系统进行自动验证。图3 是PRISM 工具的工作过程。

图3 PRISM工作过程

PRISM 建模语言是一种基于状态的描述性语言，它的基本组成部分是模块和变量。其语法结构如下所示：

其中，guard 是模型中变量的谓词逻辑；upi描述了一个状态转换，如果guard 为真，模块可以进行状态转换；pi表示当前转换的概率（或速率）；action 可以是为了对转换进行注释，或者可以是为了同步。

2 Raft协议建模与分析

Raft 算法中Leader 负责处理客户端的所有请求，以及将日志分发给其他Followers，本章将详细介绍领导者选举过程的形式化建模与分析。

2.1 Raft协议建模

领导者选举采用投票机制，只要某个Candidate得到大多数Follower的支持，那它就能成为Leader，并开始向客户端提供服务。单个任期中的领导者选举流程如图4所示。

图4 单个Term内领导者选举流程

其中，ID表示集群中某台服务器的唯一身份码，CID表示Candidate 的ID，LogIndex 表示最新日志的标号，Term表示当前领导者的任期，voteResult表示Follower的投票结果。当Follower 收到投票申请时，会比较自身的最新日志序号与Candidate 的日志序号，如果自身日志旧或是一样新则投赞同票，否则投反对票，并告知当前Candidate：日志不是最新的，宣告本轮选举失败。最后Candidate 只有获得大部分的赞同票才能当选成功。单轮选举具体流程见图5。

图5 Raft协议领导者选举流程

Raft协议中每个任期都是连续递增，并且在一个任期内所进行的操作都是领导者选举和处理日志复制的，因此将Raft协议建模为连续时间的马尔可夫链模型，其中各个模块的变量定义见表1。

表1 领导者选举变量定义

定义整个模型到达选举成功（有且仅有一个领导者）的状态如下：

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 动作标志选举开始，后面也会用来记录回合数；request动作用来模拟当集群中没有Leader时，随机选择一个节点发起投票请求；retry动作表示当本轮选举的赞同票数没有过半时，重新进行下一轮选举；done 命令表示选举成功，当前Candidate_ID 担任集群的领导者；最后3 行代码表示概率模型检测中的奖励机制，为每个候选者发起投票请求时分配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建模结果如算法3所示。

算法3 Raft协议建模日志

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协议分析

本节将对Raft协议领导者选举的有效性、时效性以及通过选举的回合数对选举所耗时间进行定量分析。

属性1 有效性。领导者选举的有效性是指保证能够在一定时间内选举出一个领导者。本文实验将从跟随者回复成功率与集群节点数2 个维度验证Raft协议中领导者选举过程的有效性。

验证各种回复成功率的情况下是否能达到稳定状态，使用PCTL表达式描述如下：

P≥1［F“success”］

从图6可以得知，当voteProbability＞0 时，模型最终到达选举成功的状态概率≥1。

图6 跟随者回复率对有效性的影响

下面验证集群中节点数对达到选举成功状态的影响；由于概率模型检测中的状态爆炸问题［22-23］的存在，所以本次仅模拟节点数达到7，属性的PCTL 表达式描述如下：

P=？［F“success”］

由图7 可知，当N=3|5|7 时，它们的概率变化曲线一样，换言之，集群中节点个数并不影响模型达到选举成功的状态。

图7 节点数对有效性的影响

综合上述2 个验证实验可知，只要有跟随者能对此次投票进行表决（voteProbability＞0），Raft 协议就能保证一定能选出唯一的领导者，即满足有效性。

属性2 时效性。时效性是领导者选举过程中的衡量资源消耗的一个重要指标。如果选举过程较长，会使整个集群的服务效率大大降低，从而影响系统的效率和用户满意度。本次实验利用选举的回合数（rounds）来模拟从开始选举到选举成功所需时间。

首先验证前T个单位时间内，不同的回复成功率下所需rounds的总数量，利用PCTL表达式描述如下：

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

由图8 中变化曲线可知，跟随者回复成功率越高，模型达到success 状态所需的单位时间越少；当T≥50 时，选举成功率≥0.5 的所需rounds 明显减少，且都能达到success状态。

图8 投票成功率对选举回合数的影响

Raft 协议规定各节点的本地状态机上的日志序号连续递增，并且跟随者的日志不会比领导者的新，因此在选举过程中，一定是日志最新的节点当选领导者，所以本次实验将验证各节点最新日志的范围对选举回合数的影响。为了尽量排除跟随者回复率对实验的影响，本次实验取voteProbability≥0.5，单位时间T∈［0，50］。属性描述如下：

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

其中，K表示最新日志范围，即 logIndex_maxlogIndex_min；由图9可知：K值越大，模型达到success状态的回合数就多。

图9 日志范围对选举回合数的影响

结合上述2 个实验可知，当节点回复成功率大于或等于0.5 时，能选举出唯一的领导者平均也需要2～3 回合，但这是不可避免的，因为分布式系统中单点故障是客观存在的；而对于日志范围较大的情况下，所需选举的回合数还会持续增加，原因就是由于每次选举都是随机产生的，并且可能会出现同一选举周期内，候选者重复提交选举申请。

3 结束语

随着分布式系统的快速发展，使各节点在可能出现故障的情况下，依然能对同一数据的多个副本保持一致就成为了影响整个分布式系统运行的关键一环，本文通过概率模型检测技术对解决分布式系统数据一致性问题的Raft协议进行建模与分析，发现Raft协议能够有效地解决某一时间内数据一致性，然而在投票选举中，随着最新日志序号的范围不断增大，所需的选举回合数也会增加，即选举时间会变长，从而影响系统效率。相比于何东炼等人［27］使用模型检测技术去验证分布式协议的研究，本文采用概率模型检测技术可以量化地表示分布式协议的设计和运行指标，从而使得协议逐步完善，以满足设计所需；且本文采取分阶段建模方法，化繁为简，验证了分布式协议算法中的核心选举阶段，从而提出了Raft协议在选举阶段所需回合数较多，耗时较长。因此本文的工作可以给Raft协议选举阶段的优化提供参考方案，通过优化Raft 协议选举阶段的选举回合数来提高Raft 协议的执行效率。下一步工作可以进一步分析和优化Raft协议选举阶段，然后进行实验验证。