支持乱序执行的Raft协议

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 with Out-of-order Executions