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

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

/\negMsgs′=negMsgs\cup {〈〈currentTerm[i],j〉〉}
/\UNCHANGED log
/\UNCHANGED 〈〈serverVars,r1amsgs,r1bmsgs,r2amsgs,r2bmsgs,
r3amsgs,leaderLog,vote〉〉

ClientRequest(i)==
LET ind=={b\in Index:leaderLog[currentTerm[i]][b][1]/=−1}
nextIndex==IF ind={⋅}
THEN 0
ELSE Max(ind)+1
IN
/\currentState[i]=Leader
/\\E v\in Value:leaderLog′=[leaderLog EXCEPT ![currentTerm[i]][nextIndex]=
〈〈currentTerm[i],v,FALSE〉〉]
/\UNCHANGED 〈〈serverVars,log,r1amsgs,r1bmsgs,r2amsgs,r2bmsgs,r3amsgs,
negMsgs,vote〉〉
---------------------------------------------------------------------------------------------------------------------
Next 定义了次态关系.Spec 定义了完整的行为规约.
------------------------------------------------------------------------------------
Next==\/\E i\in Server:Timeout(i)
\/\E i\in Server:RequestVote(i)
\/\E i\in Server:HandleRequestVoteRequest(i)
\/\E i\in Server:BecomeLeader(i)
\/\E i\in Server:CommitEntry(i)
\/\E i\in Server:ClientRequest(i)
\/\E i,j\in Server:RequestCommit(i)
\/\E i\in Server:HandleRequestCommitRequest(i)
\/\E i,j\in Server:RequestSync(i)
\/\E i\in Server:HandleRequestSyncRequest(i)

Spec==Init/\[⋅][Next]_vars
--------------------------------------------------------------------------------------
2.2 精化ParallelRaft-SE到Multi-Paxos

ParallelRaft-SE 支持乱序提交、顺序执行用户命令,这与 Multi-Paxos 相同.此外,ParallelRaft-SE 的日志恢复
阶段本质上是使用 Paxos 对可能缺失的日志项重确认,而 Multi-Paxos 也通过 Paxos 发起提议.实际上,我们可以
建立从 ParallelRaft-SE 到 Multi-Paxos 的精化关系,从而也证明了 ParallelRaft-SE 的正确性.这种精化关系基于
ParallelRaft-SE 与 Multi-Paxos 的以下相似之处.
• RequestVote 对应于 Phase1a.ParallelRaft-SE 中的任期对应于 Multi-Paxos 中的提议编号;
• HandleRequestVote 对应于 Phase1b.二者都需要通过比较任期/提议编号来决定是否同意选举/接受提
议请求,且都需要在回复中包含自己的日志;
• BecomeLeader 对应于 Merge.收到多数派回复的主节点/提议者运行 Paxos 恢复可能缺失的日志项;
• RequestSync 对应于 Phase2a.在 ParallelRaft-SE 中,主节点完成日志恢复后,向从节点同步日志项.在