分布式共识(consensus)问题是分布式计算领域中的核心问题, 它要求多个参与者就某个值达成一致^{[1, 2]}. Paxos(也称Basic Paxos或single-decree Paxos)是解决分布式共识问题的经典协议^{[3, 4]}.通过并行执行多个独立的Paxos实例, Multi-Paxos允许参与者就一系列值(也称序列)达成一致^{[3, 4]}.Paxos/Multi-Paxos及其变体被广泛用于需要提供强一致性的分布式系统中, 如Google的Chubby分布式锁服务系统^{[1, 5]}与Spanner分布式数据库系统^[6]、微软的Autopilot自动数据中心管理系统^[7]以及腾讯的PaxosStore分布式存储系统^[8].本文关注PaxosStore系统所实现的Paxos变体.我们称其为TPaxos.

在TPaxos中, 每个参与者(即数据副本节点)都同时具有提议者(proposer)、接受者(acceptor)与学习者(learner)这3种角色.TPaxos的新颖之处在于它的“统一性”:它为每个参与者维护统一的状态类型, 并采用统一格式的消息进行通信.在TPaxos中, 参与者通过互相交换统一类型的消息, 不断更新状态, 最终达成共识.相比而言, 经典的Paxos协议(及其众多变体)为不同的角色维护不同的状态类型, 并且需要使用4种消息类型, 以区分准备阶段(prepare phase, 包含Phase1a与Phase1b两个子阶段)与接受阶段(accept phase, 包含Phase2a与Phase2b两个子阶段)中的两轮双向通信.这种设计方案可以带来精简而高效的系统实现^[8].然而, 这也带来了TPaxos与Paxos之间的诸多差异, 给理解TPaxos造成了障碍.其次, 虽然腾讯开源了TPaxos协议的核心代码(包括论文中的伪代码与实际系统中的C++代码^[9]), TPaxos仍缺少抽象而精确的形式化规约.最后, 据我们所知, TPaxos的正确性尚未经过必要的数学论证或者形式化工具的检验.

针对上述情况, 本文有3个主要贡献.

●   第一, 我们论证如何从Paxos出发, 逐步推导出Tpaxos:首先, 我们通过合并3种角色, 统一参与者的状态类型; 其次, 基于统一的状态类型, 我们可以统一消息内容; 然后, 通过合并某些子阶段, 并避免使用消息状态信息区分协议阶段, 我们可以得到一种比TPaxos更为精简的统一消息类型; 最后, 我们指出TPaxos在消息处理阶段所作的优化, 从而推导出最终的TPaxos版本.

●   第二, 我们给出了TPaxos的TLA+^[10-12]形式化规约.与已有的Paxos的TLA+规约^[13]类似, TPaxos采用“已发送消息集合”作为通信信道以及消息发送与接收动作的抽象.这种抽象使得该规约不依赖于代码层面的具体通信机制.更重要的是, 在开发TLA+规约的时候, 我们发现TPaxos协议描述中存在至关重要但并未充分阐明的微妙之处:在消息处理阶段, 参与者(作为接受者角色)是先作出“不再接受具有更小编号的提议”的承诺(promise)还是先接受(accept)提议?这导致对TPaxos的两种不同理解, 并促使我们提出TPaxos的一种变体, 称为TPaxosAP.在TPaxosAP中, 参与者先接受提议后作承诺.虽然在TLA+规约层面, TPaxosAP与TPaxos(先作承诺后接受提议)相差甚小, 但它却体现了不同的投票机制.具体来讲, Paxos协议的投票机制Voting^[13]仍适用于TPaxos, 却不能完整刻画TPaxosAP的行为.在本节, 我们将举例说明TPaxosAP与TPaxos的不同之处, 并论证TPaxosAP的正确性.

●   第三, 我们采用精化(refinement)^{[14, 15]}技术论证了TPaxos与TPaxosAP的正确性.对于TPaxos, 我们仍采用Paxos所使用的Voting^[13]机制, 建立了从TPaxos到Voting的精化关系.对于TPaxosAP, 我们首先提出了一种新的投票机制, 称作EagerVoting.EagerVoting允许参与者在接受提议的同时, 作出比Paxos/ TPaxos更“激进”的“不再接受具有更小编号的提议”的承诺.然后, 我们建立了从TPaxosAP到EagerVoting以及从EagerVoting到Consensus的精化关系, 并使用TLC模型检验工具^[16]验证它们的正确性.

本文第1节介绍预备知识.第2节介绍TPaxos协议, 并论证如何逐步从Paxos推导出TPaxos.第3节先给出TPaxos的TLA+规约, 然后提出它的一种变体TPaxosAP并论证其正确性.第4节构建从TPaxos与TPaxosAP到Consensus的精化关系.第5节使用TLC模型检验工具验证精化关系并展示实验结果.第6节讨论相关工作.第7节总结全文, 并讨论可能的未来工作.

1 预备知识

我们先介绍TLA+形式化规约语言然后介绍分布式共识问题与经典Paxos协议(包括协议描述、TLA+规约与精化).

1.1 TLA+简介

TLA+是LeslieLamport基于时序逻辑TLA(temporal logic of actions)^[12]开发的一种形式化规约语言, 适用于描述并发及分布式系统.TLA+将系统建模成状态机, 一个状态机由它可能的初始状态(initial states)与一组动作(actions)来刻画.在TLA+中, 一个状态是系统中所有变量的实例化.一个行为是状态的序列.一个动作是新旧状态之间的转移, 刻画了系统执行指令前后的变化.例如, 对于指令x:=x+1, TLA+采用动作x’=x+1进行描述.TLA+使用一个包含带撇变量(表示新状态的值)与不带撇变量(表示旧状态的值)的公式来描述动作.

一般而言, 一个系统可以表达为TLA中的一个形如Spec≜Init∧[Next]_vars∧L的时序公式.其中, Init和Next都是状态谓词(结果为布尔值), 对系统状态进行刻画.Init刻画了系统的初始状态, Next是所有动作的析取式, 描述了系统的所有动作.vars是包含系统所有变量的元组, W是“总是(always)”的时序操作符.表达式[Next]_vars为真当且仅当Next为真(即某个动作为真, 意味着该动作对应的指令被系统执行), 或者vars在新旧状态中保持不变.后者是TLA+的一个特性, 有利于构建系统间的精化关系.L用于检测系统的活性(liveness).

在TLA+中, L通常是WF的析取式, WF指弱公平性(weak fairness), WF_vars(A)刻画了动作A的公平性, 即要求:如果动作A从某个时刻开始是持续可执行的, 则A最终将被执行.WF_vars(A)的定义如下:

$ W{{F}_{\mathit{vars}}}\left( A \right)\triangleq \square \left( \square ENABLED{{\left\langle A \right\rangle }_{\mathit{vars}}}\Rightarrow \diamond {{\left\langle A \right\rangle }_{\mathit{vars}}} \right). $

其中, 〈A〉_vars表示动作A被执行, ENABLED〈A〉_vars表示动作A(在当前状态下)是可执行的, ◇是“最终(eventually)”的时序操作符.

TLA+在TLA的基础上加入了一阶谓词逻辑以及ZF集合论, 从而支持丰富的数据类型与表达式.图 1总结了本文使用到的逻辑与集合操作符(operator).文献[17]给出了完整的TLA+操作符列表.

TLA+规约以模块(module)的形式组织在一起.在每个模块中, 我们可以声明常量(constants)与变量(variables)或者提出定理(theorem).一个模块M可以通过扩展其他模块M₁, …, M_n的方式引入声明、定义与定理; 在模块M中, 写作EXTENDS M₁, …, M_n.模块也可以被实例化.考虑M模块中的实例化语句:

$ I{{M}_{1}}\triangleq \text{INSTANCE}\ {{M}_{1}}\ \text{WITH}\ {{p}_{\text{1}}}\leftarrow {{e}_{1}}\ldots {{p}_{n}}\leftarrow {{e}_{n}}, $

其中, p_i包含了M₁中的所有常量与变量, e_i是M中的合法表达式.该语句是通过将M₁中的p_i替换为M中相应的e_i来进行M₁的实例化, 我们可以使用IM₁!F来访问模块M₁中的表达式F.此外, TLA+中的隐式替换规则允许我们在e_j与p_j相同时省略p_j←e_j子句.

TLC是TLA+的模型检验工具, 它通过遍历TLA+规约的有穷状态空间来验证规约是否满足具体的性质.然而有些分布式系统的状态并非有穷, 例如, 考虑一个包含多个服务器的分布式系统, 服务器(定义为Server)的数量可以任意大, 甚至无穷.为了能够验证这一类系统规约, TLC通过模型(model)的方式限制了这些系统的状态数, 即TLC可以在模型中实例化服务器为有穷集合, 如Server≜{s₁, s₂, s₃}.如果对于值{s₁, s₂, s₃}进行任意重排(如将s₁替换为s₂, s₂替换为s₃, s₃替换为s₁)不影响TLC的验证结果, 我们可以将Server标记为对称集(symmetry set)^[18]以减少TLC需要遍历的状态空间.

在TLA+中, 精化(refinement)关系就是逻辑蕴含(logical implication)关系.例如, 考虑模块AbsModule中的AbsSpec规约以及模块ImplModule中的ImplSpec规约.AbsSpec包含变量x₁, …, x_m, y₁, …, y_n, ImplSpec包括变量x₁, …, x_m, z₁, …, z_p.令X, Y与Z分别代表变量组x₁, …, x_m, y₁, …, y_n与z₁, …, z_p.为了验证ImplSpec实现/精化了AbsSpec (也称ImplSpec是AbsSpec的精化, 即ImplSpec⇒AbsSpec), 我们需要证明:对于每一个满足ImplSpec的行为, 都存在一种关于变量组Y的赋值方式, 使得赋值后所得的行为(考虑变量组X与Y)满足AbsSpec^{[14, 15]}.具体而言, 对于每个一y_i, 我们仅使用X与Z定义表达式${{\bar{y}}_{i}}$, 在AbsSpec中做替换${{y}_{i}}\leftarrow {{\bar{y}}_{i}}$, 得到新的规约$\overline{AbsSpec}$, 然后证明ImplSpec实现/蕴含了$\overline{AbsSpec}$.这里, 替换${{y}_{i}}\leftarrow {{\bar{y}}_{i}}$被称为精化映射(refinement mapping).为了使用TLC检验在精化映射${{y}_{i}}\leftarrow {{\bar{y}}_{i}}$下, ImplSpec实现了AbsSpec, 我们在模块ImplModule中添加定义AbsSpec≜INSTANCE AbsModule WITH$~{{y}_{1}}\leftarrow {{\bar{y}}_{1}}, ..., {{y}_{n}}\leftarrow {{\bar{y}}_{n}}$, 并检验定理THEOREM ImplSpec⇒AbsSub!AbsSpec.

1.2 分布式共识

我们使用“3种角色模型”定义分布式共识问题^{[3, 19]}.提议者(proposer)可以提出值(value), 接受者(acceptor)负责选择值, 学习者(learner)需要获悉被选中(chosen)的值.分布式共识问题的安全性(safety)需求包括:

●   非平凡性(nontriviality).只有被提出过的值才能被选中.

●   一致性(consistency).最多只有一个值被选中.

TLA+模块Consensus^[13]抽象地描述了分布式共识问题.常量Value表示所有可能被提出的值构成的集合, 它建模了提议者角色.变量chosen表示已被选中的值构成的集合, 它建模了接受者角色.在初始状态下, chosen为空.该规约只有一个可能的动作:如果chosen为空, 则从Value中任选一个值v加入chosen中(即选中v).不变式Inv表达了分布式共识问题的安全性.其中, 第3条合取式是一致性的定义, 描述了chosen中的元素个数不超过1, 即最多只有一个值被选中.显然, 规约Spec满足Inv, 即有THEOREM Spec⇒Inv成立.

除了安全性以外, 分布式共识问题还包括活性, Liveness表达了活性的具体定义, 即最终会有某个值被选中.

1.3 Paxos协议

Paxos是在异步消息传递系统中解决分布式共识问题的重要协议, 它采用传统的非拜占庭(non-Byzantine)故障模型^[3].在该模型中,

●   每个参与者(包括提议者、接受者与学习者)以各自的速度异步执行, 参与者可能终止执行(fail by stopping), 也可能重启(restart).

●   消息可能会延时到达、重复或丢失, 但是消息不会被篡改.

在Paxos中, 提议者为每个提议值v附加一个(全局唯一的)提议编号b.我们用〈b, v〉表示提议, 接受者按规则接受提议.如果某个提议被“足够多”的接受者接受了, 则称该提议以及它包含的值被选中.这里的“足够多”通常是指接受者中的任意一个多数派(majority).因此, Paxos可以容忍不超过半数的接受者失效.“多数派”是一种特殊的议会系统(quorum system).设集合Q⊆2^A是由接受者集合A的子集构成的集合.如果Q满足以下两个条件, 则称Q为一个议会系统.

●   Q构成A的集合覆盖(set cover):$\bigcup\nolimits_{Q\in \mathcal{Q}}{Q}=A$.

●   任意两个议会(quorum)相交不为空:∀Q₁, Q₂∈Q:Q₁∩Q₂≠Ø.

Paxos包含两个阶段, 每个阶段由两个子阶段构成^[3]:

●   准备(prepare)阶段(也称第1阶段Phase1).

   ➢   子阶段Phase1a:提议者选取一个提议编号b, 然后向所有接受者(在原始Paxos协议描述中, 只要求向接受者中的某个议会发送请求.为了叙述方便, 本文改为向所有接受者发送请求.显然, 该改动不影响协议的正确性)发送编号为b的Prepare请求.

   ➢   子阶段Phase1b:如果一个接受者收到编号为b的Prepare请求, 并且编号b大于它之前回复过的所有Prepare请求的编号, 那么它就将自己接受过的编号最大的提议(包括编号与值)回复给相应的提议者, 并承诺不会再接受任何编号小于b的提议;

●   接受(accept)阶段(也称第2阶段Phase2):

   ➢   子阶段Phase2a:如果提议者收到来自接受者中的某个议会对编号为b的Prepare请求的回复, 那么它就向所有接受者发送一个针对提议〈b, v〉的Accept请求.其中, v由收到的回复决定:如果回复中不包含任何提议, 则v可以是任意值; 否则, v是这些回复中编号最大的提议对应的值.

   ➢   子阶段Phase2b:如果一个接受者收到针对提议〈b, v〉的Accept请求, 只要它尚未对编号大于b的Prepare请求作过回复, 它就可以接受该提议.

1.4 Paxos协议的TLA+规约 1.4.1 常量

Paxos的TLA+规约^[13]包含3个常量.

●   Value:所有可能的提议值构成的集合(如, {v₁, v₂, v₃}).我们定义None≜CHOOSE v:v∉Value表示不属于Value的某个值.

●   Acceptor:所有接受者构成的集合(如, {a₁, a₂, a₃}).

●   Quorum:由接受者形成的议会系统.QuorumAssumption给出了议会系统需要满足的条件.

我们用自然数表示可能的提议编号, 即Ballot≜Nat, 并用-1表示相关变量初始化时用到的最小提议编号.

1.4.2 变量

Paxos的TLA+规约包含4个变量.

●   maxBal:maxBal[a]表示接受者a在Phase1b与Phase2b两个子阶段见到过的最大提议编号, 也是a承诺可以接受的提议的最小编号.

●   maxVBal与maxVVal:maxVBal[a]表示接受者a接受过提议的最大编号, maxVVal[a](Paxos的原始TLA+规约中使用了变量名maxVal.为了与maxVBal对应, 本文改用maxVVal)是对应提议中的提议值.我们使用符号〈maxVBal[a], maxVVal[a]〉表示该提议.

●   msgs:所有已发送消息构成的集合.参与者通过向该集合添加消息, 或者从该集合读取消息模拟消息的发送(广播)与接收动作.Send(m)将消息m加入到msgs中.为了对应Paxos协议的4个子阶段, 该规约定义了4种消息类型, 分别为“1a”, “1b”, “2a”与“2b”.

●   TypeOK定义了各个变量的类型.Init给出了初始状态下各个变量的取值.

1.4.3 动作

Paxos规约定义了4种动作, 分别对应于协议的4个子阶段.

●   Phase1a(b):提议者选取提议编号b, 发起Prepare请求.消息类型为m.typea“1a”, 并携带提议编号m.balab.

●   Phase1b(a):接受者a收到类型为“1a”的消息m.如果m中携带的提议编号m.bal大于maxBal[a], 则接受者a将maxBal[a]更新为m.bal, 并将它接受过的最大编号提议(即〈maxVBal[a], maxVVal[a]〉)回复给提议者.消息类型为“1b”, 并携带收到的提议编号m.bal.

●   Phase2a(b, v):提议者发起针对提议〈b, v〉的Accept请求.该动作有两个前置条件:(1)第1个合取子句要求, 针对提议编号b, 提议者尚未发起过Accept请求, 即msgs中不存在类型为“2a”且编号为b的消息; (2)第2个合取子句要求, 存在接受者中的某个议会Q, Q中的每个接受者都回复过针对提议编号b的Prepare请求.前置条件成立时, 提议者便根据Q中每个接受者回复的消息确定b值(方法如Paxos协议的Phase2a子阶段所述), 然后通过类型为“2a”的消息发起针对提议〈b, v〉的Accept请求.

●   Phase2b(a):接受者a接受某个提议.该动作的前置条件是存在类型为“2a”的消息m, 并且m中携带的提议编号m.bal大于等于maxBal[a].前置条件成立时, 接受者a将maxBal[a]更新为m.bal(需要注意的是, 自然语言描述的Paxos协议^[3]没有要求更新maxBal[a].然而, 可以通过反例说明, 如果不同时更新maxBal[a], 则Paxos并不能保证论文中的不变式P2^c成立), 并且接受消息m中携带的提议〈m.bal, m.val〉, 然后将该提议封装在类型为“2b”的消息中发送出去.

1.4.4 行为

Next定义了次态关系.Spec定义了完整的行为规约.

1.5 Paxos的精化

Paxos协议的核心在于接受者何时可以接受提议, 以及这些提议需要满足何种条件.一方面, 接受者a只有在提议编号b大于等于它回复过的最大提议编号maxBal[a](也是它承诺可以接受的提议的最小编号)时, 才可能接受该提议.另一方面, 可被接受的提议〈b, v〉需要满足两个关键条件:一是每个提议编号(这里的b)最多对应一个提议(这里的〈b, v〉), 该条件称为OneValuePerBallot; 二是〈b, v〉是安全的, 即对于任何提议〈b’, v’〉, 其中, b’∈0…b-1, v’≠v, 〈b’, v’〉都尚未被选中且将来也不会被选中.该条件称为SafeAt(b, v).Lamport使用TLAPS(TLA+ proof system)证明了^[20]Paxos协议正确性的关键在于上述两个条件, 即只要满足这两个条件, 就能保证Paxos的正确性.

为了更好地理解上述核心问题, Lamport提出了一个更抽象的规约, 记为Voting^[21].在Voting中, 每个接受者a仍然维护maxBal[a].此外, 它还维护它曾接受过的所有提议votes.该规约包含两个动作:在IncreaseMaxBal(a, b)中, 接受者a可以提高自己的maxBal[a], 该动作对应于Phase1a与Phase1b子阶段; 在VoteFor(a, b, v)中, 接受者a接受提议〈b, v〉.其中, 第2个与第3个合取式保证了OneValuePerBallot条件; 第4个合取式保证了SafeAt(b, v)条件, 该动作对应于Phase2a与Phase2b子阶段.

由于VoteFor(a, b, v)使用了所有被接受过的提议这一全局信息, Voting可以看作分布式共识问题的集中式解决方案, 而Paxos是Voting的分布式实现.实际上, Lamport构建了从Paxos到Voting以及从Voting到Consensus的精化关系^[13].

2 TPaxos协议及其推导

本节首先介绍TPaxos协议, 然后论证如何从经典Paxos协议推导出TPaxos协议.

2.1 TPaxos协议

在TPaxos协议中, 所有的参与者(即数据副本节点, 假设有N个)都同时具有提议者、接受者与学习者这3种角色.TPaxos协议的新颖之处在于它的“统一性”:它为每个参与者维护统一的状态类型, 并采用统一格式的消息进行通信.相比而言, Paxos及其众多变体为提议者与接受者维护不同的状态类型(即维护不同的变量), 并且需要4种消息类型来区分协议的4个子阶段.下面我们先分别介绍统一的状态类型与消息类型, 然后介绍具体协议过程.

在TPaxos中, 每个提议P是一个二元组〈b, v〉, 其中, b表示提议编号, v表示提议值.每个参与者p维护一个大小为N的状态向量S^p.其中, 参与者q对应的向量值, 记为$S_{q}^{p}$, 表示p对q的观察状态(view state).特殊地, 如果p=q, 则称$S_{p}^{p}$为p的当前实际状态(actual state).每个状态$S_{q}^{p}$记为(m, P):m表示q承诺可以接受提议的最小编号; P表示q最近一次接受的提议〈b, v〉.我们使用$S_{q}^{p}.m, S_{q}^{p}.P, S_{q}^{p}.P.b$与$S_{q}^{p}.P.v$访问相应的状态分量.

在TPaxos中, 参与者p发送给q的统一消息类型可记为${{M}_{p\to q}}=(S_{p}^{p}, S_{q}^{p})$.也就是说, p会将自身的实际状态$S_{p}^{p}$以及它对q的观察状态$S_{q}^{p}$一起发送给q.

参与者之间通过相互交换此类消息不断更新状态, 并在本地判断是否有值已被选中, 从而最终达成共识.具体而言, TPaxos的执行过程与Paxos类似, 也分为两个阶段(伪代码如图 2所示).

(1) 准备阶段

●   Phase1a子阶段:参与者p选取一个大于$S_{p}^{p}.m$的提议编号b, 更新$S_{p}^{p}.m$至b, 然后向其他所有参与者q≠p发送消息${{M}_{p\to q}}=(S_{p}^{p}, S_{q}^{p})$(即Prepare请求).

●   消息处理(OnMessage)子阶段:参与者q收到并处理来自p的消息${{M}_{p\to q}}=(S_{p}^{p}, S_{q}^{p}).$

   ➢   首先, q根据$S_{p}^{p}$更新本地状态$S_{p}^{q}$与$S_{q}^{q}$.此处重点关注$S_{q}^{q}$的更新:

      1)   作承诺:如果$S_{q}^{q}.m<S_{p}^{p}.m$, 则将$S_{q}^{q}.m$更新为$S_{p}^{p}.m$.这模拟了Paxos中的Phase1b阶段.

      2)   接受提议:如果$S_{q}^{q}.m<S_{p}^{p}.P.b$, 则将$S_{q}^{q}.P$更新为$S_{p}^{p}.P$.这模拟了Paxos中的Phase2b阶段.

      消息处理阶段(的核心)是Phase1b与Phase2b子阶段的合并.需要注意看到, 根据TPaxos的伪代码, q先作承诺后接受提议(此时, 第2)步$S_{q}^{q}.m<S_{p}^{p}.P.b$中的$S_{q}^{q}.m$可能已被更新).第3节将讨论另一种方案, 即q先接受提议后作承诺.

   ➢   然后, q根据本地状态向量S^q判断是否有值已被选中, 见IsValueChosen(q).

   ➢   最后, 如果$S_{q}^{p}$比更新后的$S_{q}^{q}$状态要旧, 那么q向p发送消息${{M}_{q\to p}}=(S_{q}^{q}, S_{p}^{q})$.

(2) 接受阶段

●   Phase2a子阶段:参与者p根据本地状态向量S^p判断是否可以发起针对提议P=〈b, v〉的Accept请求.它要求存在某个议会Q, 使得对于Q中的每个参与者q, 都满足$S_{q}^{p}.m=b$.这表明, p观察到Q中每个参与者都回复了编号为b的Prepare请求.在这种情况下, p将根据S^p确定提议值v:如果对于所有的参与者q, 都满足$S_{q}^{p}.P.b=-1$(即p未观察到某参与者接受过任何提议), 则v可以为任意值; 否则, v是所有$S_{q}^{p}.P$中最大提议编号对应的提议值.然后, p更新本地状态$S_{p}^{p}.P$为〈b, v〉, 并向其他所有参与者q≠p发送消息${{M}_{p\to q}}=(S_{p}^{p}, S_{q}^{p})$(即Accept请求).

在该阶段, 有两点需要特别注意:第一, 在TPaxos中, p根据它对所有参与者的观察状态确定v, 而不仅限于议会Q中的参与者, 第4节将讨论如何处理这种差别; 第二, p在确定v之后, 立即将本地状态$S_{p}^{p}.P$设置为〈b, v〉, 第3节将论述它可能带来的问题.

●   消息处理子阶段:与准备阶段中的消息处理子阶段相同.

2.2 从Paxos推导TPaxos

如前所述, TPaxos采用统一的状态与统一的消息类型.这有助于精简而高效的工程实现.但是, 这个特点也带来了TPaxos与Paxos之间的诸多差异, 给理解TPaxos造成了障碍.本节分4个步骤论证如何从Paxos推导出TPaxos, 使得TPaxos可看作Paxos的一种自然变体, 更易于理解.

Ⅰ.统一状态类型

TPaxos之所以能够采用统一的状态类型, 是因为在TPaxos中, 每个参与者都同时具有提议者、接受者与学习者的角色.一方面, 由于参与者p既是提议者也是接受者, 所以p需要维护状态(m, P), 其中, m是p承诺可以接受提议的最小编号, P=〈b, v〉是p最近一次接受的提议; 另一方面, 由于p也是学习者, 它需要在本地判断是否有值/提议已被选中, 所以p还需要维护它对其他所有参与者的观察状态.综上所述, 在TPaxos中, 每个参与者p需要维护一个大小为N的状态向量, 即S^p.

Ⅱ.统一消息内容

在状态类型统一的基础上, 我们进一步要求, 每次p与q通信时, p将它的真实状态$S_{p}^{p}$发送出去.需要注意的是, 该步骤并未统一消息类型.这是因为协议还需要在消息中添加类似“1a”, “2a”等标志信息, 以区分多个子阶段.第Ⅲ步推导将论述如何统一消息类型.另外, 这步推导不要求发送p对q的观察状态$S_{q}^{p}$.TPaxos采用的消息类型${{M}_{p\to q}}=(S_{p}^{p}, S_{q}^{p})$中, $S_{q}^{p}$的作用将在第Ⅳ步推导中论述.

Ⅲ.统一消息类型

Paxos使用了消息类型以区分4个子阶段, 为了统一这4种消息类型, 我们先论证如何统一某些子阶段, 然后讨论如何避免通过消息类型区分子阶段.

a) 将子阶段Phase1b与Phase2b统一为消息处理阶段.

●   一方面, 在Paxos规约的Phase2b(a)动作中, 接受者a在接受类型为“2a”并且携带提议〈m.bal, m.val〉的消息m时, 不仅更新了〈maxVBal[a], maxVVal[a]〉, 也同时将maxBal[a]更新为m.bal(条件m.bal≥maxBal[a]成立).也就是说, 接受者a在接受某提议时, 可以同时作出“不再接受具有更小编号的提议”的承诺.

●   另一方面, 经过第Ⅱ步的推导, 接受者q收到的来自p的信息$不仅包含提议编号m, 还包含p最近接受的提议P=〈b, v〉.根据Paxos的Phase1b阶段, 如果条件$S_{q}^{q}.m<S_{p}^{p}.m$成立, q就将$S_{q}^{q}.m$更新为$S_{p}^{p}.m$.然而我们注意到, 若条件$S_{q}^{q}.m<S_{p}^{p}.P.b$成立(注意, $可能已被更新), 那么q也可以接受提议$.

综上所述, 在Phase1b与Phase2b子阶段, 接受者都可以(在各自条件成立的情况下)既作承诺又接受提议.因此, 我们可以将这它们统一为一个阶段, 即消息处理阶段.需要注意看到, 由于在第Ⅱ步推导中, p不需要发送它对q的观察状态$S_{q}^{p}$, 因此第Ⅱ步推导得出的消息处理阶段只包含对$S_{q}^{q}$的更新, 而不包含对$S_{p}^{q}$的更新.此外, q需要将$S_{q}^{q}$回复给p.与TPaxos最终版本不同的是, 该回复是无条件执行的.这将在第Ⅳ步推导中论述.

b) 消除消息标志.

经过前面的推导, 目前我们得到的协议包含3个阶段, 分别是准备阶段、接受阶段与消息处理阶段.为了区分各个阶段, (统一内容的)消息中仍需携带标志信息.下面我们说明这些标志信息是可以避免的.

●   首先, 在Paxos中, 接受者通过判断收到的消息类型是“1a”还是“2a”来确定进入Phase1b还是Phase2b子阶段.由于在第Ⅲ-a)步推导中, Phase1b与Phase2b被统一成消息处理阶段, 所以不需要再区分消息类型“1a”与“2a”.

●   其次, 在Paxos的Phase2a(b, v)阶段, 提议者需要收集类型为“1b”且携带提议编号b的消息.它们是由接受者发送的针对编号为b的Prepare请求的回复.在TPaxos中, 参与者p可以通过S_q^p.m=b是否成立来判断q是否发送了这样的回复.

●   最后, 在Paxos中, 接受者使用类型为“2b”的消息, 将它最新接受的提议通知给学习者.由于在TPaxos中, 参与者同时具有3种角色, 因此不再需要发送该类消息.参与者可以根据本地状态向量判断是否有提议已被选中.

Ⅳ.优化消息处理阶段

在第Ⅲ-a)步推导中, 参与者在消息处理阶段会将自身真实状态无条件地回复给消息的发送者, 这导致任意两个参与者之间都会无休止地互相发送消息, 交换各自的状态信息.为了避免这种情况, TPaxos作了如下优化:首先, p发送给q的消息会携带p对q的观察状态, 也就是说, 统一的消息类型变成${{M}_{p\to q}}=(S_{p}^{p}, S_{q}^{p})$; 其次, 在q的消息处理阶段, 只有当观察状态$S_{q}^{p}$比更新后的$S_{q}^{q}$状态要旧时, q才回复消息${{M}_{q\to p}}=(S_{q}^{q}, S_{p}^{q})$给p.

3 TPaxos与TPaxosAP的TLA+规约及证明

本节使用TLA+描述TPaxos.我们发现, TPaxos协议描述中存在至关重要但并未充分阐明的微妙之处:在消息处理阶段, 参与者是先作出“不再接受具有更小编号的提议”的承诺还是先接受提议?这可能导致对TPaxos的两种不同理解, 并促使我们提出TPaxos的一种变体, 称为TPaxosAP.在TPaxosAP中, 参与者先接受提议后作承诺.虽然在TLA+规约层面, TPaxosAP与TPaxos(先作承诺后接受提议)相差甚小, 但它却体现了不同的投票机制.具体来讲, Paxos协议的投票机制Voting^[13]仍适用于TPaxos, 却不能完整刻画TPaxosAP的行为.在本节, 我们将举例说明TPaxosAP与TPaxos的不同之处, 并论证TPaxosAP的正确性.

3.1 TPaxos的TLA+规约 3.1.1 常量

与Paxos对应, TPaxos的TLA+规约也包含3个常量.

●   Value:所有可能的提议值构成的集合(例如{v₁, v₂, v₃}), None表示不属于Value的某个值.

●   Participant:所有参与者构成的集合(例如{p₁, p₂, p₃}), 每个参与者都同时是提议者、接受者与学习者.

●   Quorum:由参与者形成的议会系统.

为了避免多个参与者使用相同的提议编号发起多个Accept请求, 我们使用Bals(p)为参与者预分配可用的提议编号^[3](如, p₁使用{1, 4}, p₂使用{2, 5}, p₃使用{3, 6})(Paxos规约未采用预分配提议编号的方式.这有两个原因:第一, 在Phase1a(b)与Phase2a(b, v)阶段, 提议者并不改变自身状态, 所以可由任意提议者执行; 第二, 它在Phase2a(b, v)中, 通过消息类型限制了最多只会产生一个针对提议编号b的Accept请求).其中, Ballot是所有可能的提议编号构成的集合, NP是参与者数目, PIndex为参与者分配了索引.

3.1.2 变量

在TPaxos中, 每个参与者都维护一个状态向量, 包含自身的实际状态以及它对其他参与者的观察状态.参与者之间交换具有统一类型的消息, 不断更新状态向量, 进而达成共识.因此, TPaxos的TLA+规约需要维护如下变量.

●   state:全局状态矩阵.其中, state[p][q]表示参与者p对参与者q的观察状态(即$S_{q}^{p}$), state[p]则表示p维护的状态向量(即S^p).每个状态(定义见state)包含3个分量(maxBal, maxVBal, maxVVal), 含义与第2.1节中的(m, b, v)一一对应.

●   msgs:所有已发送消息构成的集合.Message表示所有可能的消息, 它定义了格式统一的消息.需要注意看到, 为了简化消息广播过程, 我们选择每次发送整个状态向量.消息接收者可以根据需要提取协议规定的部分状态信息进行处理.

TypeOK给出了变量state与msgs的类型约束.Init给出了初始状态下变量state与msgs的值.

3.1.3 动作

TPaxos包含3个动作, 分别是发起准备请求、消息处理以及发起接受请求.

●   Prepare(p, b):参与者p选取提议编号b, 发起Prepare请求.它要求b是预分配给p的编号, 并且b > state[p][p].maxBal.p先将state[p][p].maxBal更新为b, 然后广播当前本地状态向量state’[p].

●   OnMessage(q):参与者q处理收到的消息m∈msgs.消息m的发送者记为p≜m.from.表达式m.state[p]从消息m中抽取p发送的自身真实状态.q先根据m.state[p]更新本地状态向量, 包括q的真实状态state[q][q]以及q对p的观察状态state[q][p], 见UpdateState(q, p, pp≜m.state[p]).其中, 前3条更新观察状态, 后3条更新真实状态, 如第2.1节所述, 包括“先作承诺(将state[q][q].maxBal更新为pp.maxBal)后接受(分别将state[q][q].maxVBal与state[q][q].maxVVal更新为pp.maxVBal与pp.maxVVal)”这两个步骤.然后, 如果p对q的观察状态m.state[q]比更新后的state’[q][q]状态要旧, 则q广播当前本地状态向量state’[q].最后, 为了避免q不必要地重复处理消息m, 该规约将q从m.to中移除.

●   Accept(p, b, v):参与者p发起针对提议〈m, b, v〉的Accept请求.

   ➢   第1个前置条件要求提议编号b是参与者p的预分配编号, 从而避免多个参与者使用相同的提议编号b发起多个Accept请求.

   ➢   第2个前置条件避免参与者接受违背其承诺的提议.下面我们通过示例论述该条件的必要性.假设有5个参与者p₁~p₅, 见图 3.首先, p₁执行Prepare(1).p₂~p₅收到该Prepare请求后, 更新状态并回复p₁.此时, 所有参与者的状态如图 3第1行所示.接着, p₂执行Prepare(2).p₁和p₃收到该Prepare请求后, 更新状态并回复p₂, 见图 3第2行.然后, p₂执行Accept(2, v₁).p₁收到该Accept请求并更新状态, 见图 3第3行.此时, p₁观察到存在议会p₃~p₅, 它们的maxBal为1.如果没有前置条件2=state[p][p].maxBal≤b=1, 则p₁可以执行Accept(1, v₁), 并接受提议〈1, v₁〉.这违背了它“不再接受编号小于state[p][p].maxBal=2的提议”的承诺.

   ➢   前3个前置条件共同保证OneValuePerBallot成立, 证明见第3.3节.其中, 如果第3个前置条件不成立, 即state[p][p].maxVBal=b, 则表示p已经执行过一个Accept(p, b, v).然而, 仅有第3个前置条件并不能避免p多次执行Accept(p, b, v).这是因为, p可能会在之后的OnMessage动作中接受具有更大编号的提议, 从而使得state[p][p].maxVBal > b.

   ➢   第4个前置条件要求存在某个议会Q∈Quorum, 使得Q中的每个参与者q都回复了针对b的Prepare请求, 即有state[p][q].maxBal=b.

   ➢   第5条合取式描述了根据本地状态向量state[p]确定值v的方法.第6条合取式更新p的真实状态, 即p接受了提议〈b, v〉.第7条合取式表示向其他参与者广播本地状态向量state’[p].

3.1.4 行为

Next定义了次态关系.Spec定义了完整的行为规约.

3.2 TPaxosAP的TLA+规约

TPaxosAP与TPaxos的唯一不同在于:在消息处理阶段, OnMessage(q)的UpdateState(q, p, pp)中, 参与者q先接受提议〈pp.maxVBal, pp.maxVVal〉后作承诺.

需要注意看到, 在TLA+规约中, 判断q能否接受提议的条件state[q][q].maxBal≤pp.maxBal中使用的是当前值state[q][q].maxBal, 而不是像TPaxos那样使用了先作承诺而更新后的maxB.

下面我们举例说明TPaxosAP与TPaxos的不同之处.假设某参与者q收到了来自p的消息, 消息内容包含〈m, b, v〉≜〈state[p][p].maxBal, state[p][p].maxVBal, state[p][p].maxVVal〉, 且m > b.如果p的状态“领先”于q, 比如p比q多执行过几次Prepare与Accept, 则对TPaxos与TPaxosAP来说, q都可以在OnMessage(q)中既作承诺又接受提议.具体而言, 在TPaxosAP中, 〈state[q][q].maxBal, state[q][q].maxVBal, state[q][q].maxVVal〉被更新为〈m, b, v〉.这可以看作q先将其更新为〈b, b, v〉, 然后再更新为〈m, b, v〉, 相当于q先处理了针对提议〈b, v〉的Accept请求, 然后处理了针对提议编号m的Prepare请求.然而在TPaxos中, q会将它的真实状态更新为〈m, -, -〉(-表示相应分量保持不变).这相当于q先处理了针对提议编号m的Prepare请求, 从而导致它不能再接受提议〈b, v〉.

我们将在第4节中论述TPaxosAP和TPaxos代表两种不同的投票机制.然而除了上述情况, TPaxosAP与TPaxos在实际应用中没有较大区别.

3.3 TPaxos与TPaxosAP的正确性

我们证明TPaxos与TPaxosAP满足第1.5节介绍的两个条件OneValuePerBallot与SafeAt(b, v), 从而保证了一致性(consistency)条件.SafeAt(b, v)由Accept动作的第4个和第5个合取式(确定值v)保证, 其证明与Lamport使用TLAPS证明Paxos的子阶段Phase2a保证了SafeAt(b, v)^[21]类似.下面我们证明TPaxos与TPaxosAP满足OneValuePerBallot.该证明仅用到Accept动作的前3个前置条件, 因此对TPaxos与TPaxosAP都适用.我们先介绍两个简单的引理.

引理1.  对任意参与者p, 它接受过的提议编号state[p][p].maxVBal是(非严格)单调递增的.

引理2.  对任意参与者p, 它承诺可以接受提议的最小编号始终大于等于它接受过的提议编号, 即满足:

$ state\left[ p \right]\left[ p \right].\mathit{max}Bal\ge state\left[ p \right]\left[ p \right].\mathit{max}Bal. $

OneValuePerBallot保证对于任意提议编号b, 最多对应一个提议〈b, v〉, 即最多执行一次Accept(_, b, _)(_表示该分量可为任意值).注意到Accept(_, b, _)的第1个前置条件b∈Bals(p)要求, 只有b的拥有者p才能使用b执行Accept(p, b, _), 故只需要保证参与者p最多执行一次Accept(p, b, _)即可保证OneValuePerBallot.

假设在时刻t, 参与者p执行了Accept(p, b, _), 此时state[p][p].maxVBal=b.由Accept(p, b, _)的第3个前置条件state[p][p].maxVBal≠b可知, p不能在state[p][p].maxVBal=b的情况下执行Accept(p, b, _).

根据引理1, 在任意时刻t’≥t, 都有state[p][p].maxVBal≥b.当state[p][p].maxVBal > b时, 根据引理2可得, state[p][p].maxBal≥state[p][p].maxVBal > b.由于Accept(p, b, _)的第2个前置条件state[p][p].maxBal≤b的限制, p在时刻t’≥t也不能执行Accept(p, b, _).综上所述, 对于提议编号b, 它的拥有者p最多只能使用b执行一次Accept(p, b, _), 从而保证了OneValuePerBallot.

4 TPaxos与TPaxosAP的精化

本节建立从TPaxos到Consensus以及TPaxosAP到Consensus的精化关系.对于TPaxos, 我们仍采用Paxos所使用的Voting^[13]机制(第1.5节), 建立了从TPaxos到Voting的精化关系.对于TPaxosAP, 我们发现Voting并不能完整刻画TPaxosAP的行为, 因此, 我们首先提出了一种新的投票机制, 称作EagerVoting.EagerVoting允许参与者在接受提议的同时, 作出比Paxos/TPaxos更“激进”的“不再接受具有更小编号的提议”的承诺.然后, 我们建立了从TPaxosAP到EagerVoting以及从EagerVoting到Consensus的精化关系.

需要注意看到, 在TPaxos与TPaxosAP规约的Accept(p, b, v)动作中, 参与者p在前置条件满足的情况下, 需要根据本地状态向量state[p]确定值v.然而, 在Voting(第1.5节)与EagerVoting(将在第4.2.1节介绍)的VoteFor(a, b, v)动作中, 参与者需要根据某个议会的状态(而不是所有参与者)确定值v.这并不会影响协议的正确性.但是不难论证:存在某些情况, 使得两种方案确定的v值不同.这给构建从TPaxos到Voting以及从TPaxosAP到EagerVoting的精化关系造成了障碍.为此, 在本节, 我们修改TPaxos与TPaxosAP的Accept(p, b, v)动作, 改用“从议会确定值v”的方案(我们将如下两个相关问题列入未来工作:第一, 如何修改Voting的VoteFor动作, 使其采用“从全体参与者确定值v”的方案?第二, 如何在采用不同(“确定值v”的)方案的Voting之间建立精化关系?).修改后的Accept(p, b, v)动作如下所示.

4.1 TPaxos的精化

TPaxos采取了与Paxos相同的投票机制, 都可以用Voting^[21]规约(第1.5节)来刻画.本节构建从TPaxos到Voting的精化关系.TPaxos中的动作与Voting中的动作存在着明确的对应关系.具体而言,

●   在TPaxos的Preapare(p, b)中, 参与者p将state[p][p].maxBal增加至更大的提议编号b.这对应于Voting中的IncreaMaxBal(a, b)动作(此处a=p).具体而言, Prepare(p, b)中的前置条件state[p][p].maxBal < b对应于IncreaMaxBal(a, b)中的前置条件maxBal[a] < b.另外, Prepare(p, b)中的状态更新(将state[p][p].maxBal更新为b)也对应于IncreaMaxBal(a, b)中的状态更新(将maxBal[a]更新为b).

●   在TPaxos的Accept(p, b, v)中, 参与者p在确定值v之后, 随即接受了提议〈b, v〉.这对应于Voting中的VoteFor(a, b, v)动作(此处a=p).具体而言,

   ➢    Accept(p, b, v)中的第2个前置条件state[p][p].maxBal≤b与第3个前置条件state[p][p].maxVBal≠ b分别对应于VoteFor(a, b, v)中的第1个前置条件maxBal[a]≤b与第2个前置条件:

$ \forall vt\in votes\left[ a \right]:vt\left[ 1 \right]\ne b. $

   ➢    VoteFor(a, b, v)中的第3个前置条件∀c∈Acceptor\{a}:∀vt∈votes[c]:(vt^[1]=b)⇒(vt^[2]=v)与第2个前置条件共同保证OneValuePerBallot.在Accept(p, b, v)中, OneValuePerBallot由它的前3个前置条件共同保证.

   ➢    Accept(p, b, v)“从议会Q∈Quorum确定值v”的方法与VoteFor(a, b, v)中的ShowsSafeAt(Q, b, v)对应.

   ➢    Accept(p, b, v)中的状态更新(分别将state[p][p].maxVBal与state[p][p].maxVVal更新为b与v)对应于VoteFor(a, b, v)中对votes的更新(将提议〈b, v〉加入到votes[a]中), 表示参与者a(即p)接受了提议〈b, v〉.

   ➢    VoteFor(a, b, v)会将max[a]更新为b.对于TPaxos, 参与者p可以执行Accept(p, b, v), 表明p已执行过Prepare(p, b)并更新了state[p][p].maxBal=b.根据第3.1.3节对前置条件state[p][p].maxBal≤b的分析可知:在p执行Accept(p, b, v)时, state[p][p].maxBal=b仍然成立.

●   现在考虑TPaxos中的OnMessage(q)动作(第3.1节).参与者q收到了来自p≜m.from的消息m∈msgs.记pp≜m.state[p]为m中携带的p的真实状态, 即(pp.maxBal, pp.maxVBal, pp.maxVVal).在UpdateState(q, p, pp)中, q需要根据pp更新自身真实状态state[q][q].这里可能有两种更新结果:

   ➢   第1种是只“作承诺”, 即将state[q][q].maxBal更新至pp.maxBal.此时, “接受提议”的条件不再成立.这种情况对应于Voting中的IncreaMaxBal(a, b)动作(此处a=p, b=pp.maxBal).

   ➢   第2种是“作承诺”且“接受提议”, 即将state[q][q].maxBal更新至pp.maxBal, 并且分别将state[q][q].maxVBal与state[q][q].maxVVal更新为pp.maxVBal与pp.maxVVal.这要求state’[q][q].maxBal=pp.maxBal=pp.maxVBal成立(state’[q][q].maxBal为“作承诺”更新后的值).因此, 这种情况对应于Voting中的VoteFor(a, b, v)动作(此处a=p, b=pp.maxVBal, v=pp.maxVVal).

为了构建从TPaxos到Voting的精化关系, 我们需要在TPaxos规约中模拟Voting中的变量maxBal与votes, 即参与者承诺可以接受提议的最小编号以及已接受的提议构成的集合, 见模块TPaxosWithVotes.从上面的分析可以得出, Voting中的maxBal[p]对应于TPaxos中的state[p][p].maxBal.因此, 针对maxBal, 我们定义精化映射为maxBal≜[p∈Participantastate[p][p].maxBal].对于votes, 我们在TPaxos的基础上添加辅助变量votes^{[15, 22]}(在TPaxosWithVotes模块中, 故与Voting中的votes冲突), 为每个参与者p收集它已接受过的提议votes[p].具体而言, 在Prepare(p, b)中, 参与者p未接受任何提议, 所以在PrepareV(p, b)中, votes保持不变.在Accept(p, b, v)中, 参与者p接受了提议〈b, v〉, 所以在AcceptV(p, b, v)中, 我们将〈b, v〉添加到votes[p].在OnMessage(q)中, 如果state[q][q].maxVBal发生了改变, 则表明q接受了新的提议(这是因为OneValuePerBallot成立).在OnMessageV(q)中, 我们将该提议添加到votes[q].最后, TPaxosWithVotes模块给出了从TPaxos到Voting的精化映射(即用辅助变量替换Voting中的对应变量):V≜INSTANCE Voting WITH Acceptor←Participant, maxBal←maxBal, votes←votes.

4.2 TPaxosAP的精化

我们先介绍适用于TPaxosAP的投票机制EagerVoting, 然后建立从TPaxosAP到EagerVoting以及从EagerVoting到Consensus的精化关系.

4.2.1 EagerVoting规约

根据第4.1节的分析, 在TPaxos中, 每个参与者p要么仅提高它承诺不再接受的最小提议编号state[p][p]. maxBal, 要么在接受提议〈b, v〉的同时, 也将state[p][p].maxBal更新为b.这与Voting规约是相符的.然而, Voting并不能完全刻画TPaxosAP的行为.如第3.2节所述, TPaxosAP与TPaxos的行为在OnMessage(q)消息处理阶段的状态更新UpdateState(q, p, pp)方面有所不同:在TPaxosAP中, 参与者先接受提议〈pp.maxVBal, pp.maxVVal〉(即更新state[q][q].maxVBal与state[q][q].maxVVal)后作承诺(即将state[p][p].maxBal提高至pp.maxBal).这可能导致更新后的state[p][p].maxBal不等于pp.maxVBal, 从而违反了Voting规约.

这种情况是有可能发生的.考虑如下示例.

假设有3个参与者p₁~p₃, p₁先执行Prepare(1).p₂, p₃收到该Prepare请求后更新状态并回复p₁.接着, p₁执行Accept(1, v₁)以及Prepare(2), 并发送携带〈2, 1, v₁〉的Prepare请求.如果p₂与p₃收到该请求并将自身状态更新为〈2, 1, v₁〉, 则违反了Voting规约.

为了弥补Voting的不足, 我们提出一种新的适用于TPaxosAP的投票机制, 称为EagerVoting.EagerVoting与Voting的唯一不同在于:在VoteFor(a, b, v)动作中, 我们允许参与者a在接受提议〈b, v〉的同时, 将maxBal[a]提高到比b更大的提议编号c≥b.

直观地讲, Voting与EagerVoting是等价的.

●   一方面, 由于Voting的每个动作都是EagerVoting所允许的, 因此Voting的每个行为也都是EagerVoting所允许的.

●   另一方面, 如果EagerVoting的动作VoteFor(a, b, v)在更新maxBal[a]时选择的提议编号c等于b, 则该动作与Voting中的VoteFor(a, b, v)等价; 如果c大于b, 则该动作可以看作Voting中的VoteFor(a, b, v)与IncreaseMaxBal(a, c)的组合.

因此, EagerVoting的每个行为都可以被Voting中的行为所模拟(如果要使用精化技术严格证明EagerVoting可以被Voting所以模拟, 需要找到从EagerVoting到Voting的精化映射.我们将其列为未来工作).

4.2.2 从EagerVoting到Consensus的精化

为了构建从EagerVoting到Consensus的精化关系, 我们需要在EagerVoting中模拟Consensus规约中的变量chosen, 即协议已选中的值构成的集合, 见EagerVotingWithChosen.一个提议b, v以及它包含的值被选中当且仅当该存在某个议会Q∈Quorum的接受者都接受了该提议, 见ChosenAt(b, v).辅助变量chosen则收集了所有被选中的值.最后, 该模块给出了从EagerVoting到Consensus的精化映射C≜INSTANCE Consensus WITH Acceptor←Acceptor, chosen←chosen, 即用辅助变量chosen替换Consensus中的变量chosen.

4.2.3 从TPaxosAP到EagerVoting的精化

第4.1节描述的TPaxos和Voting之间的对应关系在TPaxosAP和EagerVoting之间仍然成立.需要注意看到, 根据第4.2.1节的论述, TPaxosAP的OnMessage(q)动作对“先接受提议后作承诺”的改动对应于EagerVoting的VoteFor(a, b, v)动作对“允许将maxBal[a]提高到c≥b”的改动.因此, TPaxosAP中的动作与EagerVoting中的动作也存在着明确的对应关系.从TPaxosAP到EagerVoting的精化关系与从TPaxos到Voting的精化关系相同, 构建方法也相同, 此处不再赘述.

5 模型检验

本节使用TLC模型检验工具验证TPaxos与TPaxosAP算法的正确性, 并且验证了从TPaxos到Voting及从TPaxosAP到EagerVoting的精化关系的正确性.

5.1 实验设置

在所有的实验中(基于Lamport给出的从Voting到Consensus的TLAPS证明^[21], 我们使用TLAPS定理证明系统^[23]证明了从EagerVoting到Consensus的精化关系的正确性^[24]), 我们调整了参与者集合Participant、提议值集合Value、提议编号集合Ballot的大小, 并将前两者设置为对称集^[10], 以提高TLC的验证效率.我们使用了10个线程进行了实验, 以下是我们的实验统计结果:已遍历(BFS方式遍历)的系统状态图的直径、TLC已检验的所有状态的数量、TLC已检验的不同状态的数量以及检验时间(格式为hh:mm:ss).当TLC已检验的不同状态数的数量超过某个阈值(设置为1亿, 以3个提议编号、3个提议值和3个参与者为例, 此时, 变量state总共有27个分量, 粗略估计状态数最多有3²⁷(约为万亿量级)), 我们就人为地停止该次实验.

实验所用的机器配置如下.

●   机器1:2.40GHz GPU, 6核以及64GB内存, TLC^[25]版本号为1.6.0.负责TPaxos相关实验.

●   机器2:2.10GHz GPU, 6核以及64GB内存, TLC版本号1.6.0.负责TPaxosAP相关实验.

5.2 验证结果 5.2.1 TPaxos与TPaxosAP满足Consistency

表 1和表 2分别给出了在不同配置下, 验证TPaxos及TPaxosAP满足一致性的结果.总体而言:在相同配置下, 这两种协议的模型检验结果相似.在不同的配置下, 参与者数量和提议编号个数对协议的规模影响较大.相对而言, 提议值的个数对协议的规模影响较小.

5.2.2 TPaxos与TPaxosAP满足Liveness

TPaxos与TPaxosAP的活性要求只有一个提议者, 即只允许某个参与者p来执行动作Prepare(p, b)及Accept(p, b, v).以TPaxos为例, 对于TPaxos的任何一个阶段, 一旦其异常终止(即没有提议被选中), 参与者p将会选择增大提议编号b重新开始新的TPaxos过程.b将最终大于所有参与者维护的值maxBal, 从而, 两个阶段将执行完成并且有提议最终被选中.

在TLA+中, 一般使用公平性来验证活性.表达式Fairness做出了相应的限制.参与者p为唯一的提议者, MaxBallot是最大的提议编号.参与者p选择MaxBallot发起Prepare(p, MaxBallot)和Accept(p, MaxBallot, v)动作, 第5条合取式保证了议会Q能接受Prepare请求和Accept请求(参与者p是根据本地状态判断能否进入Accept阶段, 条件p∈Q允许p和Q中的参与者通信以更新本地状态).表达式Liveness定义了TPaxos的活性, 即最终一定会有值被选中.

表 3和表 4分别给出了多种配置下, 验证TPaxos与TPaxosAP满足活性的结果.由于使用公平性来验证活性的方法增加了对动作的约束, 因此状态数相对而言较少.

5.2.3 TPaxos与TPaxosAP的精化

表 5和表 6分别给出了多种配置下, 验证从TPaxos到Voting与从TPaxosAP到EagerVoting精化关系的正确性.由于该组实验检验的性质包含时序操作符, 不再是定义在单个状态上的不变式, 验证算法较为复杂, 所以需要消耗更多的时间.

6 相关工作

Paxos^{[3, 4]}协议衍生出了许多变体^[26-29], 如Disk Paxos^[30]、Cheap Paxos^[31]、Fast Paxos^[19]、Generalized Paxos^[32]、Stoppable Paxos^[33]、Vertical Paxos^[34]、ByzantinePaxos^[26]、EPaxos(egalitarian Paxos)^[35]、Raft^[36]、CASPaxos^[37]等.本文关注腾讯开发的分布式存储系统PaxosStore中实现的TPaxos变体.TPaxos的新颖之处在于它的“统一性”:它为每个参与者维护统一的状态类型, 并采用类型统一的消息进行通信.我们从Paxos出发, 论证了如何逐步推导出TPaxos.基于这种推导, 我们可以将TPaxos看作Paxos的一种自然变体.

使用形式化规约语言描述分布式协议并使用相应的模型检验工具进行验证, 可有效提高协议的可信度^[38].近年来, 研究者使用TLA+/TLC描述并验证了Paxos协议及其多种变体.Lamport等人使用TLA+分别描述了Paxos^[13]、FastPaxos^[19]、Disk Paxos^[3]以及Byzantine Paxos^[39], 并使用TLC在一定规模上验证了它们的正确性. Moraru在博士论文中给出了EPaxos的TLA+规约.最近, Sutra发现并纠正了其中的错误^[40].Ongaro给出了Raft协议的TLA+规约^[41].在本文, 我们使用TLA+描述了TPaxos.在开发规约的时候, 我们发现TPaxos协议描述中存在至关重要但并未完全阐明的微妙之处:在消息处理阶段, 参与者是先作出“不再接受具有更小编号的提议”的承诺还是先接受提议?这促使我们发现了TPaxos的一种变体, 称为TPaxosAP.与TPaxos相比, TPaxosAP改动很小, 但却体现了一种不同于Voting^[13]的投票机制.

精化(refinement)技术^{[14, 15]}有助于理解Paxos各种变体的正确性以及它们之间的关系.Lampson^[26]提出了一个抽象的Paxos协议(abstract Paxos, 简称AP).AP刻画了Paxos协议的核心, 但是由于它使用了全局信息, 无法直接在分布式系统中实现.接着, 他们使用精化/模拟(refinement/simulation)技术分别建立了Paxos, Disk Paxos以及Byzantine Paoxs与AP的关系.在AP的视角下, 它们都可以看作AP的具体实现.Lamport等人提出了抽象的投票机制Voting^[13], 用于刻画接受者“作承诺”与“接受提议”两种核心行为.Voting可以看作分布式共识问题的集中式解决方案, 而Paxos是Voting的分布式实现.实际上, Lamport等人给出了从Paxos到Voting以及从Voting到Consensus的精化映射^[13].同样基于Voting, Lamport还使用精化技术从Paxos推导出了Byzantine Paxos^[26], 并使用TLC验证了它们之间的精化关系.Maric等人^[42]在HO(heard-of)模型^[43]下研究了多种Paxos^[42]变体. Maric等人首先为它们建立了一个共同的抽象, 也称为Voting, 根据Voting行为的差异, 这些Paxos变体可以被归为3类; 然后, 他们构建了这3类变体之间的精化关系, 并使用定理证明器Isabelle/HOL进行了形式化验证.在本文, 我们分别建立了从TPaxos以及TPaxosAP到Consensus的精化关系.特别地, 在TPaxosAP方面, 我们首先在Voting的基础上提出了一种适用于TPaxosAP的投票机制EagerVoting, 然后建立了从TPaxosAP到EagerVoting以及从EagerVoting到Consensus的精化关系.

7 总结与未来工作

本文深入研究了PaxosStore系统中的TPaxos协议^[8], TPaxos的新颖之处在于它的“统一性”:它为每个参与者维护统一的状态类型, 并采用统一类型的消息进行通信.

●   首先, 我们从经典的Paxos协议出发, 论证如何逐步推导出TPaxos协议.基于这种推导, 我们可以将TPaxos看作Paxos的一种自然变体.

●   其次, 我们给出了TPaxos的TLA+规约.我们发现, TPaxos协议描述中存在至关重要但并未完全阐明的微妙之处.这促使我们提出了它的一种变体, 称为TpaxosAP.

●   最后, 我们分别建立了从TPaxos以及TPaxosAP到Consensus的精化关系.特别地, 在TPaxosAP方面, 我们在Voting的基础上提出了一种适用于TPaxosAP的投票机制EagerVoting, 并使用TLC模型检验工具验证了从TPaxosAP到EagerVoting以及从EagerVoting到Consensus的精化关系的正确性.

目前, 我们正在使用TLAPS^{[11, 23, 44]}定理证明系统开发机器可检验的证明.另外, 我们计划对PaxosStore进行更全面的研究.比如, 我们将采用形式化方法(如形式化规约、精化技术、模型检验与定理证明等)研究共识层中另外两个模块的正确性:实现了Multi-Paxos^[3]功能的PaxosLog机制以及允许故障切换(failover)的一致性读写协议.