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

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

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

CommitEntry(i)==
/\\E index\in Index,Q\in Quorums:
LET syncSuccess=={m\in r2bmsgs:
m[4]=i/\m[3]\in Q
/\m[1]=currentTerm[i]/\m[2]=index}
IN
/\currentState[i]=Leader
/\\A q\in Q:\E m \in syncSuccess:m[3]=q
/\leaderLog′=[leaderLog EXCEPT ![currentTerm[i]][index][3]=TRUE]
/\UNCHANGED 〈〈serverVars,log,r1amsgs,r1bmsgs,r2amsgs,r2bmsgs,
r3amsgs,negMsgs,vote〉〉

RequestCommit(i)==
/\currentState[i]=Leader
/\LET committed=={n\in Index:leaderLog[currentTerm[i]][n][3]=TRUE} IN
\E n\in committed:r3amsgs′=r3amsgs\cup {〈〈currentTerm[i],n,i〉〉}
/\UNCHANGED 〈〈serverVars,log,r1amsgs,r1bmsgs,r2amsgs,r2bmsgs,
negMsgs,leaderLog,vote〉〉
---------------------------------------------------------------------------------------------------------------
• HandleRequestCommit(i):节点 i 收到来自主节点的 RequestCommit 请求 m,如果 m 携带的任期不小于 i
自身的任期,则 i 将相应的日志项标记为已提交;
• ClientRequest(i):收到用户的命令 v 后,主节点 i 将 v 作为新的日志项添加到日志中.
--------------------------------------------------------------------------------------------------------
HandleRequestCommitRequest(i)==
/\\E m\in r3amsgs:
LET grant==currentTerm[i]\leq m[1]
j==m[3]
IN
/\\//\m[1]>currentTerm[i]
/\UpdateTerm(i,m[1])
\//\m[1]\leq currentTerm[i]
/\UNCHANGED 〈〈currentTerm,currentState〉〉
/\\//\grant
/\log[i][m[2]][1]=m[1]
/\log′=[log EXCEPT ![i][m[2]][3]=TRUE]
/\UNCHANGED negMsgs
\//\\neg grant