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

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

主节点(主节点候选者)根据回复修改对 i 的同步号的记录(syncTrack);
• HandleUpdateSyncResponse(i):主节点或主节点候选者 i 收到 UpdateSyncResponse 回复后,更新对发送
者同步号的记录.
--------------------------------------------------------------------------------
HandleUpdateSyncRequest(i)==
\E m\in messages:
LET grant==/\currentTerm[i]=m.mterm
/\m.msync>sync[i]
j==m.msource
IN
/\m.mtype=UpdateSyncRequest
/\i \in m.mdest
/\m.mterm\leq currentTerm[i]
/\\//\grant
/\sync′=[sync EXCEPT ![i]=m.msync]
/\log′=[log EXCEPT ![i]=[n\in Index6
IF log[i][n].term=sync[i] THEN
log[i][n].committed=TRUE
ELSE log[i][n]]]
\//\\neg grant
/\UNCHANGED 〈〈log,sync〉〉
/\Send([mtype6UpdateSyncResponse,mterm6currentTerm[i],
mupdateSyncGranted6grant,msync6sync′[i],
msource6i,mdest6j])
/\UNCHANGED 〈〈currentTerm,currentState,votedFor,end,syncTrack,electionVars〉〉

HandleUpdateSyncResponse(i)==
/\\E m\in messages:
LET j==m.msource IN
/\m.mtype=UpdateSyncResponse
/\m.mdest=i
/\currentTerm[i]=m.mterm
/\currentState[i]\in {Leader,LeaderCandidate}
/\\//\m.mupdateSyncGranted
/\syncTrack′=[syncTrack EXCEPT ![i][j]=m.msync]
\//\\neg m.mupdateSyncGranted
/\UNCHANGED syncTrack
/\UNCHANGED 〈〈messages,serverVars,log,electionVars〉〉
---------------------------------------------------------------------------------------------------
• BecomeLeader(i):主节点候选者 i 执行 UpdateSync 后,若有一个多数派 Q 的节点的同步号升级为
currentTerm[i],且 i 收到它们的确认(∀q∈Q:syncTrack[i][q]=currentTerm[i]),那么 i 转变为主节点,并提交
日志中的所有日志项;