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

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

规模以及检验时间的影响较大,而投票轮数对实验的规模影响相对较小.
6.2.2 ParallelRaft-CE 满足一致性
图 6 给出了在不同配置下使用模型检验模式验证 ParallelRaft-CE 满足一致性的验证结果.

Fig.6 Model checking results of verifying that ParallelRaft-CE satisfies consistency
图 6 ParallelRaft-CE 满足一致性的验证结果

ParallelRaft-CE 的一致性形式化定义为:
AllEntries(i)=={〈〈n,log[i][n]〉〉:n\in Index}
Consistency==\A i,j\in Server:
{e \in AllEntries(i):e[2].term\geq 0/\e[2].term<Min({sync[i],sync[j]})}=
{e\in AllEntries(j):e[2].term\geq 0/\e[2].term<Min({sync[i],sync[j]})}
其中,AllEntries(i)为节点 i 的所有日志项(日志编号与日志的二元组).Consistency 定义了 ParallelRaft-CE 的
一致性,即:任意两个节点,若它们的同步号都大于 t,那么它们的日志中有相同的任期为 t 的日志项.
ParallelRaft-CE 协议更加复杂,不同状态的数量较多,因此我们设置不同状态数达到 2 亿时停止实验.
6.3 模拟模式验证结果
6.3.1 ParallelRaft-SE 精化 Multi-Paxos
图 7 给出了在不同配置下使用模拟模式验证 ParallelRaft-SE 精化 Multi-Paxos 的实验结果.经过估算,在实
验规模较小的情况下(3 个参与者,2 轮投票),状态图的直径为 30 左右;实验规模较大的情况下(4 个参与者,3 轮
投票),状态图的直径为 50 左右.实验设置模拟模式的检测深度为 50.

Fig.7 Simulation results of the refinement from ParallelRaft-SE to Multi-Paxos
图 7 模拟模式验证 ParallelRaft-SE 精化 Multi-Paxos 的实验结果

6.3.2 ParallelRaft-CE 满足一致性
图 8 给出了在不同配置下,使用模拟模式验证 ParallelRaft-CE 满足一致性的实验结果.实验同样设置最大深
度为 50.