支持乱序执行的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的正确性.     

GIS和FLAC~(3D)耦合下的采场上覆岩层破坏空间分布

在分析GIS空间数据模型和FLAC3D初始单元模型的基础上,通过GIS栅格数据模型与FLAC3D的六面体单元(Brick)模型的数据耦合,提出了两者耦合下的煤矿采场三维空间构模方法。利用该方法在数值模拟计算结果的基础上建立了GIS时空数据库,以"三带"的断裂带上限值定义了上覆岩层破坏高度函数。结合汝箕沟煤矿32211工作面的开采实际,计算了工作面上覆岩层破坏空间分布,给出了终采线附近上覆岩层破坏高度。