Page 174 - 《软件学报》2021年第6期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2021,32(6):1748−1778 [doi: 10.13328/j.cnki.jos.006248] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

∗
支持乱序执行的 Raft 协议

2
1
1
谷晓松 , 魏恒峰 , 乔 磊 , 黄 宇 1
1
(计算机软件新技术国家重点实验室(南京大学),江苏 南京 210023)
2 (北京控制工程研究所,北京 100190)
通讯作者: 魏恒峰, Email: hfwei@nju.edu.cn; 乔磊, Email: fly2moon@aliyun.com

摘 要: 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 的正确性.
关键词: Raft;ParallelRaft;Multi-Paxos;共识协议;TLA+;精化关系;模型检验
中图法分类号: TP311

中文引用格式: 谷晓松,魏恒峰,乔磊,黄宇.支持乱序执行的 Raft 协议.软件学报,2021,32(6):1748−1778. http://www.jos.org.cn/
1000-9825/6248.htm
英文引用格式: Gu XS, Wei HF, Qiao L, Huang Y. Raft with out-of-order executions. Ruan Jian Xue Bao/Journal of Software,
2021,32(6):1748−1778 (in Chinese). http://www.jos.org.cn/1000-9825/6248.htm

Raft with Out-of-order Executions

2
1
1
GU Xiao-Song , WEI Heng-Feng , QIAO Lei , HUANG Yu 1
1 (State Key Laboratory for Novel Software Technology (Nanjing University), Nanjing 210023, China)
2 (Beijing Institute of Control Engineering, Beijing 100190, China)
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

∗ 基金项目: 国家自然科学基金(61932021, 61772258); 五〇二所空间先进计算与电子信息专业实验室开放基金(OBCandETL-
2020-04)
Foundation item: National Natural Science Foundation of China (61932021, 61772258); Space Advanced Computing and Electronic
Information Laboratory of BICE (OBCandETL-2020-04)
本文由“形式化方法与应用”专题特约编辑邓玉欣教授推荐.
收稿时间: 2020-08-30; 修改时间: 2020-10-26, 2021-01-18; 采用时间: 2021-01-27; jos 在线出版时间: 2021-02-07