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

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

前取得共识的日志项不会丢失.根据规约,当完成重确认后,一个多数派的节点升级同步号为 t 2 ,且由于节点的同
步号递增,之后,同步号小于 t 2 的节点无法通过选举成为主节点候选者,因此已经取得共识的任期为 t 1 的日志项
不会改变.
性质 5(一致性). 对任意两个节点,如果它们的同步号都大于某个任期 t,则它们的日志中包含相同的任期为
t 的日志项.
ParallelRaft-CE 的主节点根据从节点的同步号同步日志项,这与恢复阶段的正确性(性质 3 与性质 4),保证
了节点间日志的一致性.
ParallelRaft-CE 中不会出现“幽灵日志”现象.
在 ParallelRaft-CE 中,新的主节点候选者通过重确认过程对上一主节点的日志项进行重确认.当重确认过
程结束后,主节点候选者的同步号升级为任期.由于节点的同步号递增,选举机制保证了同步号落后的节点无法
成为主节点.因此,系统不会重新提交之前任期的日志项.
6 模型检验与模拟测试

本节使用 TLC 模型检验工具,在模型检验模式与模拟模式下验证 ParallelRaft-CE 协议的正确性,并验证
ParallelRaft-SE 到 Multi-Paxos 的精化关系.
6.1 实验设置
在所有的实验中,我们调整参与者集合 Proposer(Server)、提议者集合 Value、提议编号集合 Ballot(Term)
的大小,并将前两者设置为对称集 [13] ,以提高 TLC 的验证效率.我们使用 10 个线程进行实验,以下是我们的实验
统计结果.
模型检验模式的统计结果包括:已遍历(BFS 方式遍历)的系统状态图的直径、已遍历的状态的数量、已发
现的不同状态的数量以及检验花费的时间(单位是 hh:mm:ss).在验证 ParallelRaft-SE 精化 Multi-Paxos 时,我们
设置 TLC 已检验的不同状态数量超过 1 亿时,人为停止实验.在验证 ParallelRaft-CE 满足一致性时,我们设置
TLC 已检验的不同状态数超过 2 亿时,人为停止实验.
模拟模式下,我们使用随机种子,设置最大深度为 50.统计结果主要为已遍历的状态的数量.每组实验运行 6
小时.
实验使用的机器配置为: 2.40 GHz 10 核 CPU 以及 64GB 内存,TLC 版本号为 1.7.0

6.2 模型检验验证结果
6.2.1 ParallelRaft-SE 精化 Multi-Paxos
图 5 给出了在不同配置下使用模型检验模式验证 ParallelRaft-SE 精化 Multi-Paxos 的验证结果.

Fig.5 Model checking results of verifying the refinement from ParallelRaft-SE to Multi-Paxos
图 5 ParallelRaft-SE 精化 Multi-Paxos 的验证结果
精化关系在 ParallelRaft-SE 的 TLA+规约中给出.从实验数据可以发现:参与者数量与提议值个数对实验的