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

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

法与 ParallelRaft-SE(或 Multi-Paxos)相同,l 需要从多数派节点收集日志项,并从中选择最“新”的日志项.由于日
志项的任期是固定的,ParallelRaft-CE 为每个日志项增加一个新的变量:日期(date).日期相当于 Paxos 中日志项
的提议编号.日志编号相同,日期越大的日志项就越“新”.
l 需要分 3 个阶段将恢复得到的日志项同步给从节点.设 l 记录某从节点的同步号为 n.如果 n>s,则直接进
入第 3 阶段;如果 n=s,则直接进入第 2 阶段;否则,先进入第 1 阶段.
第 1 阶段(n<s):l 先向该从节点发送任期为 n 的日志项.当这些项被从节点全部确认后,l 通知从节点升级到
满足以下条件的下一个同步号 k:
(1) k>n;
(2) l 的日志中含有任期为 k 的日志项;
(3) k 是满足条件 1、条件 2 的最小值.
收到升级同步号请求后,从节点删除日志中所有未确认的任期为 n 的日志项,并将同步号升级为 k.之后,主
节点候选者向从节点发送任期为 k 的日志项.持续以上过程,直到从节点的同步号升级为 s.进入第 2 阶段.
第 2 阶段(n=s):l 持续向从节点同步日志项,直到任期为 s 的所有日志项都被相同的多数派提交,记这个多数
派为 Q.进入第 3 阶段.
第 3 阶段(n>s):l 将它的同步号升级为自身的任期 t(根据性质 3,这是安全的).然后,l 通知 Q 中的节点将自身
同步号升级为 t.收到某多数派节点(均来自 Q)的确认消息后,恢复过程结束,l 正式成为主节点.
4.4 ParallelRaft-CE的TLA+规约
ParallelRaft-CE 使用常量 LeaderCandidate 表示主节点候选者角色.其中的变量包括:
• messages:节点发送的消息的集合;
• currentTerm[i]:节点 i 记录的最大的任期;
• currentState[i]:节点 i 的状态,为 Leader,LeaderCandidate,Follower,Candidate 之一;
• votedFor:每个节点一个任期内只能为一个候选节点投票.votedFor[i]表示 i 在本任期(currentTerm[i])内
投票的候选节点.若 i 没有为任何节点投票,则 votedFor[i]=Nil;
• sync[i]:节点 i 的同步号;
• end[i][t]:节点 i 记录的可接受的任期为 t 的日志项的最大编号.ParallelRaft-CE 使用 Paxos 的投票机制
确定每一个任期的最大编号;
• log[i]:节点 i 的日志.log[i][k]为 i 的日志中编号为 k 的日志项.每个日志项是〈t,d,v,b〉的四元组.其中:t 是
日志项的任期,不可修改;d 是日期,用于判断日志项的新旧;v 是提议值;b 是布尔值,当且仅当日志项被
提交时,b 为真;
• syncTrack:状态为 Leader 或 LeaderCandidate 的节点用来记录其他节点的同步号.syncTrack[i][a]为节点
i 记录的节点 a 的同步号;
• elections,halfElections 为历史变量,记录了选举信息.
-------------------------- MODULE ParallelRaft-CE --------------------------
CONSTANTS Server,Follower,Candidate,Leader,LeaderCandidate,Nil,Value,
RequestVoteRequest,RequestVoteResponse,
RequestCommitRequest,RequestCommitResponse,
RequestSyncRequest,RequestSyncResponse,
UpdateSyncRequest,UpdateSyncResponse

Quorums=={i\in SUBSET (Server):Cardinality(i)*2>Cardinality(Server)}

VARIABLE messages,currentTerm,currentState,votedFor,sync,end,log,syncTrack