删除或更新信息,请邮件至freekaoyan#163.com(#换成@)

支持乱序执行的Raft协议

本站小编 Free考研考试/2022-01-02

摘要:PolarFS是阿里巴巴开发的分布式文件系统,它实现了分布式共识协议Raft的一种变体,称为ParallelRaft.ParallelRaft突破了Raft中顺序提交、顺序执行的限制,允许状态机乱序执行用户命令.然而文献表明:ParallelRaft并未开源,仅有简短的文字描述,更缺乏严格的形式化规约.更进一步,它的正确性也尚未经过必要的数学论证或形式化检验.旨在为ParallelRaft提供严格的形式化规约并证明其正确性,主要贡献包括:首先,为了理清ParallelRaft与Raft之间的关系,提出了允许乱序提交、顺序执行的ParallelRaft-SE (sequential execution)协议,并建立了从ParallelRaft-SE到Multi-Paxos的精化关系;其次,现有的ParallelRaft描述忽略了可能会违反状态一致性的“幽灵日志”问题,因此在ParallelRaft-SE的基础上提出了ParallelRaft-CE (concurrent execution)协议.ParallelRaft-CE限制了ParallelRaft-SE在乱序提交阶段的并行度,避免了“幽灵日志”问题,支持乱序执行,并保证乱序执行下的状态机一致性.证明了ParallelRaft-CE的正确性.最后,使用TLA+给出了ParallelRaft-SE和ParallelRaft-CE的形式化规约,并对协议参与者数量较小的情形,使用TLC模型检验与模拟测试工具验证了从ParallelRaft-SE到Multi-Paxos的精化关系以及ParallelRaft-CE的正确性.



Abstract:PolarFS is a distributed file system developed by Alibaba Inc. with ultra-low latency and high availability. It implemented a variant of the Raft consensus protocol, called ParallelRaft. ParallelRaft breaks Raft's strict serialization restrictions in the commitment and execution of log entries and enables state machines to commit and execute log entries in an out-of-order way. However, ParallelRaft is not open-sourced. It has only a brief description, lacking formal specification. Moreover, the correctness of ParallelRaft has not been manually proven or formally checked. The purpose of the study is to provide a precise formal specification for ParallelRaft and to prove its correctness. Specifically, the following main contributions are accomplished. First, to clarify the relationship between Raft and ParallelRaft, ParallelRaft-SE (sequential execution) is proposed, which allows out-of-order commitment but prohibits out-of-order executions. Also, a refinement mapping from ParallelRaft-SE to Multi-Paxos is established. Second, it is discovered that ParallelRaft, according to its brief description in the literature, neglects the so-called "ghost log entries" phenomenon, which may violate the consistency among state machines. Therefore, based on ParallelRaft-SE, ParallelRaft-CE (concurrent execution) is proposed. ParallelRaft-CE avoids the "ghost log entries" phenomenon and ensures the consistency among state machine when executing concurrently by limiting parallelism in the commitment of log entries. The correctness of ParallelRaft-CE is proved manually. Finally, the formal specifications of ParallelRaft-SE and ParallelRaft-CE using TLA+ (TLA stands for temporal logic of actions) are provided, and the refinement mapping from ParallelRaft-SE to Multi-Paxos and the correctness of ParallelRaft-CE are verified using the TLC model checker when the number of participants of the protocols is small.



PDF全文下载地址:

http://www.jos.org.cn/jos/article/pdf/6248
相关话题/检验 数学 文献 规约 正确性

  • 领限时大额优惠券,享本站正版考研考试资料!
    大额优惠券
    优惠券领取后72小时内有效,10万种最新考研考试考证类电子打印资料任你选。涵盖全国500余所院校考研专业课、200多种职业资格考试、1100多种经典教材,产品类型包含电子书、题库、全套资料以及视频,无论您是考研复习、考证刷题,还是考前冲刺等,不同类型的产品可满足您学习上的不同需求。 ...
    本站小编 Free壹佰分学习网 2022-09-19
  • 基于偶然正确性概率的错误定位技术
    摘要:基于代码覆盖的错误定位技术是一种常用的错误定位方法,被用来识别与故障相关的程序元素.然而,有研究工作表明,基于代码覆盖的错误定位技术的有效性受到了偶然正确性现象的影响.偶然正确性现象是指程序中包含的错误被执行,但没有产生错误结果的情况,它在实际场景中是非常普遍的.根据以往的研究工作,提出了一种 ...
    本站小编 Free考研考试 2022-01-02
  • 协同业务过程的建模及正确性修正
    摘要:由自底向上建模方法建立的协同业务过程中通常存在不一致,故对其进行正确性分析是确保其正确实施的重要手段.现有方法大多关注正确性检测,这使得协同业务过程的正确性分析过程复杂且耗时.而正确性修正方法能够避免正确性检测方法中存在的重复检测和调整,但这方面的研究较少,不能有效地应用于协同业务过程修正.为 ...
    本站小编 Free考研考试 2022-01-02
  • 基于概率模型检验的云渲染任务调度定量验证
    摘要:云渲染技术已被广泛应用于影视和动漫等行业.与传统的渲染农场和租赁市场模式不同,云渲染系统依托云计算基础设施提供多种软件服务进行渲染作业的方式,正逐渐成为新兴的计算模式.由于任务执行和资源操作等作业调度对于用户而言是透明的,这要求云渲染系统应具备智能化以实现计算资源优化调度和多端任务管理,并对系 ...
    本站小编 Free考研考试 2022-01-02
  • 一种基于时变Petri网的服务组合质量检验方法
    摘要:为了解决动态服务组合过程中功能执行时序与工作流的关系问题,提出了一种基于时变Petri网技术的Web服务组合模型.引入Petri网有向网结构来描述组合过程中输入/输出功能及时间因素影响,以Petri网的有向弧结构表示服务组合过程中服务功能时间参数输入/输出表达式,利用时变函数表示服务的时间消耗 ...
    本站小编 Free考研考试 2022-01-02
  • 经验研究中情景感知需求获取与建模系统文献综述
    摘要:情景感知(contextaware)的应用是当前的一个研究热点,但是,由于情景的复杂性和不确定性,如何获取这些应用的需求面临着巨大挑战,需求工程领域出现了大量的研究来解决这一挑战.使用系统文献综述(systematicliteraturereview)的方法首先分析了不同情景维度对需求获取与建 ...
    本站小编 Free考研考试 2022-01-02
  • 沙尘预报客观检验中最优实况资料和圆插值半径选择研究
    摘要摘要:使用2012~2014年每年3~5月CUACE(ChinaMeteorologicalAdministrationUnifiedAtmosphericChemistryEnvironment)模式地面沙尘浓度格点预报产品,预报员预报等级产品、实况地面观测沙尘等级和特征站观测PM10(空气动 ...
    本站小编 Free考研考试 2022-01-02
  • 高阶<bold>Runge-Kutta-Li</bold>算法对二维线性平流方程的计算检验
    摘要摘要:利用高阶Li空间微分方案(Li,2005),实现了时间积分为3~6阶Runge-Kutta-Li(RKL)格式的求解算法。二维线性平流方程的试验结果表明:在计算稳定的条件下,各阶算法的计算误差随时间的推移基本上是线性增加的。非转动背景场的平流算例中(高斯型的初值),高阶RKL算法可以取得较 ...
    本站小编 Free考研考试 2022-01-02
  • 中国科学院软件研究所航天软件测评中心获颁《检验检测机构资质认定证书》
    1月26日,中国科学院软件研究所航天软件测评中心(以下简称航天软件测评中心)获得由国家认证认可监督管理委员会颁发的《检验检测机构资质认定证书》,标志着该中心正式获得了为社会出具相关检验检测报告或证书的行政许可。  航天软件测评中心经中国科学院软件研究所批准,于2020年3月19日成立。自成立以来,航 ...
    本站小编 Free考研考试 2022-01-02
  • 基于卫星降水和WRF预报降水的“6.18”门头沟泥石流事件的回报检验研究
    摘要摘要:2017年6月18日北京门头沟地区突发泥石流,造成6人伤亡。短时强降水是这起事件的主要诱发因素,但常规气象观测并没有很好地观测到此次降水过程,可见降水数据的准确性对于滑坡泥石流的实时预警及预报至关重要。近年来,卫星遥感估算降水发展迅速,WRF(WeatherResearchandForec ...
    本站小编 Free考研考试 2022-01-02
  • 基于文献整合的中国典型陆地生态系统初级生产力、呼吸和净生产力数据集
    摘要&关键词摘要:陆地生态系统与大气间的碳交换是重要的生物地球化学循环过程,包含了生态系统的光合生产和呼吸利用,直接决定了生态系统的物质资源生产、生物多样性维持以及气候调节等功能。本文收集整理了2000–2015年中国区域公开发表的生态系统碳交换通量的文献资料,构建了中国区域典型陆地生态系统生产力和 ...
    本站小编 Free考研考试 2022-01-02
闂傚倸鍊烽懗鍫曞箠閹捐瑙﹂悗锝庡墮閸ㄦ繈骞栧ǎ顒€濡肩痪鎯с偢閺屻劑鎮ら崒娑橆伓2濠电姷鏁搁崑鐐哄垂閸洖绠扮紒瀣紩濞差亜惟闁冲搫顑囩粙蹇涙⒑閸︻厼鍔嬫い銊ユ瀹曠敻鍩€椤掑嫭鈷戦柛娑橈工婵箑霉濠婂懎浠辩€规洘妞介弫鎾绘偐瀹曞洤骞橀梻浣告惈椤︻垶鎮樺┑瀣辈闁靛繈鍊栭悡鐔兼煥閺囨浜惧銈忓閺佸鐛崘鈺冾浄閻庯綆鍋掑Λ鍐ㄢ攽閻愭潙鐏︾痪鏉跨Ч楠炲濡堕崱娆戭啎闂佺懓顕崑鐐核夐弽顓熷仯濞撴艾锕﹂幃鍏间繆閸欏濮囬柍璇查叄楠炲洭宕滄担铏瑰幀濠电姷顣藉Σ鍛村垂闂堟稈鏋嶉柨婵嗘媼濞尖晠鏌曟繛鐐珕闁绘挶鍎茬换娑㈠箣閻愩劎绱伴梺缁樺浮閺€閬嶅Φ閸曨垼鏁冮柕蹇婃櫅閸撻亶姊洪幐搴b姇闁告梹鐟╅悰顔锯偓锝庡櫘閺佸秵绻濇繝鍌涘婵″弶鎸冲缁樻媴閸涢潧婀遍幑銏ゅ箛椤斿墽鐓嬮梺缁樺灱濡嫰宕归崒鐐寸厱鐎光偓閳ь剟宕戦悙鍝勭;闁靛ň鏅滈悡銉╂煟閺囩偛鈧湱鈧熬鎷�
濠电姷鏁告慨浼村垂瑜版帗鍋夐柕蹇嬪€曢悙濠勬喐瀹ュ棙鍙忛柕鍫濐槹閳锋垿鏌涘☉姗堝伐缂佹甯楁穱濠囶敃閿濆洦鍒涘銈冨灪濡啯鎱ㄩ埀顒勬煏閸繃锛嶆俊顐㈠閺岋絾鎯旈婊呅i梺鍝ュУ閻楃姴鐣烽姀銈呯妞ゆ梻鏅崢鎼佹⒑閸涘﹥绀嬫繛浣冲洦鍊堕柨婵嗘娴滄粓鏌熺€涙ḿ绠栧璺哄缁辨帞鈧綆浜跺Ο鈧梺绯曟杹閸嬫挸顪冮妶鍡楀潑闁稿鎹囬弻宥囨嫚閺屻儱寮板┑锟犵畺娴滃爼寮诲鍫闂佸憡鎸婚悷鈺佺暦椤栨稑顕遍悗娑櫭禍顖氣攽閻愬弶鈻曞ù婊勭箞瀵煡顢楅崟顒€鈧爼鏌i幇顔芥毄闁硅棄鍊块弻娑㈠Χ閸ヮ灝銏ゆ婢跺绡€濠电姴鍊搁弳锝嗐亜鎼淬埄娈曢柕鍥у閸╃偤顢橀悙宸痪婵犳鍨遍幐鎶藉蓟閿熺姴鐐婇柍杞扮劍閻忎線姊洪崨濠勬喛闁稿鎹囧缁樻媴閸濄儳楔濠电偘鍖犻崱鎰睏闂佺粯鍔楅弫鍝ョ不閺冨牊鐓欓柟顖嗗苯娈堕梺宕囩帛濮婂綊骞堥妸銉庣喓鎷犻幓鎺濇浇闂備焦鎮堕崐褏绮婚幘璇茶摕闁绘棁娅i惌娆撴煙缁嬪灝顒㈤柟顔界懇濮婄儤瀵煎▎鎴犘滅紓浣哄У閻楁洟顢氶敐澶樻晝闁冲灈鏅滈悗濠氭⒑瑜版帒浜伴柛妯哄⒔缁瑩宕熼娑掓嫼闂佸湱枪濞寸兘鍩ユ径鎰厸闁割偒鍋勬晶瀵糕偓瑙勬礀缂嶅﹥淇婂宀婃Ъ婵犳鍨伴妶鎼佸蓟濞戞ǚ妲堟慨妤€鐗婇弫鍓х磽娴e搫校閻㈩垳鍋ら崺鈧い鎺嗗亾闁诲繑鑹鹃…鍨潨閳ь剟骞冭瀹曞崬霉閺夋寧鍠樼€规洜枪铻栧ù锝夋櫜閻ヮ亪姊绘担渚敯闁规椿浜浠嬪礋椤栨稒娅栭梺鍝勭▉閸樹粙鎮¤箛娑欑厱闁斥晛鍟粈鈧銈忕岛閺嗘竼e濠电姷鏁告慨浼村垂閸︻厾绀婂┑鐘叉搐閻掑灚銇勯幒宥堝厡闁愁垱娲熼弻鏇㈠幢濡も偓閺嗭綁鏌$仦鍓ф创妤犵偞甯¢獮瀣倻閸℃﹩妫у┑锛勫亼閸婃牜鏁悙鍝勭獥闁归偊鍠氶惌娆忊攽閻樺弶澶勯柛瀣姍閺岋綁濮€閵忊剝姣勯柡浣哥墦濮婄粯鎷呯粙鎸庡€┑鐘灪閿曘垹鐣烽娑橆嚤閻庢稒锚娴滎垶姊洪崨濠勭畵濠殿垵椴搁幆鏃堝閿涘嫮肖婵$偑鍊栭崝妤呭窗鎼淬垻顩插Δ锝呭暞閻撴盯鏌涢妷锝呭闁汇劍鍨块弻锝夋偄閸欏鐝旈梺瀹犳椤︾敻鐛Ο鑲╃闁绘ê宕銏′繆閻愵亜鈧牕煤濠靛棌鏋嶉柡鍥╁亶缂傛岸鐓崶銊р槈鐎瑰憡绻冮妵鍕箻濡も偓閸燁垶顢欓敓锟�20婵犲痉鏉库偓妤佹叏閻戣棄纾婚柣妯款嚙缁犲灚銇勮箛鎾搭棡妞ゎ偅娲樼换婵嬫濞戝崬鍓扮紓浣哄У閸ㄥ潡寮婚妶鍡樺弿闁归偊鍏橀崑鎾澄旈埀顒勫煝閺冨牆顫呴柣妯烘閹虫捇銈导鏉戠闁冲搫锕ラ敍鍛磽閸屾瑧顦︽い锔诲灦椤㈡岸顢橀姀鐘靛姦濡炪倖宸婚崑鎾寸節閳ь剟鏌嗗鍛紱闂佺粯姊婚崢褔寮告笟鈧弻鏇㈠醇濠垫劖效闂佺ǹ楠哥粔褰掑蓟濞戙垹鍗抽柕濞垮劚椤晠姊烘导娆戠暠缂傚秴锕獮鍐ㄎ旈崘鈺佹瀭闂佸憡娲﹂崣搴ㄥ汲閿熺姵鈷戦柛婵嗗椤ユ垿鏌涚€n偅宕屾慨濠冩そ瀹曨偊宕熼崹顐嵮囨⒑閸涘﹥鈷愰柣妤冨█楠炲啴鏁撻悩铏珫闂佸憡娲﹂崜娆撴偟娴煎瓨鈷戦梻鍫熺〒缁犳岸鏌涢幘瀵哥疄闁诡喒鈧枼鏋庨柟閭﹀枤椤旀洘绻濋姀锝嗙【妞ゆ垵妫涚划鍫ュ焵椤掑嫭鍊垫繛鍫濈仢濞呭秹鏌¢埀顒勫础閻戝棗娈梺鍛婃处閸嬫帡宕ョ€n喗鐓曢柡鍥ュ妼楠炴ɑ淇婇崣澶婄伌婵﹥妞藉畷顐﹀礋椤愮喎浜惧ù鐘差儜缂嶆牕顭跨捄鐑樻拱闁稿繑绮撻弻娑㈩敃閿濆棛顦ㄩ梺鍝勬媼閸撶喖骞冨鈧幃娆撴濞戞顥氱紓鍌欒兌婵數鏁垾鎰佹綎濠电姵鑹鹃悙濠囨煥濠靛棙鍣稿瑙勬礋濮婃椽鎳¢妶鍛€惧┑鐐插级閸ㄥ潡骞婂Δ鍐╁磯閻炴稈鍓濋悘渚€姊虹涵鍛涧闂傚嫬瀚板畷鏇㈠箣閿旇棄鈧敻鏌ㄥ┑鍡涱€楁鐐瘁缚缁辨帡鎮╁畷鍥р拰闂佸搫澶囬崜婵嗩嚗閸曨偀妲堟繛鍡楁禋娴硷拷