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

谷晓松 等:支持乱序执行的 Raft 协议 1749

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.
Key words: Raft; ParallelRaft; Multi-Paxos; consensus protocols; TLA+; refinement; model checking

分布式共识问题是分布式计算领域的核心问题,它要求多个参与者对某个值或一系列值(也称序列)达成一
[3]
[4]
致 [1,2] .分布式系统通常采用共识协议提供所需的强一致性,如开源 Ceph 、Google 公司的 Spanner 、Oracle
[6]
[5]
[7]
公司的 MySQL 、腾讯的 PaxosStore 以及阿里巴巴(Alibaba)的 PolarDB 等分布式数据存储系统.
Multi-Paxos(Paxos) [8,9] 与 Raft [10] 是解决分布式共识问题的两种经典协议,它们都基于复制状态机(replicated
state machine) [11] 模型,通过投票、日志复制等机制,保证多副本节点上的状态一致性.每个用户命令都将经历“提
交”(commit)与“执行”(execute)两个阶段:如果某命令收到来自多数派(Majority)服务器的投票,则称该命令被“提
交”.只有被提交的命令才能被执行.对于多个命令,这两个阶段都可以以顺序或乱序的方式进行.在乱序方式下,
较大日志编号所对应的命令可能会在较小日志编号所对应的命令之前被提交或者被执行.比如,Raft 要求顺序
提交、顺序执行,Multi-Paxos 则允许乱序提交,但它仍要求顺序执行.
[7]
PolarDB 使用了分布式文件系统 PolarFS .为了提高系统性能,PolarFS 基于 Raft 实现了允许乱序提交、乱
序执行的 ParallelRaft 共识协议.然而文献中并未给出 ParallelRaft 的严格规约,尤其是缺少对乱序执行机制的完
整描述.此外,ParallelRaft 尚未经过必要的数学证明或形式化验证.本文旨在为 ParallelRaft 提供严格的形式化规
约,并基于精化关系 [12] 以及数学论证证明其正确性.具体而言,本文的主要贡献如下:
• 首先,为了理清 ParallelRaft 与 Raft 之间的关系,我们基于 Raft 提出了允许乱序提交,但要求顺序执行的
ParallelRaft-SE(sequential execution)协议.ParallelRaft 可以看作 ParallelRaft-SE 的乱序执行版本.建立
了从 ParallelRaft-SE 到 Multi-Paoxs 之间的精化关系(表明 ParallelRaft-SE 是 Multi-Paxos 的一种实现),
从而证明了 ParallelRaft-SE 的正确性;
• 其次,我们发现文献中描述的 ParallelRaft 乱序执行机制忽略了可能会破坏状态一致性的“幽灵日志”
问题.已有研究表明:在顺序执行方式下(如 Raft 或 Multi-Paxos),“幽灵日志”问题不会破坏副本间的状
态一致性.相反地,我们将论证:在乱序执行方式下,它可能造成副本间状态不一致.更进一步地指出,针
对 Raft 和 Multi-Paxos 的解决方案无法解决乱序执行方式下的状态机的一致性问题;
• 在 ParallelRaft-SE 的基础上提出了支持乱序执行的 ParallelRaft-CE(concurrent execution)协议.通过限
制 ParallelRaft-SE 在乱序提交阶段的并行度,ParallelRaft-CE 避免了“幽灵日志”问题.我们证明了
ParallelRaft-CE 的正确性;
• 最后,使用 TLA+ [13−15] 语言给出了 ParallelRaft-SE 与 ParallelRaft-CE 的形式化规约,并对协议参与者数
量较小的情形,使用 TLC [16] 模型检验工具验证了从 ParallelRaft-SE 到 Multi-Paxos 的精化关系以及
ParallelRaft-CE 的正确性.
本文第 1 节介绍预备知识,包括 TLA+形式化规约语言、分布式共识问题以及 Multi-Paxos 与 Raft 共识协
议.第 2 节介绍 ParallelRaft-SE 协议,并建立从 ParallelRaft-SE 到 Multi-Paxos 的精化关系.第 3 节分析在乱序执
行方式下,“幽灵日志”问题对状态一致性的影响,并指出现有解决方案的不足.第 4 节介绍允许乱序执行且避免
了“幽灵日志”问题的 ParallelRaft-CE 协议.第 5 节简要证明 ParallelRaft-CE 的正确性.第 6 节使用 TLC 模型检
验工具,验证从 ParallelRaft-SE 到 Multi-Paxos 的精化关系以及 ParallleRaft-CE 的正确性.第 7 节讨论相关工作.