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

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

定性质.然而有些分布式系统包含无穷的状态,比如 TLA+规约中常常包含自然数,而自然数是无穷的.为了验证
这样的系统,TLA+引入模型(model).模型所有的集合都是有穷的,因此系统的状态数目是有穷的.模型检验常常
面临组合爆炸的问题,为此,TLC 可以利用模型中的对称性缩减状态空间.例如,假设 CONSTANTS Server 定义了
系统中所有进程的集合.在进行模型检验时,我们需要将它实例化为一个有穷的集合,比如 Server={S 1 ,S 2 ,S 3 }.如
果 S 1 ,S 2 ,S 3 之间的任意排列(比如 S 1 替换 S 2 ,S 2 替换 S 3 ,S 3 替换 S 1 )都不会影响系统规约满足给定的性质,那么我们
可以将 Server 设置为对称集(symmetry set) [13,21] .
在 TLA+中,精化(refinement)关系 [12] 用来描述模块之间的逻辑蕴含(logical implication)关系 [18] .精化关系由
精化映射(refinement mapping)定义.比如,一个由模块 ImplModule 中的 ImplSpec 规约到模块 AbsModule 中的
AbsSpec 规约的精化映射φ将 AbsSpec 中的每个变量 v 对应于一个表达式 ,vv 由 ImplSpec 中的变量定义.对于
ImplSpec 的每一个状态 s,精化映射φ定义了 AbsSpec 的状态 ,s s 中的每个变量 v 的值由 s 中的 v 定义.若σ为
ImplSpec 的行为 s 1 →s 2 →…,我们定义 AbsSpec 的行为 σ : s → s → ... .ImplSpec 在精化映射φ下实现/精化了
1 2
AbsSpec(ImplSpec⇒AbsSpec)当且仅当对于任何一个满足 ImplSpec 的行为σ,行为σ 满足规约 AbsSpec [14] .为了使
用 TLC 检验在精化映射φ下,ImplSpec 到的精化关系,我们在模块 ImplModule 中添加了定义 AbsSub INSTANCE
AbsModule,并检验定理 THEOREM ImplSpec⇒AbsSub!AbsSpec [18] .
1.2 分布式共识

分布式共识要求多个副本服务器节点保持状态一致.每个服务器节点可以建模为一个复制状态机,通过执
行用户命令进行状态转换.
通常使用复制日志的机制实现复制状态机.每个服务器保存一份日志.日志由按顺序编号(通常是自然数)
的日志项组成.每个日志项存储了一条来自用户的命令.服务器每次按顺序从日志中读取下一条已经取得共识
的命令,在状态机上执行,并将结果返回给用户.由于服务器按照编号顺序执行一条命令,我们称此为顺序执行.
传统的分布式共识协议(Multi-Paxos,Raft)都是顺序执行.在此条件下,我们假设副本服务器上的复制状态机具
有相同的初始状态,那么只需要保证日志之间的一致性,就可以保证服务器之间的状态一致.因此,分布式共识
问题可以转化为保证不同副本服务器节点上日志之间的一致性.具体而言,它要求:
• 非平凡性(nontriviality):只能对用户发出的命令取得共识;
• 一致性(consistency):每个位置最多只能对一条命令取得共识.
服务器通过运行共识协议保证日志的一致性.本文考虑异步消息传递系统中的共识协议,其故障模型
(failure model)如下.
[8]
• 服务器可能终止执行(fail by stop),但不会出现拜占庭错误 ;
• 消息可能被延时、乱序到达、丢失或重复,但消息的内容不会被篡改.
1.3 Paxos协议
Paxos 协议是解决分布式共识问题的经典协议,它允许一组服务器对单个值(即单个日志项)取得共识,是
Multi-Paxos 的基础.Paxos 中定义了 3 种角色:提议者(proposer)、从节点(acceptor)和学习者(learner).提议者提出
[8]
值(value),接受者选择值,学习者学习被选中的值.Paxos 包括两个阶段,每个阶段又包括两个子阶段 .
• 准备(prepare)阶段(也称第 1 阶段,Phase1)
¾ 子阶段 Phase1a:提议者选择一个全局唯一的编号 b(通常是自然数),向所有接受者发送编号为 b
的 Prepare 请求;
¾ 子阶段 Phase1b:接受者收到编号为 b 的 Prepare 请求.如果它之前收到过编号大于 b 的 Prepare
请求,则忽略该编号为 b 的请求;否则,接受者将自己接受过的提议(包括编号与值)中编号最大的
回复给提议者;
• 接受(accept)阶段(也称第 2 阶段,Phase2)
¾ 子阶段 Phase2a:提议者收到来自超过半数的接受者发送的针对编号为 b 的 Prepare 请求的回复.