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

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

些可能已被提交但新任主节点缺失的日志项.
经过恢复,新任主节点满足完全性,此时可以向从节点同步日志项.
ParallelRaft-SE 的规约中使用了如下的常量与变量(仅介绍相对于 Multi-Paxos 模块新引入的部分).
• Server 是所有参与共识的节点的集合;
• Follower,Candidate,Leader 是服务器的 3 种不同状态;
• r1amsgs,r1bmsgs,r2amsgs,r2bmsgs,r3amsgs,negMsgs 是不同类型的消息的集合;
• currentTerm[i]为节点 i 所记录的最大的任期;
• currentState[i]为节点 i 的状态,在任何时候都是 Follower,Candidate,Leader 之一;
• vote[i][n][t]表示节点 i 在任期 t 接受的序号为 n 的日志项.引入 vote 是为了构建 ParallelRaft-SE 到
Multi-Paxos 的精化,实际协议中不需要 vote;
• leaderLog 记录了每个任期的主节点的日志.leaderLog 同样是为了构建 ParallelRaft-SE 到 Multi-Paxos
的精化,实际协议中不需要.leaderLog[t][n]表示任期 t 的主节点的日志中编号为 n 的日志项.每个日志
项是形如〈t′,v,b〉的三元组.其中,t′是日志项的任期;v 是提议值;b 是一个布尔值,当且仅当日志项被提交
时,b 为真;
• log[i][n]为节点 i 的日志中编号为 n 的日志项.
---------------------------------- MODULE ParallelRaft-SE ----------------------------
EXTENDS Integers,FiniteSets,Sequences,TLC
CONSTANTS Server,Follower,Candidate,Leader,Nil,Value

Quorums=={i\in SUBSET(Server):Cardinality(i)*2>Cardinality(Server)}
Index==Nat
Term==Nat

VARIABLE r1amsgs,r1bmsgs,r2amsgs,r2bmsgs,r3amsgs,negMsgs,
currentTerm,currentState,vote,leaderLog,log
serverVars==〈〈currentTerm,currentState〉〉
vars==〈〈r1amsgs,r1bmsgs,r2amsgs,r2bmsgs,r3amsgs,negMsgs,log,
serverVars,leaderLog,vote〉〉
------------------------------------------------------------------------------------------------------
主要的动作包括:
• Timeout(i):从节点或候选节点 i 因未收到来自主节点的消息而超时,则增大自身任期(currentTerm′[i]=
currentTerm[i]+1),将状态转变为选举者(currentState′[i]=Candidate);
• RequestVote(i):候选节点 i 向其他节点发送自身任期,发起选举请求;
• HandleRequestVote(i):节点 i 收到选举请求 m,如果 m 携带的任期大于 i 的任期(m[1]>currentTerm[i]),
则 i 升级任期,接受该选举请求,并将自己的日志发送给候选节点;否则,i 拒绝该选举请求.
------------------------------------------------------------------------------------------------------
Timeout(i)==
/\currentState[i]\in {Follower,Candidate}
/\currentTerm′=[currentTerm EXCEPT ![i]=currentTerm[i]+1]
/\currentState′=[currentState EXCEPT ![i]=Candidate]
/\UNCHANGED 〈〈r1amsgs,r1bmsgs,log,r2amsgs,r2bmsgs,r3amsgs,
negMsgs,leaderLog,vote〉〉