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

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

allLog==UNION {m[2]:m\in voteGranted}
valid=={e\in allLog:e[2][1]/=−1}
end==IF valid={⋅} THEN −1 ELSE Max({e[1]:e\in valid})
IN
/\\A q\in Q:\E m\in voteGranted:m[3]=q
/\leaderLog′=[leaderLog EXCEPT ![currentTerm[i]]=
[n\in Index6IF n\in 0..end THEN
Merge({l[2]:l\in {t\in allLog:t[1]=n}},currentTerm[i])
ELSE 〈〈−1,Nil,FALSE〉〉]]
/\currentState′=[currentState EXCEPT ![i]=Leader]
/\UNCHANGED 〈〈currentTerm,r1amsgs,r2amsgs,r1bmsgs,r2bmsgs,r3amsgs,
negMsgs,log,vote〉〉

RequestSync(i)==
/\currentState[i]=Leader
/\LET sync=={n\in Index:leaderLog[currentTerm[i]][n][1]/=−1}
IN
\E n\in sync:r2amsgs′=r2amsgs\cup
{〈〈currentTerm[i],n,leaderLog[currentTerm[i]][n],i〉〉}
/\UNCHANGED 〈〈serverVars,log,r1amsgs,r1bmsgs,r2bmsgs,
r3amsgs,negMsgs,leaderLog,vote〉〉
------------------------------------------------------------------------------------------------------------------
• HandleRequestSyncRequest(i):i 收到 RequestSync 请求 m,如果 m 携带的任期不小于 i 自身的任期(m[1]>
currentTerm[i]),则 i 接受该请求,升级自己的任期,更新 log[i]与 vote,并回复确认;
• CommitEntry(i):收到多 数派节点对 某个日志项 的确认后 ,主节点 i 将该日志项标记 为已提交
(Committed);
• RequestCommit(i):主节点将已提交的日志项发送给其他节点.
--------------------------------------------------------------------------------------------------
HandleRequestSyncRequest(i)==
/\\E m\in r2amsgs:
LET j==m[4]
grant==m[1]\geq currentTerm[i]
IN
/\\//\m[1]>currentTerm[i]
/\UpdateTerm(i,m[1])
\//\m[1]\leq currentTerm[i]
/\UNCHANGED 〈〈currentTerm,currentState〉〉
/\\//\grant
/\log′=[log EXCEPT ![i][m[2]]=m[3]]
/\vote′=[vote EXCEPT ![i][m[2]][m[1]]=m[3][2]]
/\r2bmsgs′=r2bmsgs\cup {〈〈m[1],m[2],i,j〉〉}
/\UNCHANGED negMsgs