![点击分享此内容可以赚币 分享](/master/images/share_but.png)
基于概率模型的Raft协议形式化验证.pdf
《基于概率模型的Raft协议形式化验证.pdf》由会员分享,可在线阅读,更多相关《基于概率模型的Raft协议形式化验证.pdf(6页珍藏版)》请在咨信网上搜索。
1、计算机与现代化JISUANJI YU XIANDAIHUA2023年第9期总第337期文章编号:1006-2475(2023)09-0077-05收稿日期:2022-09-22;修回日期:2022-11-09基金项目:广东省自然科学基金资助项目(2020A1515010445)作者简介:管金平(1997),男,湖南衡阳人,硕士研究生,研究方向:模型检测,协议验证,E-mail:;通信作者:杨晋吉(1968),男,教授,博士,研究方向:模型检测,协议验证,E-mail:;杨成龙(1996),男,硕士研究生,研究方向:模型检测协议验证。0引言随着Internet的迅速发展,分布式系统应用也越来越广
2、泛。它与传统的集中式系统相比较更适合目前的大数据时代,但分布式系统目前也存在一些缺点亟需解决,比如在可能出现故障的各节点间保证同一数据的多个副本的一致性问题。在分布式系统中,有很多复杂的理论,从CAP理论1到BASE理论2,学者们不断地在可用性以及一致性之间做出权衡,就分布式一致性而言,又有许多协议,如从 Paxos算法3到ZAB 协议4,再到 Raft共识协议5(以下简称 Raft协议或Raft算法)。Raft协议是目前分布式系统中常见且有效的共识算法,因此稳定可靠的Raft算法能够保证分布式系统的数据一致性以及高效运转。概率模型检测6是一种高度自动化的形式化验证技术,基于数学理论依据和模型
3、检测工具对具体的计算机系统抽象建模并分析验证,在软件开发、博弈论、生物工程、通信协议和网络安全等领域都有大量成果。概率模型检测作为模型检测技术里的重要分支,近年来在各形式化验证领域都有了显著的研究结果。任胜兵等人7设计了基于概率模型检测的软件缺陷定位算法,用于缺陷定位分析。Mohsin等人8使用概率模型检测来评估并分析了物联网中由于不同的配置部署,而带来的不同级别的安全风险,并通过模型计算出每个配置的可能性与攻击者的成本。王晶等人9使用概率模型检测方法对Web服务组合进行了建模,定量分析并验证了Web服务组合的有效性和可靠性。本文使用概率模型检测技术对分布式系统中的Raft协议进行形式化建模,
4、并用概率计算树逻辑表达式描述要检测的性质,对该协议的一致性与高效性进基于概率模型的Raft协议形式化验证管金平,杨晋吉,杨成龙(华南师范大学计算机学院,广东 广州 510631)摘要:共识协议作为分布式系统的关键要素和核心组件,用于解决分布式场景下可能出现故障的节点间保证同一数据一致的问题,其准确性和高效性直接决定了系统的性能。Raft共识协议是目前分布式系统中常见且有效的算法。本文首先使用概率模型检测方法对Raft共识协议进行形式化建模,然后利用概率模型检测的属性规约技术对它的相关属性进行描述,最后通过模型检测工具验证并分析Raft共识协议的一致性和高效性。实验结果表明,Raft共识协议满足
5、一致性,但是在领导者选举阶段,当跟随者维护的最新日志序号的差值范围增加时,选举回合数也会增多,使得整个服务周期选举时间增加,从而影响协议的执行效率。关键词:分布式系统;Raft共识协议;概率模型检测;形式化验证;属性规约中图分类号:TP391文献标志码:ADOI:10.3969/j.issn.1006-2475.2023.09.012Formal Verification of Raft Protocol Based on Probabilistic ModelGUAN Jin-ping,YANG Jin-ji,YANG Cheng-long(School of Computer Scienc
6、e,South China Normal University,Guangzhou 510631,China)Abstract:Consensus protocol is important element and core component of distributed system,it is dedicated to solve the problem of ensuring the same data consistency among nodes that may fail in a distributed scenario,and its accuracy and efficie
7、ncy directly determine the performance of the system.Raft consensus protocol is common and effective consensus algorithm in currentdistributed systems.This paper firstly models the Raft consensus protocol formally using a probabilistic model detection method,then describes its relevant properties us
8、ing property spcification technique of probabilistic model checking,and finally verifiesand analyses the consistency and efficiency of the Raft consensus protocol.The experimental results show that it satisfies consistency,but the number of election rounds increases during the leader election phase
9、when the difference range of the latest log serial numbers maintained by followers increases,resulting in the election time increase throughout the service cycle,thus affecting the execution efficiency of Raft.Key words:distributed system;Raft consensus protocol;probabilistic model checking;formal v
10、erification;property specification计算机与现代化2023年第9期行定量分析,最终对验证结果进行分析与讨论。目前,已有学者对Raft算法的形式化验证进行了一些相关的工作。Schultz等人10对基于Raft协议的复制系统的重新配置协议进行了形式化验证,并使用 TLA+和 TLAPS(TLA+证明系统)来形式化和机械验证协议中的归纳不变量和安全证明。Woos 等人11对Raft协议的状态机安全性进行形式化验证,并提出了一种在验证过程中证明不变量的方法。周浩洋12使用形式化方法对共识算法PBFT进行形式化建模,验证并分析了协议的安全性,并提出了改变参与协议执行的节点
11、数量来探究协议容错性上限的方法。顾佳仪13使用概率模型检测对动态系统领导者选举协议进行分析与验证,在模型构建的过程中,引入了“假设-保证”的组合式验证思想,将层次式协议进行分别处理,建立了一个具有双层结构的领导者选举协议模型,并通过实验,得出了结果,显示了模型的有效性。Evrard14使用LNT过程代数对Raft协议进行建模,指出了Raft算法的原始TLA+规范存在的一些问题,并讨论了如何最好地使用 LNT形式语言的特性和相关的 CADP 验证工具箱来模拟分布式协议,包括网络和服务器故障。1相关基础知识1.1Raft协议Raft协议是一种用于管理状态复制机集群的复制日志算法15。Raft集群包
12、含多个服务器,在任何给定的时刻,每个服务器都处于以下3种角色之一:领导者(Leader)、候选者(Candidate)和追随者(Follower):1)Follower:每个服务器的初始角色,主要负责执行来自Leader的指令。如果收到客户端的操作请求会转发给 Leader。2)Candidate:这是一个过渡角色,如果 Follower在一定的时间没有接收到 Leader的心跳,此时进入领导者选举,本节点切换为Candidate,直到选举结束。3)Leader:整个集群中只有一台服务器是Leader,主要负责处理客户端的所有请求,并发送指令给所有Follower。它们之间的转换关系如图1所示
13、。图1Raft协议中角色转换Raft算法中是以任期(Term)为时间单位,如图2所示,每个任期都会以领导者选举开始,选举成功后,领导者会管理这个任期内的所有操作直到任期结束。在某些情况下,选举会导致分裂投票。此时,任期将在没有领导者的情况下结束,紧接着会开始下一个新的任期。Raft算法确保在给定的任期内最多有一个领导者。图2Raft协议的任期1.2概率模型检测1.2.1连续时间的马尔可夫链连续时间马尔可夫链16(Continuous-Time Markov Chain,CTMC)扩展了DTMC17,使得CTMC可以描述状态迁移随时间连续变化的系统。定义1连续时间的马尔可链定义为C=,其中:S是
14、非空有限状态集;s是初始状态,且sS;R:SSR+是迁移比率函数;AP是一个原子谓词集合;:S2AP是状态映射到AP的标记函数。CTMC的状态转换只有在R(s,s)0的情况下发生,在这种情况下,t个单位时间内触发状态转换的概率为1-e-R(s,s)t。当一个状态中有多个可能的转换可用时,就会发生竞争状况。引入出逃率E(s)来表示状态迁移的概率 E(s)=defssR(s,s)=1,sS,如果 E(s)=0,则状态s为吸收状态,表示状态s没有对外发生迁移。因此状态s迁移到s的概率为:P(s,s)=R(s,s)E(s),E(s)01,E(s)=0且 s=s0,其他1.2.2概率计算树逻辑概率计算树
15、逻辑(PCTL)18-19是一个著名的概率时间逻辑,也是计算树逻辑(CTL)20的扩展。PCTL是能够定量描述概率系统的时序命题。定义2PCTL语法表示如下:状态公式:=true|a 12|pp()路径公式:=X|12|F|G|1W 2|1R 2其中,a是一个原子命题;p是概率界限值;X(next)表示路径的下一个状态;U(until)表示某状态直到另一状态;F(future)表示某状态在结束时的状态;G(globally)表示某状态直到结束时的状态;W(weak until)是U的变体,相当于1U 2|G1,要求1直到2前永远为真;R(release)相当于!(!1U!2),表示2在1变为真
16、之前一直为真。1.2.3概率模型检测工具PRISM是由牛津大学 Kwiatkowska 教授课题组开发的概率模型检测工具21,它可以对具有随机行为的系统进行自动验证。图3是PRISM工具的工作过程。PRISM建模语言是一种基于状态的描述性语言,它的基本组成部分是模块和变量。其语法结构如下所示:跟随者候选者领导者跟随者跟随者开始超时时间片到,开始选举选举超时,开始新一轮收到大多数赞同的选票发现新的领导者或更高任期发现其他服务器有更高的任期Term1Term2Term3Term4Terms选举正常操作选举被分裂782023年第9期actionguard(p1:up1)+(pn:upn)其中,gua
17、rd是模型中变量的谓词逻辑;upi描述了一个状态转换,如果 guard为真,模块可以进行状态转换;pi表示当前转换的概率(或速率);action可以是为了对转换进行注释,或者可以是为了同步。图3PRISM工作过程2Raft协议建模与分析Raft算法中Leader负责处理客户端的所有请求,以及将日志分发给其他Followers,本章将详细介绍领导者选举过程的形式化建模与分析。2.1Raft协议建模领导者选举采用投票机制,只要某个 Candidate得到大多数Follower的支持,那它就能成为Leader,并开始向客户端提供服务。单个任期中的领导者选举流程如图4所示。图4单个Term内领导者选举
18、流程Step1:CandidateFollower:RequestVoteRPC(CID,TermID,LogIndexID)Step2:FollowerCandidate:(voteResultID)其中,ID表示集群中某台服务器的唯一身份码,CID表示 Candidate 的 ID,LogIndex 表示最新日志的标号,Term表示当前领导者的任期,voteResult表示Follower的投票结果。当Follower收到投票申请时,会比较自身的最新日志序号与Candidate的日志序号,如果自身日志旧或是一样新则投赞同票,否则投反对票,并告知当前Candidate:日志不是最新的,宣告本
19、轮选举失败。最后Candidate只有获得大部分的赞同票才能当选成功。单轮选举具体流程见图5。Raft协议中每个任期都是连续递增,并且在一个任期内所进行的操作都是领导者选举和处理日志复制的,因此将Raft协议建模为连续时间的马尔可夫链模型,其中各个模块的变量定义见表1。定义整个模型到达选举成功(有且仅有一个领导者)的状态如下:label“success”=leader=true&phase=4&state1=2&state2=2&state3=2&state4=2&state5=2使用 PRISM 语言描述跟随者模块如算法 1 所示,其中vote动作是模拟跟随者进行投票表决;retry命令表示
20、当前Candidate没能当选成功,需要接受新的Candidate的投票请求。算法1Follower模块核心代码module Follower1 vote state1=1&phase=2-voteProbability:(voteResult1=(logIndex1C_logIndex赞同Candidate担任LeaderCandidate选举成功,担任Leader选票是否过半?当前Candidate日志不是最新,开始新一轮选举否是是否图5Raft协议领导者选举流程表1领导者选举变量定义变量名NKvoteProbabilityphasecandidateLogIndexleaderstate
21、logIndexvoteResult描述服务器节点数量日志序号范围跟随者回复成功率表示控制投票过程:0:初始化阶段1:Candidate发起选举投票2:Follower开始投票表决3:重新发起投票4:结束candidate的日志序号选举成功的标志:true:本次选举成功false:不成功,重新选举Follower的状态枚举:0:随机生成日志序号1:开始投票表决2:重新下一轮投票日志序号投票表决结果:0:不赞同1:赞同2:候选者日志不是最新的,终止本轮选举管金平,等:基于概率模型的Raft协议形式化验证79计算机与现代化2023年第9期+(1-voteProbability):(voteResu
22、lt1=false)&(state1=2);retryphase=3&!leader-(state1=1);endmodule候选者模块的建模如算法2所示,其中round动作标志选举开始,后面也会用来记录回合数;request动作用来模拟当集群中没有Leader时,随机选择一个节点发起投票请求;retry动作表示当本轮选举的赞同票数没有过半时,重新进行下一轮选举;done命令表示选举成功,当前 Candidate_ID担任集群的领导者;最后3行代码表示概率模型检测中的奖励机制,为每个候选者发起投票请求时分配1的奖励。算法2候选者模块核心代码module Candidateroundphase=
23、0-(phase=1)&(leader=false);request phase=1&end_init-1/N:(phase=2)&(candidateLogIndex=logIndex1)+1/N:(phase=2)&(candidateLogIndex=logIndex5);retryphase=3&num_ticket(phase=0);done phase=3&num_ticket=N-(phase=4)&(leader=true);endmodulerewards“rounds”roundphase=0:1;endrewardsPRISM建模结果如算法 3所示。算法3Raft协议建模
24、日志Model constants:K=8,voteProbability=0.5Computing reachable states.Reachability(BFS):9iterationsin0.03seconds(average0.003222,setup 0.00)Time for model construction:0.239 seconds.Type:CTMCStates:8476782(1 initial)Transitions:38004665Rate matrix:58992 nodes(12 terminal),38004665 minterms,vars:38r/38
25、c2.2Raft协议分析本节将对Raft协议领导者选举的有效性、时效性以及通过选举的回合数对选举所耗时间进行定量分析。属性1 有效性。领导者选举的有效性是指保证能够在一定时间内选举出一个领导者。本文实验将从跟随者回复成功率与集群节点数 2 个维度验证Raft协议中领导者选举过程的有效性。验证各种回复成功率的情况下是否能达到稳定状态,使用PCTL表达式描述如下:P1 F“success”从图6可以得知,当voteProbability0 时,模型最终到达选举成功的状态概率1。下面验证集群中节点数对达到选举成功状态的影响;由于概率模型检测中的状态爆炸问题22-23的存在,所以本次仅模拟节点数达到7
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 基于 概率 模型 Raft 协议 形式化 验证
![提示](https://www.zixin.com.cn/images/bang_tan.gif)
1、咨信平台为文档C2C交易模式,即用户上传的文档直接被用户下载,收益归上传人(含作者)所有;本站仅是提供信息存储空间和展示预览,仅对用户上传内容的表现方式做保护处理,对上载内容不做任何修改或编辑。所展示的作品文档包括内容和图片全部来源于网络用户和作者上传投稿,我们不确定上传用户享有完全著作权,根据《信息网络传播权保护条例》,如果侵犯了您的版权、权益或隐私,请联系我们,核实后会尽快下架及时删除,并可随时和客服了解处理情况,尊重保护知识产权我们共同努力。
2、文档的总页数、文档格式和文档大小以系统显示为准(内容中显示的页数不一定正确),网站客服只以系统显示的页数、文件格式、文档大小作为仲裁依据,平台无法对文档的真实性、完整性、权威性、准确性、专业性及其观点立场做任何保证或承诺,下载前须认真查看,确认无误后再购买,务必慎重购买;若有违法违纪将进行移交司法处理,若涉侵权平台将进行基本处罚并下架。
3、本站所有内容均由用户上传,付费前请自行鉴别,如您付费,意味着您已接受本站规则且自行承担风险,本站不进行额外附加服务,虚拟产品一经售出概不退款(未进行购买下载可退充值款),文档一经付费(服务费)、不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
4、如你看到网页展示的文档有www.zixin.com.cn水印,是因预览和防盗链等技术需要对页面进行转换压缩成图而已,我们并不对上传的文档进行任何编辑或修改,文档下载后都不会有水印标识(原文档上传前个别存留的除外),下载后原文更清晰;试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓;PPT和DOC文档可被视为“模板”,允许上传人保留章节、目录结构的情况下删减部份的内容;PDF文档不管是原文档转换或图片扫描而得,本站不作要求视为允许,下载前自行私信或留言给上传者【自信****多点】。
5、本文档所展示的图片、画像、字体、音乐的版权可能需版权方额外授权,请谨慎使用;网站提供的党政主题相关内容(国旗、国徽、党徽--等)目的在于配合国家政策宣传,仅限个人学习分享使用,禁止用于任何广告和商用目的。
6、文档遇到问题,请及时私信或留言给本站上传会员【自信****多点】,需本站解决可联系【 微信客服】、【 QQ客服】,若有其他问题请点击或扫码反馈【 服务填表】;文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“【 版权申诉】”(推荐),意见反馈和侵权处理邮箱:1219186828@qq.com;也可以拔打客服电话:4008-655-100;投诉/维权电话:4009-655-100。