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

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

/\UNCHANGED 〈〈ballot,vote,leaderVote,1bmsgs,2amsgs〉〉

MaxAcceptorVote(a,i)==
LET maxBallot==Max({b\in Ballots:vote[a][i][b]#Nil}\cup {−1})
v==IF maxBallot>−1 THEN vote[a][i][maxBallot] ELSE Nil
IN 〈〈maxBallot,v〉〉

Phase1b(a,b)==
/\ballot[a]<b
/\〈〈b〉〉\in 1amsgs
/\ballot′=[ballot EXCEPT ![a]=b]
/\1bmsgs′=1bmsgs\cup
{〈〈b,{〈〈i,MaxAcceptorVote(a,i)〉〉:i\in Instances},a〉〉}
/\UNCHANGED 〈〈vote,leaderVote,1amsgs,2amsgs〉〉

IncreaseBallot(a,b)==
/\ballot[a]<b
/\ballot′=[ballot EXCEPT ![a]=b]
/\UNCHANGED 〈〈vote,leaderVote,1amsgs,1bmsgs,2amsgs〉〉
-------------------------------------------------------------------------------------------------
• Merge(b):与 Propose(b,i),Phase2a(b,i)动作一起对应于 Paxos 的 Phase2a 阶段.在 Merge 动作中,提议者
根据收到的投票回复更新自己的日志,但是不发起 Accept 请求.当发起提议编号为 b 的 Prepare 请求的
提议者收到一个多数派的回复时,对每一个实例编号 i,根据回复(方法如 Paxos 协议的 Phase2a 阶段描
述)选取提议值,并保存在 leaderVote[b][i]中.值得注意的是:只有当 leaderVote[b][i]之前没有被修改过
时(leaderVote[b][i]=〈−1,Nil〉)时才能更新.因为 Multi-Paxos 中每个提议编号只能有一个提议者发起投
票,且对于每个实例编号,它只能提出一个提议值;
• Propose(b,i):提议者对实例编号 i 提出提议值.若 leaderVote[b][i]=〈−1,Nil〉,那么提议者选取一个合法的
提议值 v,更新 leaderVote[b][i]=〈b,v〉,并发起请求;否则,提议者直接将 leaderVote[b][i]发送给接受者;
• Phase2a(b,i):提议者根据 Merge(b)和 Propose(b,i)中对实例编号 i 确定的提议值,发起 Accept 请求;
• Vote(a,b,i):对应于 Paxos 的 Phase2b 阶段.接受者 a 收到提议编号为 b、实例编号为 i 的 Accept 请求时,
若 b 不小于 a 的提议编号(b>ballot[a]),则 a 接受 Accept 请求,并更新 vote[a][i][b]为对应的提议值.
-------------------------------------------------------------------------------------------
1bMsgs(b,Q)=={m\in 1bmsgs:m[3]\in Q/\m[1]=b}

MaxVote(b,i,Q)==
LET entries==UNION {m[2]:m\in 1bMsgs(b,Q)}
ientries=={e\in entries:e[1]=i}
maxBal==Max({e[2][1]:e\in ientries})
IN CHOOSE v\in Value\cup {Nil}:\E e\in ientries:
/\e[2][1]=maxBal/\e[2][2]=v

lastInstance(b,Q)==LET entries==UNION {m[2]:m\in 1bMsgs(b,Q)}