主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公English
2022年专刊出版计划 微信服务介绍 最新一期:2021年第2期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
谷晓松,魏恒峰,乔磊,黄宇.支持乱序执行的Raft协议.软件学报,2021,32(6):23-0
支持乱序执行的Raft协议
Raft with Out-of-Order Executions
投稿时间:2020-08-30  修订日期:2021-01-18
DOI:10.13328/j.cnki.jos.006248
中文关键词:  Raft  ParallelRaft  Multi-Paxos  共识协议  TLA+  精化关系  模型检验
英文关键词:Raft  ParallelRaft  Multi-Paxos  consensus protocols  TLA+  refinement mapping  model checking
基金项目:国家自然科学基金(61932021,61772258);五〇二所空间先进计算与电子信息专业实验室开放基金(OBCandETL-2020-04)
作者单位E-mail
谷晓松 计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023  
魏恒峰 计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023 hfwei@nju.edu.cn 
乔磊 北京控制工程研究所, 北京 100190 fly2moon@aliyun.com 
黄宇 计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023  
摘要点击次数: 43
全文下载次数: 30
中文摘要:
      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的正确性.
英文摘要:
      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. We aim to provide a precise formal specification for ParallelRaft and prove its correctness. Specifically, we make the following main contributions:First, to clarify the relationship between Raft and ParallelRaft, we proposed ParallelRaft-SE (Sequential Execution), which allows out-of-order commitment but prohibits out-of-order executions. We also established a refinement mapping from ParallelRaft-SE to Multi-Paxos. Second, we 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, we proposed ParallelRaft-CE (Concurrent Execution). 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. We proved the correctness of ParallelRaft-CE manually. Finally, we provided the formal specifications of ParallelRaft-SE and ParallelRaft-CE using TLA+ (TLA stands for Temporal Logic of Actions), and verified the refinement mapping from ParallelRaft-SE to Multi-Paxos and the correctness of ParallelRaft-CE using the TLC model checker when the number of participants of the protocols is small.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利