软件学报

作者：谷晓松，魏恒峰，乔磊，黄宇

单位：谷晓松，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002311,魏恒峰，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002302,乔磊，北京控制工程研究所, 北京 10019003,黄宇，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002304

关键词：Raft;ParallelRaft;Multi-Paxos;共识协议;TLA+;精化关系;模型检验

基金：国家自然科学基金（61932021，61772258）；五〇二所空间先进计算与电子信息专业实验室开放基金（OBCandETL-2020-04）

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的正确性.

来源：2021年第6期

《软件学报》期刊编辑部

查看软件学报杂志2021年第6期