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

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

\/\E i,j\in Server:RequestSync(i)
\/\E i\in Server:HandleRequestSyncRequest(i)
\/\E i\in Server:HandleRequestSyncResponse(i)
\/\E i,j\in Server:UpdateSync(i)
\/\E i\in Server:HandleUpdateSyncRequest(i)
\/\E i\in Server:HandleUpdateSyncResponse(i)

Spec==Init/\[⋅][Next]_vars
--------------------------------------------------------------------------------------------

5 ParallelRaft-CE 的正确性证明

本节简要论证 ParallelRaft-CE 协议的正确性.ParallelRaft-CE 的正确性包括两部分:一是共识协议的一致
性,二是 ParallelRaft-CE 中不会出现“幽灵日志”现象.由此可以得到复制状态机的安全性:节点间执行每个日志
项的顺序没有冲突,状态机的状态一致.
性质 1. 节点的任期与同步号单调递增.
根据规约容易得到,任何节点的任期和同步号是单调递增的;
根据规约,节点只会修改任期等于同步号的日志项,而不会增加、删除或修改日志中任期小于同步号的日
志项.
性质 2(选举的安全性). 每个任期最多选出一个主节点.
ParallelRaft-CE 中,从节点成为主节点需要两个阶段:一是从节点通过选举成为主节点候选者,二是主节点
候选者转变为主节点.其中,选取主节点候选者的方式与 Raft中选取主节点的方式相同.根据 Raft 选主的安全性,
可以得到 ParallelRaft-CE 中每个任期最多选出一个主节点候选者;
主节点候选者可能成功转变为主节点,可能由于失效,或是任期更大的节点发起选举等原因没有转变为主
节点,在这种情况下,系统进入下一任期.因此,每个任期最多选出一个主节点.
任期相同、编号相同的日志项一定包含相同的命令.根据选举的安全性,以及对任意编号,每个主节点最多
添加一个日志项可以得到.这个性质与 Raft 相同.
性质 3. 设主节点候选者的任期为 t,同步号为 s,则 s<t 且系统内不存在任期大于 s 的日志项.
首先,任何节点的同步号不大于任期.由于节点在发起选举需要增大任期(同步号不变),且在选举过程中任
期与同步号不变,因此主节点候选者的同步号小于任期.设主节点候选者 i 的同步号为 s,任期为 t(s<t);
对任意 s<k<t,不存在任期为 k 的主节点.使用反证法,假设存在节点 j 为任期 k 的主节点.根据规约,存在多数
派节点 Q 1 为 i 投票.j 由主节点候选者转变为主节点,因此存在多数派节点 Q 2 升级同步号为 k.根据多数派的性
质,Q 1 ∩Q 2 ≠∅.设 r∈Q 1 ∩Q 2 .若 r 先为 i 投票,那么 r 升级任期为 t.由于 t>k,因此 r 之后会拒绝 j 升级同步号的请求,
这与 r∈Q 2 矛盾.若 r 先升级同步号为 k,那么由于 k>s,之后,r 会拒绝 i 的选举请求(注意,选举投票要比较同步号),
这与 r∈Q 1 矛盾.由此可知,不存在这样的 k;
对 k≥t,不存在任期为 k 的主节点.若系统中存在任期为 k 的主节点,那么 k 在选举中获得多数派节点 Q 的
投票,因此 Q 中节点的任期至少为 k.由于节点的任期递增,因此 i 发起选举时,Q 中的节点的任期要么大于 t,要么
已经为任期为 t 的其他节点投过票,因此不会为 i 投票.这与 i 成为任期为 t 的主节点候选者矛盾.
综上,系统中没有出现过任期大于 s 的主节点,因此不存在任期大于 s 的日志项.
性质 4(主节点的完全性). 若主节点的任期为 t,则其日志中包括所有任期小于 t 且被提交的日志项.
ParallelRaft-CE 中,任期为 t 1 的主节点失效后,新的主节点候选者(任期为 t 2 )会对任期为 t 1 的日志项进行重
确认.在重确认的过程中,所有上一任期的日志项的状态被确定:被提交或者丢弃.重确认过程结束后,主节点候
选者成为新的主节点.重确认的过程实质上是对每个位置执行 Paxos 协议的过程,因此可以保证取得共识,且之