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

1776 Journal of Software 软件学报 Vol.32, No.6, June 2021

Fig.8 Simulation results of the consistency of ParallelRaft-CE
图 8 模拟模式验证 ParallelRaft-CE 满足一致性的验证结果

7 相关工作

经典分布式共识协议 Multi-Paxos(Paxos) [8,9] 衍生出了多种变体 [23,24] ,如 Disk Paxos [25] ,Cheap Paoxs [26] ,Fast
Paxos [27] ,Generalized Paxos [28] ,Stoppable Paxos [29] ,Vertical Paxos [30] ,Byzantine Paxos [31] ,EPaxos [32] ,TPaxos 等 [18] .
Multi-Paxos 支持乱序提交、顺序执行用户命令.Raft [10] 也可以看作 Multi-Paxos(Paxos)的变体 [33] ,它限制了乱序
提交行为,通过顺序提交、顺序执行用户命令简化了协议设计.本文关注分布式文件系统 PolarFS 使用的
[7]
ParallelRaft 协议 ,它基于 Raft 实现了乱序提交、乱序执行,更适用于高并发系统.为了理清 ParallelRaft 与 Raft
之间的关系,我们提出了 ParallelRaft-SE.ParallelRaft-SE 是 Multi-Paxos 的一种变体,支持乱序提交、顺序执行用
户命令.
利用无冲突命令之间的可交换性,可以提高共识协议的性能.在 Generalized Paxos [28] 中,如果命令无冲突,用
户可以绕过主节点,直接将命令广播给所有节点,减少通信开销、提高性能.微软公司提出的分布式复制框架
[7]
Tribble [34] 利用多线程技术并发执行无冲突的命令项,同时保证状态一致性.ParallelRaft 根据命令的逻辑区块
地址进行冲突判断,无冲突的命令可以乱序执行.我们分析了 ParallelRaft 的乱序执行机制,发现文献[7]中的描
述忽略了可能会违反状态一致性的“幽灵日志”问题.因此,我们提出了 ParallelRaft-CE,它通过限制乱序提交阶
段的并行度,避免了“幽灵日志”问题.
使用形式化规约语言描述分布式协议,并使用模型检验工具验证预期的性质,可以有效地增强人们对协议
可靠性的信心 [18] .Lamport 使用 TLA+ [13,15] 描述了 Paxos [35] ,Fast Paxos [27] ,Byzantine Paxos [31] 等协议 [18] ,并使用模
型检验工具 TLC 验证了这些协议(在受限规模下)的正确性.Ongaro 等人提出了 Paxos 的变体 Raft,并给出了 Raft
的 TLA+规约 [22] .本文给出了 ParallelRaft-SE 和 ParallelRaft-CE 的 TLA+规约,并验证了它们(在受限规模下)的
正确性.
精化技术 [12] 有助于理解各种协议之间的关系.在研究 Paxos 时,Lamport 提出了共识问题的抽象描述
Consensus,给出了分布式共识问题的集中式解决方案 Voting [35] ,并构建了从 Paxos 到 Voting 以及从 Voting 到
Consensus 的精化关系 [35] .Yi 等人在研究腾讯公司 PaxosStore 系统中的 TPaxos 时,提出了 Voting 的一种变体
EagerVoting,并构建了从 TPaxos 到 EagerVoting 以及从 EagerVoting 到 Consensus 的精化关系 [18] .本文构建了从
ParallelRaft-SE 到 Multi-Paxos 的精化关系,证明了 ParallelRaft-SE 的正确性.

8 总结与未来工作

[7]
本文的目标是为 PolarFS 文件系统中使用的 ParallelRaft 协议 (它支持乱序提交、乱序执行用户命令)提
供严格的形式化规约并证明其正确性.首先,为了理清 ParallelRaft 与 Raft 之间的关系,我们提出了允许乱序提
交、顺序执行的 ParallRaft-SE 协议,并建立了从 ParallelRaft-SE 到 Multi-Paxos 的精化关系;其次,我们发现现有
的 ParallelRaft 描述忽略了可能会违反状态一致性的“幽灵日志”问题,并提出了 ParallelRaft-CE 协议.通过限制
ParallelRaft-SE 在乱序提交阶段的并行度,ParallelRaft-CE 避免了“幽灵日志”问题.最后,我们给出了 ParallelRaft-
SE 和 ParallelRaft-CE 的 TLA+规约,并对协议参与者数量较小的情形使用 TLC 模型检验工具,验证了从