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

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

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

HandleRequestVoteRequest(i)==
/\\E m\in r1amsgs:
LET j==m[2]
grant==m[1]>currentTerm[i]
entries=={〈〈n,log[i][n]〉〉:n\in Index}
IN
\//\grant
/\UpdateTerm(i,m[1])
/\r1bmsgs′=r1bmsgs\cup {〈〈m[1],entries,i,j〉〉}
/\UNCHANGED negMsgs
\//\\neg grant
/\negMsgs′=negMsgs\cup {〈〈currentTerm[i],j〉〉}
/\UNCHANGED 〈〈currentState,currentTerm,r1bmsgs〉〉
/\UNCHANGED 〈〈log,r1amsgs,r2amsgs,r2bmsgs,r3amsgs,vote,leaderLog〉〉
--------------------------------------------------------------------------------------------------------------
• BecomeLeader(i):收到多数派投票的候选节点 i 成为主节点,并根据收到的日志恢复可能缺失的日志
项.对每个日志编号 n,考察它收到的所有编号为 n 的日志项,选择其中任期最大的日志项,将该日志项
的任期修改为 i 自身的任期.为了构建从 ParallelRaft-SE 到 Multi-Paxos 的精化关系,恢复过程将修改
leaderLog,而非直接修改 log[i].之后,i 可以向自己发送 RequestSync 请求,完成日志更新;
• RequestSync(i):主节点 i 向其他节点同步日志项.
--------------------------------------------------------------------------------------------------------------
Merge(entries,term)==
LET committed=={e\in entries:e[3]=TRUE}
chosen==
CASE committed={⋅}→CHOOSE x\in entries:
\A y\in entries:x[1]\geq y[1]
[⋅] committed/={⋅}→CHOOSE x\in committed:TRUE
safe==chosen[2]
IN 〈〈term,safe,chosen[3]〉〉

BecomeLeader(i)==
/\currentState[i]=Candidate
/\\E Q\in Quorums:
LET voteGranted=={m\in r1bmsgs:m[4]=i/\m[3]\in Q
/\m[1]=currentTerm[i]}