为了保证高可用性, 分布式系统通常采用数据副本技术, 将数据的不同副本存放在不同的物理节点上.为了保证低延迟并且容忍网络分区, 用户提交到某个副本节点的操作需要立即返回, 而不需要先与其他副本节点进行通信.本地副本节点上的更新操作将以异步的方式发送给其他副本节点[1-3].在这种情况下, 多个副本节点上的更新操作将产生冲突, 导致数据一致性问题.根据CAP定理[4, 5], 任何一个分布式数据副本系统都无法同时满足(强)数据一致性、可用性及网络分区容忍性这3种特性, 因此, 很多分布式系统都选择提供较弱的数据一致性[6-8], 如最终一致性与强最终一致性.最终一致性(eventual consistency)保证了当用户停止发送更新操作后, 各个副本节点最终将达到一致的状态[6, 9].但是, 最终一致性对系统的中间状态没有任何约束.强最终一致性(strong eventual consistency, 简称SEC)则要求执行了相同的更新操作集合(不要求以相同顺序执行)的副本节点具有相同的状态[2, 10].强最终一致性反映了分布式系统的安全性(safety), 它确保“坏事”一定不会发生.除此之外, 一个有用的分布式系统还需要具有活性(liveness), 它确保“好事”终将发生[11].最终可见性(eventual visibility, 简称EV)是一种基本的活性性质, 它要求所有(更新)操作最终都会被所有的副本节点交付并处理[1, 12].
CRDT(conflict-free replicated data type, 无冲突复制数据类型)[2, 10, 12]是一种抽象分布式数据类型, 它封装了并发冲突的消解策略, 向上层应用提供所需的强最终一致性.已实现的CRDT包括计数器(counter)、读写寄存器(read/write register)、集合(set)、列表(list)、哈希表(hashtable)、树(tree)与图(graph)等[2, 3, 13].NoSQL数据库, 如Redis Labs(Labs:https://redislabs.com/)(Redis(https://redis.io/r)的商用版本)与开源的Riak(https://riak.com/), 提供了对CRDT的支持.CRDT协议分为两类:基于操作的(op-based)协议与基于状态的(state-based)协议.基于操作的CRDT协议每次仅广播本地最新执行的更新操作, 而基于状态的CRDT则将副本节点状态包含在消息中广播给其他节点.CRDT协议通常需要精巧的设计, 正确性难以理解也难以保证[14].定理证明与模型检验这两种形式化方法可以有效地提高CRDT协议正确性的可靠性.定理证明的优点是可以得到可靠的结论, 缺点在于使用难度大.相对而言, 模型检验是一种易于使用的、能够自动化验证有限状态系统的正确性的技术[15].对于给定的系统模型, 模型检验技术遍历所有可能的执行, 检查系统是否满足给定的规约.模型检验方法的不足在于它仅能验证有限规模的系统的正确性.然而经验表明, 大多数错误在小规模分布式系统中就可以检测出来, 比如仅需要3个甚至更少副本节点[16].因此, 模型检验技术可以提供充分的可靠性保障.
本文旨在使用模型检验方法验证CRDT协议的正确性, 包括安全性(即最终一致性SEC)与活性(即最终可见性EV)两方面.具体而言, 我们使用TLA+[17, 18]形式化规约语言描述一系列CRDT协议, 并使用TLC[19]模型检验工具验证它们的正确性.为了便于验证一系列CRDT协议, 我们提出了一个可复用的、模块化的CRDT协议描述与验证框架.它包括网络通信层、协议接口层、具体协议层与规约层.
● 网络通信层描述副本节点之间的通信模型, 实现了多种类型的通信网络, 包括只提供最基本通信能力的基础(basic)网络、保证消息不丢失不重复的可靠(reliable)网络、满足因果关系的基础网络(basic causal network)与满足因果关系的可靠网络(reliable causal network).
● 协议接口层为CRDT协议(包括基于操作的协议与基于状态的协议)提供统一的接口:IntDo(r)封装了特定CRDT所提供的各种操作, IntSend(r)与IntDeliver(r)则封装了与网络通信层之间的交互.
● 在具体协议层, 每个协议根据需求选用合适的通信网络并实现上述接口.
● 规约层则描述了所有CRDT协议都需要满足的强最终一致性与最终可见性.
为此, 我们需要分别针对基于操作的协议与基于状态的协议, 为每个副本节点维护其执行过的更新操作集.我们使用TLA+实现了该框架.然后, 我们以AWSet(Add-Wins set)复制数据类型为例展示如何使用框架描述具体协议.最后, 我们使用TLC验证CRDT协议的正确性.
本文第1节先以计数器复制数据类型为例介绍CRDT协议的设计与实现, 然后介绍TLA+形式化规约语言并给出基于操作的计数器协议的TLA+描述.第2节介绍CRDT协议描述与验证框架, 重点介绍网络通信层、协议接口层与规约层的设计与实现.第3节以AWSet复制数据类型为例展示如何使用该框架描述具体协议, 包括基于操作的AWSet协议与基于状态的AWSet协议.第4节介绍模型检验实验与验证结果.第5节介绍相关工作.第6节总结全文, 并讨论可能的未来工作.
1 预备知识 1.1 CRDT协议简介CRDT协议可以分为两类:基于操作的(op-based)CRDT协议与基于状态的(state-based)CRDT协议[1, 2, 12].在基于操作的协议中, 每条消息仅携带自上次广播以来本地节点执行的更新操作.此类协议通常要求底层网络是可靠的, 即消息不能丢失、也不能重复交付.有些协议还对消息的交付顺序有额外要求.如果并发的更新操作之间具有可交换性, 那么此类协议可以满足强最终一致性.在基于状态的协议中, 每条消息会包含发送节点的当前状态.此类协议对底层网络的要求较低, 通常能容忍消息的丢失、重复交付与乱序交付.如果节点的状态集合在“合并(merge)”操作下能构成半格(join semilattice), 那么此类协议可以满足强最终一致性.下面, 我们以仅支持“自增(inc)”操作的计数器(counter)复制数据类型为例展示这两类CRDT协议的设计理念.
1.1.1 基于操作的计数器协议在基于操作的计数器协议中[1, 2, 12], 每个副本节点维护一个二元组(c, d):c表示计数器的当前值, d(称为更新缓冲值)表示自从上次消息广播以来该副本节点执行自增操作的次数.自增操作inc会同时增加c与d的值.每个副本节点以异步消息传递的方式将d值广播给其他副本节点, 同时将d置为0.当副本节点接收到消息d时, 它会将当前计数器的值c更新为c+d.
算法1.基于操作的计数器协议(以副本节点r为例).
1: ▷ (c, d): c for counter, d for update buffer
2: Σ=N0×N0 ▷ Σ: replica state
3: initial(·):(c, d)
4: let (c, d)=(0, 0)
5: read(·):v
6: let v=c
7: inc(·)
8: c←c+1
9: d←d+1
10: send(·)
11: broadcast d to other replicas
12: b←0
13: deliver(d)
14: c←c+d
该协议要求底层网络是可靠的.由于自增操作具有可交换性, 该协议可以保证强最终一致性.
1.1.2 基于状态的计数器协议在基于状态的计数器协议中[1, 2, 12], 每个副本节点r维护一个从副本节点到自然数的映射(也称向量)vv:对于副本节点s, vv[s]表示r已接收的来自s的自增操作的次数.副本节点r上的计数器的当前值就是它的vv向量的所有分量之和.自增操作inc仅增加本地分量vv[r]的值.每个副本节点会以异步消息传递的方式将自己的vv向量广播给其他副本节点.当副本节点接收到向量vvm时, 它会将vvm“合并”到本地向量vv中, 即将vv的每个分量vv[s]更新为vv[s]与vvm[s]中的较大值.
算法2.基于操作的计数器协议(以副本节点r为例).
1: Replica: the set of all replicas
2: Σ=Replica×(Replica→N0) ▷ Σ: replica state
3: initial(·):vv
4: ∀s∈Replica, vv[s]←0
5: read(·):v
6:
let
7: inc(·)
8: vv[r]←vv[r]+1
9: send(·)
10: broadcast vvm to other replicas
11: deliver(vvm)
12: ∀s∈Replica, vv[s]←max(vv[s], vvm[s])
该协议可以在任意网络中执行.特别地, 它不要求网络是可靠的.由于vv向量在上述“合并”操作下构成半格, 该协议可以保证强最终一致性.
1.2 TLA+简介TLA+是由Leslie Lamport开发的、适于描述并发与分布式系统的形式化规约语言[17, 18].TLA+将系统建模为状态机.一个状态机由它可能的初始状态(initial states)与一组动作(actions)来刻画.一个状态是对所有变量的一种赋值.一个动作表达了新、旧状态之间的某种关系(relation), 可用包含带撇变量(表示新状态)与不带撇变量(表示旧状态)的公式来描述.例如, x'=y+42断言新状态中x的值比旧状态中y的值大42.系统的一个行为就是一个状态序列, 它表示系统的一次可能的执行过程.
TLA+是对时序逻辑TLA(temporal logic of actions)[20]的扩展.在TLA+中, 一个系统可以表达为TLA中的一个形如Spec@Init∧W[Next]vars∧L的时序公式.其中, Init谓词(predicate)刻画了系统所有可能的初始状态, Next定义了系统的次态关系(next-state relation), W是表示“总是(always)”的时序操作符, vars是由系统中的所有变量构成的元组, L表示系统的公平性(fairness)性质.次态关系Next是由系统的所有动作构成的析取式.[Next]vars为真当且仅当Next为真(即某个动作为真, 我们称系统执行了该动作)或者vars(即所有变量)保持不变.
Init和Next刻画了系统动作发生的可能性, 公平性L则刻画了系统动作发生的必然性.公平性可以根据强弱程度分为弱公平性(weak fairness)与强公平性(strong fairness)[20]:弱公平性要求如果系统的某个动作从某时刻开始是持续可执行的(即该动作的前置条件持续被满足), 则该动作终将被执行; 强公平性要求如果系统的某个动作是频繁(无穷多次, 但不要求持续)可执行的, 则该动作终将被执行.TLA+分别使用WF和SF操作符表达系统的弱公平性和强公平性.对于动作A以及由所有变量构成的元组vars而言, WF与SF的定义如下.
$ W{{F}_{var}}(A)\triangleq \diamond \square ENABLED{{\langle A\rangle }_{vars}}\Rightarrow \square \diamond {{\langle A\rangle }_{vars}}, $ |
$ S{{F}_{vars}}(A)\triangleq \square \diamond ENABLED{{\langle A\rangle }_{vars}}\Rightarrow \square \diamond {{\langle A\rangle }_{vars}}. $ |
其中,
TLA+在TLA的基础上, 加入了一阶谓词逻辑以及ZF集合论, 从而支持丰富的数据类型与表达式.图 1总结了本文使用到的逻辑与集合操作符(operator).文献[21]给出了完整的TLA+操作符列表.
TLA+规约以模块(module)的形式组织在一起.在每个模块中, 我们可以声明常量(CONSTANTS)与变量(VARIABLES)、定义操作符(operator)或者提出定理(THEOREM P).一个模块M可以通过扩展(extend)其他模块M1, …, Mn的方式引入声明、定义与定理; 在模块M中, 写作EXTENDS M1, …, Mn.模块也可以被实例化(instantiated).考虑M模块中的实例化语句:
$ I M_{1} \triangleq \mathrm{INSTANCE} M_{1} \mathrm{WITH} p_{1} \leftarrow e_{1}, \ldots, p_{n} \leftarrow e_{n} $ |
其中, pi包含了M1中的所有常量与变量, ei是M中的合法表达式.对模块M1中的任一操作符F及其定义d, 该语句在模块M中引入了操作符IM1!F, 其定义是将d中的pi替换为相应的ei.此外, TLA+中的隐式替换规则允许我们在ej与pj相同时省略pj←ej子句.
TLC是TLA+的模型检验工具[19], 它通过遍历TLA+规约的有穷实例的状态空间验证规约的正确性.这些有穷实例被称为TLA+规约的TLC模型(models).例如, 考虑一个包含多个进程的分布式系统.在规约中, 我们使用CONSTANTS Proc表示可能的进程集合.在对该规约进行验证时, 我们需要在TLC模型中将Proc实例化为有穷的进程集合, 如Proc@{1, 2, 3}.为了体现Proc取值的特殊性, 我们也可以用TLA模型值(model value)表示进程.在TLA+, 一个模型值与其他任何值都不相等.因此, 我们可以将Proc实例化为一组模型值, 如Proc@{p1, p2, p3}.并且, 如果对一组模型值进行任意重排(比如将p1替换为p2, 将p2替换为p3, 将p3替换为p1)都不影响系统行为是否满足给定规约, 我们可以进一步将Proc标记为对称集(symmetry set)[17], 从而减少TLC需要遍历的状态空间.
模块OpBasedCounter展示了如何使用TLA+描述基于操作的计数器协议.在OpBasedCounter模块中, 每个副本节点r维护4个变量:c[r]表示计数器的当前值, d[r]表示更新缓冲值, incoming[r]表示接收消息的信道, seq[r]表示节点r已发送消息的数目.Msg表示消息类型, 其中包括d值和用来确保消息唯一性的r和seq.Init表示每个副本节点r的初始状态:c[r]=0, d[r]=0, incoming[r]={·}, seq[r]=0.Next表示每个副本节点r可能的动作:Do(r)包含更新操作Inc(r)与查询操作Read(r); Send(r)表示r将d[r]广播给其他副本节点; Deliver(r)表示r交付并处理一条消息.在OpBasedCounter中, 我们使用集合表示incoming信道, Deliver(r)中交付消息的方式建模了该协议所需的可靠网络(后文第2.3节详细描述了如何使用TLA+建模各种类型的网络).
2 CRDT协议描述与验证框架
本文旨在验证一系列CRDT协议的正确性, 包括安全性(强最终一致性SEC)与活性(最终可见性EV).为了描述众多的CRDT协议, 我们构建了一个可供复用、便于扩展的CRDT协议描述与验证框架.该框架分为4层, 包括网络通信层、协议接口层、具体协议层与规约层(如图 2所示).
● 网络通信层描述副本节点之间的通信模型, 实现了多种类型的通信网络, 包括只提供最基本通信能力的基础(basic)网络、保证消息不重复不丢失的可靠(reliable)网络、满足因果关系的基础网络(basic causal network)与满足因果关系的可靠网络(reliable causal network).
● 协议接口层为两类CRDT协议(包括基于操作的协议与基于状态的协议)提供统一的接口:IntDo(r)封装了特定CRDT所提供的各种操作, IntSend(r)与IntDeliver(r)则封装了与网络通信层之间的交互.
● 在具体协议层, 每个协议根据需求选用合适的通信网络并实现上述接口.
● 规约层则描述了所有CRDT协议都需要满足的强最终一致性与最终可见性.
本节先介绍系统模型, 然后分别介绍协议接口层、网络通信层与规约层.后文第3节以AWSet为例介绍具体协议层.
2.1 系统模型在模块SystemModel中, 常量Replica表示副本节点集合.副本节点之间通过异步消息传递进行通信.Msg表示可能的消息集合, 其类型由具体协议决定.每个副本节点r维护一个用于接收消息的incoming[r]信道, 用集合表示.
2.2 协议接口层
协议接口层模块CRDTInterface为两类CRDT协议提供统一的接口:IntInit(r), IntDo(r), IntSend(r)与IntDeliver(r).IntInit负责初始化副本节点的状态.IntDo(r)用以封装特定CRDT所提供的各种操作.IntSend(r)与IntDeliver(r)封装了与网络通信层之间的交互.具体的CRDT协议将扩展该模块, 并实现特定于该CRDT的Init, Do(r), Send(r)与Deliver(r)动作.比如, 假设某CRDT支持两个操作(在TLA+实现中对应于两个操作符)Op1与Op2, 则该CRDT所实现的Do(r)可以定义为Do(r)@IntDo(r)∧Op1∧Op2.
协议接口层的主要作用是为IntDo(r)与IntSend(r)生成唯一的动作标识.每个动作标识aid∈Aid是一个由副本节点r∈Replica与本地单调递增的序号seq[r]∈Nat构成的二元组.动作标识主要有3个方面的用途.第一, 用作消息标识符.在具体协议中, 每条被广播的消息都携带IntSend(r)动作对应的aid.因此在网络通信层, 消息具有唯一性.第二, 用作操作标识符.要验证SEC和EV, 需要为每个副本节点记录它已经执行的更新操作集.在Correctness模块中, 我们将使用IntDo(r)对应的aid标识这些更新操作.第三, 用作数据标识符.例如, 为了避免并发冲突, AWSet协议会为每个新添加的数据分配唯一的标识符(见后文第3节).
2.3 网络通信层
不同的CRDT协议对底层通信网络有不同的需求.总体而言, 基于状态的CRDT协议可以容忍消息的丢失、重复交付与乱序交付, 可以在任何网络条件下执行.基于操作的协议则要求网络是可靠的(即每条消息恰好被交付一次), 如第1.1.1节介绍的基于操作的计数器协议.此外, 有些基于操作的协议对消息的接收顺序还有特殊要求.例如, 第后文3.1节介绍的基于操作的AWSet协议需要按照因果序交付消息[1, 2].
已知的CRDT协议所依赖的网络通信类型可分为4类[1].
● 基础网络(basic network):基础网络允许消息的丢失(即从未被交付)、重复交付与乱序交付.
● 可靠网络(reliable network):可靠网络保证每条消息都被每个副本节点恰好交付一次.
● 因果网络(causal network):因果网络要求按照因果序交付消息.此处的因果序是由消息之间的“先于” (happen-before)关系[22]决定的.假设消息m1与m2分别由副本节点r1与r2广播, 则m1先于m2发生当且仅当:
➢ r1与r2是同一副本节点且m1在m2之前被广播; 或
➢ r2在广播m2之前已交付过消息m1; 或
➢ 存在消息m', 使得m1先于m'发生且m'先于m2发生.
因果网络要求各个副本节点按照消息之间的“先于”关系交付消息.也就是说, 只有当先于消息m发生的所有消息都被交付之后, m才能被交付.
● 可靠因果网络(reliable causal network):可靠因果网络同时满足可靠网络与因果网络的要求.
下面我们分别介绍以上4种网络通信类型在TLA+中的实现.具体CRDT协议可以通过TLA+提供的实例化(INSTANCE)机制引入并使用合适的网络通信类型.
2.3.1 BasicNetwork模块建模基础网络BasicNetwork模块通过扩展SystemModel模块引入表示信道的变量incoming.变量lmsg[r]表示在副本节点r上, 网络通信层向协议层交付的最近一次消息.BNBroadcast(r, m)表示副本节点r将消息m广播给其他所有副本节点.BNDeliver(r)建模副本节点r向协议层交付消息的行为:当信道incoming[r]不为空时, 它非确定性地(建模消息的乱序交付)从incoming[r]中选择一条消息m, 将其交付给协议层.需要注意的是, BNDeliver(r)并未删除m(UNCHANGED incoming), 因此可以建模消息的重复交付以及消息丢失(即存在消息永远不被交付).
2.3.2 ReliableNetwork模块建模可靠网络
ReliableNetwork模块扩展了BasicNetwork模块, 并向协议层提供额外的可靠性保障.
具体而言, ReliableNetwork保持了BasicNetwork中的消息广播行为.但是与BasicNetwork中的BNDeliver(r)不同, ReliableNetwork中的RNDeliver(r)会将已交付的消息从信道中删除, 因此消息不会被重复交付.而且在消息有限的情况下, 该设计方案可以保证每条消息最终都会被交付(即消息不会丢失).
2.3.3 CausalNetwork模块建模因果网络
CNBroadcast(r, m)建模因果网络中副本节点r广播消息m的行为:vc[r][r]分量加一, 并将更新后的本地向量时钟vc'[r]作为消息m的时间戳(保存在lvc域), 构成新的消息cm(可通过ts(cm)访问lvc), 然后将cm广播给其他副本节点.CNDeliver(r)建模因果网络中副本节点r向协议层交付消息的行为.CNCausallyReady(r, cm)用于判断消息cm是否可以被副本节点r交付, 即是否所有“先于"cm的消息都已被r交付.设广播消息cm的副本节点为mr.条件ts(cm)[mr]≤vc[r][mr]+1表示副本节点mr在广播cm之前所广播的消息都已被r交付.条件∀s≠mr, ts(cm)[s]≤vc[r][s]表示副本节点mr在广播cm之前所交付的来自其他副本节点的消息都已被r交付. CNDeliver(r)非确定性地从信道incoming[r]中选择一条满足CNCausallyReady的消息cm(实际消息为cm.m), 交付给上层协议, 并将本地向量时钟vc[r]的vc[r][mr]分量更新为Max(vc[r][mr], ts(cm)[mr]).
CausalNetwork模块扩展BasicNetwork模块, 并向协议层提供按因果序交付消息的保障.CausalNetwork模块使用向量时钟刻画消息之间的因果序[1, 23].为此, 每个副本节点r维护一个n维向量vc[r](n为副本节点数), 其中, vc[r][s]刻画了副本节点r观察到的来自副本节点s的最新消息.对任意副本节点r, s, vc[r][s]的初始值为0.
需要注意的是, CNDeliver(r)没有将cm从信道中删除, 因此允许消息的丢失与重复交付.特别地, 为了能在因果网络中建模消息的重复交付, CNCausallyReady(r, cm)使用了条件ts(cm)[mr]≤vc[r][mr]+1, 而不是ts(cm)[mr]= vc[r][mr]+1.相应地, CNDeliver(r)将vc[r][mr]更新为vc[r][mr]与ts(cm)[mr]中的较大值, 而不是设置为ts(cm)[mr].
2.3.4 ReliableCausalNetwork模块建模可靠因果网络
可靠因果网络ReliableCausalNetwork同时满足可靠网络对可靠性以及因果网络对因果序的要求.
ReliableCausalNetwork扩展了CausalNetwork, 其消息广播行为RCNBroadcast(r, m)与CausalNetwork中的CNBroadcast(r, m)相同.为了建模ReliableCausalNetwork的可靠性, RCNDeliver(r)会将交付给上层协议的消息cm从信道中删除.特别地, 由于该网络不允许消息的重复交付, 与CausalNetwork中的CNCausallyReady(r, cm)相比, RCNCausallyReady(r, cm)可以改用稍强的ts(cm)[mr]=vc[r][mr]+1条件.相应地, 在RCNDeliver(r)中, 可以将vc[r][mr]更新为ts(cm)[mr].
2.4 规约层
规约层给出了所有CRDT协议都应满足的强最终一致性(SEC)和最终可见性(EV)的形式化定义.强最终一致性要求(交付)执行了相同更新操作集的副本节点应具有相同的状态.最终可见性要求每个(本地)更新操作最终会被交付给所有副本节点.为此, 在模块Correctness中, 每个副本节点r维护了两个集合:doset[r]是它产生的更新操作构成的集合, delset[r]是它交付(执行)过的更新操作构成的集合.另外, 模块Correctness假设每个CRDT都提供一个读操作Read(r∈Replica), 用于返回副本节点r的当前状态.使用Read与delset, 强最终一致性可以定义为SEC@∀r1, r2∈Replica:delset[r1]=delset[r2]⇒Read(r1)=Read(r2).使用doset与delset, 最终可见性可以定义为
其中, ∀aid∈Aid枚举所有可能的更新操作.时序操作符
如第2.2节所述, 我们使用动作标识符aid代表更新操作.在CDo(r)中, 新产生的本地更新操作(的动作标识符)被添加到doset[r]和delset[r](本地操作立即交付执行)中.副本节点之间需要通过消息广播交换它们已执行过的更新操作集.UMsg定义了此类消息的类型:aid用于唯一标识每条消息, update是需要广播的更新操作集.为了将协议的实现与验证解耦, 我们使用与incoming独立的uincoming信道发送、交付UMsg消息.也就是说, 在具体协议的Send(r)动作中, 验证正确性所需的UMsg消息(使用uincoming[r]信道)会伴随协议发送的消息(使用incoming[r]信道)一同广播给其他副本节点.它们具有相同的aid(均由Send(r)决定).具体协议的Deliver(r)在交付了某条消息m后, 可以使用CDeliver(r, m.aid)取出与m一同被广播的UMsg消息um, 并将um携带的更新操作集um.update合并到副本节点r的更新操作集delset[r]中.
在CSend(r)中, 哪些更新操作需要被广播是由协议类型决定的.模块OpCorrectness与StateCorrectness扩展了Correctness, 分别针对基于操作的协议与基于状态的协议实现了广播UMsg消息的行为.具体协议可以依据协议的类型选用OpCorrectness或者StateCorrectnes.在OpCorrectness中, buset[r]表示最近一次广播之后副本节点r产生的更新操作集.OpCSend(r)每次仅广播buset[r](而非完整的delset[r]), 并清空buset[r].在StateCorrectnes中, StateCSend(r)则每次都将完整的delset[r]广播给其他副本节点.
3 CRDT协议的描述
本节以AWSet(Add-Wins set)(在参考文献[2]中, AWSet也被称为OR-Set(observed-remove set))为例, 展示如何使用框架描述具体CRDT协议.基于该框架, AWSet协议只需选择合适的底层通信网络并依照协议接口实现基本的数据添加Add与删除Remove操作.在集合数据类型上, 如果一个添加操作与另一个删除操作并发(即它们之间没有happens-before关系, 类似消息之间的happens-before关系, 同样可定义操作之间的happens-before关系)且作用在同一数据上, 则称它们产生了并发冲突.AWSet采用“添加操作胜出”的策略消解并发冲突[1, 2, 24].因此, 某数据在AWSet中当且仅当存在某个添加操作添加了该数据, 并且所有删除该数据的操作要么“先于”(在操作之间的happens-before关系下)该添加操作要么与该添加操作并发.
本节实现两个已有的AWSet协议:基于操作的AWSet协议(OpAWSet)[1, 2]与基于状态的AWSet协议(StateAWSet)[1, 2].为了消解并发冲突, AWSet协议为每个被添加的数据(包括重复添加的数据)分配唯一的标识(使其成为“元素”).删除数据d则转化为删除当前副本节点上所有数据域为d的元素.因此, 原本存在并发冲突的数据添加与删除操作被转化为没有并发冲突的元素添加与删除操作.当添加操作和删除操作并发作用在同一数据上时, 删除操作未观察到添加操作所添加的元素标识, 因此该元素被保留, 即添加操作胜出.这两种AWSet协议的不同之处在于:OpAWSet每次仅广播自上次广播以来本地节点添加与删除的元素, 而StateAWSet则需要广播本地节点当前的完整状态.在AWSet模块中, Element定义了元素的类型:d表示数据, 即实际被添加到AWSet中的数据; (r, k)表示元素的标识, 由副本节点r本身与自然数k构成.OpAWSet与StateAWSet扩展了AWSet, 并各自实现Init, Do(r)(包括Add(d, r)与Remove(d, r)), Send(r)与Deliver(r)接口.
3.1 基于操作的AWSet协议在基于操作的AWSet协议[1, 2](OpAWSet模块)中, 每个副本节点r维护3个集合:活跃(active)元素集aset[r]保存r观察的被添加过且未被删除过的元素, 添加缓冲区abuf[r]保存自上次消息广播以来r本地添加的元素, 删除缓冲区rbuf[r]则保存自上次消息广播以来r本地删除的元素.此外, 基于操作的OpAWSet协议需要在可靠因果网络中执行.因此, 我们使用TLA+提供的INSTANCE机制引入ReliableCausalNetwork网络通信模块.下面, 我们分别描述该协议的初始状态Init与可能的动作Do(r), Send(r)与Deliver(r).
● 在初始状态, 每个副本节点r上的aset[r], abuf[r]与rbuf[r]都为空.
● Do(r)包含两个更新操作和一个查询操作:
➢ 更新操作Add(d, r)表示副本节点r向AWSet添加数据d.该协议为数据d分配唯一标识aid, 将元素(aid, d)加入到元素集aset[r]中.此外, 它还将该元素加入到添加缓冲区abuf[r]中.
➢ 更新操作Remove(d, r)表示副本节点r从AWSet中删除数据d.该操作删除活跃元素集aset[r]中所有数据域为d的元素(该集合记为E, E可能为空).此外, 它还将E中元素加入到删除缓冲区rbuf[r]中.
➢ 查询操作ReadOpAWSet(r)(用于实例化Correctness模块所要求的Read(r)操作, 见第4.1节)返回副本节点r上的AWSet中的所有数据.数据d在r上的AWSet中当且仅当元素集aset[r]中存在数据域为d的元素.
● Send(r)表示副本节点r向其他副本节点广播消息.消息类型为Msg@[aid:Aid, abuf:SUBSET Element, rbuf:SUBSET Element], 其中, aid用作该消息的标识符, abuf与rbuf分别为添加缓冲区abuf[r]与删除缓冲区rbuf[r].该动作将清空本地缓冲区abuf[r]与rbuf[r].
● Deliver(r)表示副本节点r向上层协议交付一条消息.要交付的消息是由底层通信网络ReliableCausalNetwork从信道incoming[r]中选择的消息lmsg'[r].首先, 副本节点r将消息中的添加元素集lmsg'[r].abuf合并到本地的set[r]中; 然后, 从其中移除在消息发送方中被删除的元素集合lmsg'[r].rbuf.
3.2 基于状态的AWSet协议
在基于状态的AWSet协议[1, 2](StateAWSet模块)中, 每个副本节点r维护两个集合:活跃(active)元素集aset[r]保存r观察到的被添加过且未被删除过的元素; tombstone集tset[r]保存r观察到的已被删除的元素.由于StateAWSet协议可以在任意网络中执行, 因此我们使用TLA+提供的INSTANCE机制引入BasicNetwork网络通信模块.下面, 我们分别描述该协议的初始状态Init与可能的动作Do(r), Send(r)与Deliver(r).
● 在初始状态, 每个副本节点r的aset[r]与tset[r]都为空.
● Do(r)包含两个更新操作和一个查询操作:
➢ 更新操作Add(d, r)表示副本节点r向AWSet添加数据d.该协议为数据d分配唯一的标识aid, 将元素(aid, d)加入到活跃元素集aset[r]中.
➢ 更新操作Remove(d, r)表示副本节点r从AWSet中删除数据d.该操作删除活跃元素集aset[r]中所有数据域为d的元素(该集合记为E, E可能为空).此外, 它还将E中元素加入到tombstone集tset[r]中.
➢ 查询操作ReadStateAWSet(r)(用于实例化Correctness模块所要求的Read(r)操作, 见第4.1节)返回副本节点r上的AWSet中的所有数据.数据d在r上的AWSet中当且仅当aset[r]中存在数据域为d的元素.
● Send(r)表示副本节点r向其他节点广播消息.消息类型为
$ Ms{{g}^{\triangleq }}=[\text{aid}:\text{Aid}, A:\text{ SUBSET Element, T:SUBSET Element }]. $ |
其中, aid用作该消息的标识符, A和T分别为活跃元素集aset[r]与tombstone集tset[r].
● Deliver(r)表示副本节点r向上层协议交付一条消息.要交付的消息是由底层通信网络BasicNetwork从信道incoming[r]中选择的消息lmsg'[r].首先, 副本节点r将消息中的tombstone集lmsg'[r], T合并到本地的tombstone集tset[r]中, 表示副本节点r观察到lmsg'[r], T的元素已被删除; 然后, 副本节点r将消息中的活跃元素集lmsg'[r].A与本地的活跃元素集aset[r]合并, 并从中移除已确认被删除的元素(即更新后的tombstone集tset'[r]).
4 CRDT协议的验证 4.1 实验设置
本节使用TLC[19]模型检验工具验证OpAWSet与StateAWSet协议的正确性, 即是否满足强最终一致性与最终可见性.实验所用的机器配置为:2.40 GHz GPU, 6核以及64GB内存(TLA+源代码与实验脚本GitHub仓库: https://github.com/JYwellin/CRDT-TLA).
在验证强最终一致性SEC的每组实验中, 我们调整副本节点集合Replica与数据集Data的大小, 并将它们设置为对称集[17](第1.2节), 以提高TLC验证效率.另外, 在OpAWSet(相应地, StateAWSet)的TLC模型中, 我们需要使用ReadOpAWSet(r)(相应地, ReadStateAWSet(r))实例化Correctness模块中定义的常量Read(r).我们使用10个线程进行实验, 并报告如下统计数据:已遍历(以BFS方式遍历)的系统状态图的直径, TLC已检验的所有状态的数量, TLC已检验的不同状态的数量以及检验时间(格式为hh:mm:ss).由于AWSet允许重复加入或者删除元素, OpAWSet与StateAWSet的每个行为都是(潜在)无穷的.当TLC已检验的不同状态的数量超过某个阈值(设置为1亿)时, 我们就人为地终止该次检验(2019年01月28日构建的TLC版本支持该功能).
在验证最终可见性EV的每组实验中, 我们调整副本节点集合Replica与数据集Data的大小(TLC暂不支持在检验活性性质时使用对称集技术[25]), 并限制doset集合的大小(即限制每个副本节点允许产生的更新操作的数量).
4.2 验证结果图 3与图 4分别给出了多种配置下验证OpAWSet与StateAWSet满足强最终一致性所需的时间(在给定配置下, 验证时间可能受多种因素影响, 包括TLC工具本身的实现技术, 比如BFS队列的并发访问策略、磁盘读写等).总体而言, 在相同配置下, 验证OpAWSet协议比验证StateAWSet协议要消耗更多的时间.这是因为基于操作的OpAWSet协议使用的是可靠因果网络ReliableCausalNetwork, 它的TLA+实现比StateAWSet协议所使用的基础网络BasicNetwork更为复杂模型.
由于规约StateAWSet中的动作Send(r)在任意时刻都是可以执行的, 因此即使在限制doset集合大小的情况下, StateAWSet的每个行为也是(潜在)无穷的.所以, 本节仅验证OpAWSet的最终可见性(在满足最终可见性方面, StateAWSet与OpAWSet的行为是类似的).图 5给出了多种配置下验证OpAWSet满足最终可见性所需的时间.
实验结果表明, 最终可见性的验证规模显著小于强最终一致性的验证规模.这主要有两个方面的原因.
● 第一, SEC是一种定义在单个状态上的安全性(safety)性质, 针对此类性质的验证算法只需检查单个状态; 而EV是定义在行为上的活性(liveness)性质, 验证此类性质的算法更为复杂, 复杂度也较高.
● 第二, 在本工作中, 我们发现doset集合的大小与副本节点数对模型的规模都有较大影响.在目前实验结果的基础上增大doset集合或增加副本节点数, 都会将需要遍历的状态图的直径从13提高到19或以上, 从而极大地增加状态数量, 检验时间也变得无法接受.
由于最终可见性较为直观, 其正确性并不直接依赖于系统的规模, 因此我们认为如图 5所示的小规模验证结果仍然有助于增强我们对OpAWSet满足最终可见性的信心.
5 相关工作模型检验与(自动/辅助)定理证明是提高分布式协议可靠性的两种常用的形式化方法.本文使用模型检验方法验证CRDT协议的正确性.下面我们介绍使用定理证明方法验证CRDT协议正确性的相关工作.与模型检验方法相比, 该类方法的优点是验证结果不受模型规模的限制, 缺点则是使用门槛较高, 难以复用与扩展.此外, 本文不仅验证了CRDT协议的安全性(即满足强最终一致性), 而且验证了它们的活性(即满足最终可见性).下述使用定理证明方法的工作均未涉及CRDT协议的活性[14, 26, 27].
Gomes等人使用Isabelle/HOL定理证明器验证了一系列基于操作的CRDT协议的正确性[14], 如计数器协议、ORSet(即AWSet)集合协议以及RGA列表协议[3, 13]等.他们构建了一个可重用的、模块化的CRDT协议描述与定理证明框架, 该框架给出了真实环境下网络的公理语义, 克服了之前工作中由于对网络作了错误假设而导致的证明失效问题.此外, 框架还基于抽象收敛定理(abstract convergence theorem)给出了强最终一致性的形式化定义.在网络通信模块, Gomes等人使用公理化方法刻画了异步不可靠因果网络.在本文, 我们则实现了更多类型的通信网络.
Nagar等人同样考虑基于操作的CRDT协议的自动验证问题[26].他们首先论证了强最终一致性对操作之间的可交换性的要求是与系统所能提供的一致性模型(如最终一致性、因果一致性、RedBlue一致性等)相关的.在此基础上, 他们提出了以一致性模型为参数的强最终一致性证明规则, 并以集合、列表与图等CRDT为例展示了如何使用该规则自动验证CRDT协议.
Zeller等人使用Isabelle/HOL定理证明器验证了一系列基于状态的CRDT协议的正确性[27].他们首先给出了基于状态的CRDT协议的参数化操作语义.在此基础上, 他们给出了多种基于状态的CRDT协议的形式化规约, 如多值寄存器(multi-value register)[2]、PN计数器协议[2]、2P集合协议[2]以及ORSet(即AWSet)集合协议等.由于TLA+规约描述了协议的初始状态以及所有可能的动作, 因此本文中的StateCorrectness(以及Correctness)规约也可以看作基于状态的CRDT协议的操作语义.除了验证所有CRDT协议都需要满足的强最终一致性之外, Zeller等人还验证了多种CRDT协议相对于各自规约的正确性.比如, 如第3节所述, AWSet的规约是“某数据在AWSet中当且仅当存在某个添加操作添加了该数据, 并且所有删除该数据的操作要么先于该添加操作, 要么与该添加操作并发”.本文关注于CRDT协议的强最终一致性与最终可见性, 并未验证它们相对于各自规约的正确性.
使用模型检验方法验证协议的正确性是提高协议可靠性的有效手段.张玉清等人[28]使用模型检测工具SMV(symbolic model verifier)分析了著名的Needham-Schroeder(NS)公钥协议.骆翔宇等人[29]使用时间自动机验证工具UPPAAL检测组合Web服务的安全性(如死锁)与活性等性质.Leslie Lamport[30]使用TLA+/TLC描述并验证了Paxos协议及其变体的正确性.本文则使用TLA+/TLC描述并验证了一系列CRDT协议的正确性.
6 总结与未来工作本文采用模型检验技术验证了一系列CRDT协议的正确性.我们首先构建了一个可复用的、模块化的CRDT协议描述与验证框架, 包括网络通信层、协议接口层、具体协议层与规约层.我们使用TLA+形式化规约语言实现了该框架, 然后以Add-Wins Set复制数据类型为例展示了如何使用框架描述具体协议, 并使用TLC模型检验工具验证协议的正确性.我们计划扩展上述框架, 使其可以描述并验证实现同一CRDT的不同协议之间的精化关系[12, 31].此外, 我们还将研究基于操作的CRDT协议与基于状态的CRDT协议之间的等价性[2], 并使用TLAPS定理证明器[18, 32, 33]给出严格的形式化证明.
只能验证有限模型的正确性, 是模型检验方法的不足之处.有文献表明, 某些协议具有“分界点(cutoff bound)”性质:如果协议在某个特定大小的有限模型上是正确的, 那么它在任意规模的模型上都是正确的.例如, Marić等人[34]证明了多种以进程数为参数的共识算法具有该性质.具体而言, 如果它们在5个或7个进程上是正确的, 那么它们在任意多个进程上都是正确的.我们计划考察CRDT协议是否具有此类性质.
[1] |
Zawirski M. Dependable eventual consistency with replicated data types[Ph.D. Thesis]. Universite Pierre et Marie Curie, 2015.
|
[2] |
Shapiro M, Preguica N, Baquero C, Zawirski M. A comprehensive study of convergent and commutative replicated data types. Research Report, RR-7506, Centre Paris-Rocquencourt, INRIA, 2011. https://hal.inria.fr/inria-00555588
|
[3] |
Attiya H, Burckhardt S, Gotsman A, Morrison A, Yang H, Zawirski M. Specification and complexity of collaborative text editing. In: Proc. of the 2016 ACM Symp. on Principles of Distributed Computing (PODC 2016). New York: Association for Computing Machinery, 2016. 259-268. https://doi.org/10.1145/2933057.2933090
|
[4] |
Gilbert S, Lynch NA. Brewer's conjecture and the feasibility of consistent, available, partition-tolerant Web services. Sigact News, 2002, 33(2): 51-59.
[doi:10.1145/564585.564601] |
[5] |
Brewer EA. Towards robust distributed systems (abstract). In: Proc. of the 19th Annual ACM Symp. on Principles of Distributed Computing (PODC 2000). New York: ACM, 2000. 7. http://dx.doi.org/10.1145/343477.343502
|
[6] |
Decandia G, Hastorun D, Jampani MM, Kakulapati G, Lakshman A, Pilchin A, Sivasubramanian S, Vosshall P, Vogels W. Dynamo: Amazon's highly available key-value store. In: Proc. of the 21st ACM SIGOPS Symp. on Operating Systems Principles (SOSP 2007). New York: Association for Computing Machinery, 2007. 205-220. https://doi.org/10.1145/1294261.1294281
|
[7] |
Lakshman A, Malik P. Cassandra: A decentralized structured storage system. Operating Systems Review, 2010, 44(2): 35-40.
[doi:10.1145/1773912.1773922] |
[8] |
Terry DB, Theimer MM, Petersen K, Demers AJ, Spreitzer M, Hauser C. Managing update conflicts in Bayou, a weakly connected replicated storage system. In: Proc. of the 15th ACM Symp. on Operating Systems Principles (SOSP'95). New York: Association for Computing Machinery, 1995. 172-182. https://doi.org/10.1145/224056.224070
|
[9] |
Vogels W. Eventually consistent. Communications of the ACM, 2009, 52(1): 40-44.
[doi:10.1145/1435417.1435432] |
[10] |
Shapiro M, Preguica N, Baquero C, Zawirski M. Conflict-free replicated data types.In: Proc. of the 13th Int'l Conf. on Stabilization, Safety, and Security of Distributed Systems (SSS 2011). Berlin, Heidelberg: Springer-Verlag, 2011, 386-400.
http://dl.acm.org/citation.cfm?id=2050613.2050642 |
[11] |
Lamport L. Proving the correctness of multiprocess programs. IEEE Trans. on Software Engineering, 1977, 3(2): 125-143. https://doi.org/10.1109/TSE.1977.229904
|
[12] |
Burckhardt S, Gotsman A, Yang H, Zawirski M. Replicated data types: Specification, verification, optimality. In: Proc. of the 41st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL 2014). New York: Association for Computing Machinery, 2014. 271-284. https://doi.org/10.1145/2535838.2535848
|
[13] |
Roh H, Jeon M, Kim J, Lee J. Replicated abstract data types: Building blocks for collaborative applications. Journal of Parallel and Distributed Computing, 2011, 71(3): 354-368.
[doi:10.1016/j.jpdc.2010.12.006] |
[14] |
Gomes VB, Kleppmann M, Mulligan DP, Beresford AR. Verifying strong eventual consistency in distributed systems. In: Proc. of the ACM Program. 2017. Article No.109. https://doi.org/10.1145/3133933
|
[15] |
Clarke Jr EM, Grumberg O, Long D. Model checking.In: Proc. of the NATO Advanced Study Institute on Deductive Program Design. Berlin, Heidelberg: Springer-Verlag, 1996, 305-349.
|
[16] |
Yuan D, Luo Y, Zhuang X, Rodrigues GR, Zhao X, Zhang Y, Jain PU, Stumm M. Simple testing can prevent most critical failures: An analysis of production failures in distributed data-intensive systems.In: Proc. of the 11th USENIX Conf. on Operating Systems Design and Implementation (OSDI 2014). USENIX Association, 2014, 249-265.
|
[17] |
Lamport L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Boston: Addison-Wesley Longman Publishing Co., Inc., 2002.
|
[18] |
Lamport L. The TLA+ hyperbook. 2019. http://lamport.azurewebsites.net/tla/hyperbook.html
|
[19] |
Yu Y, Manolios P, Lamport L. Model checking TLA+ specifications.In: Pierre L, Kropf T, eds. Correct Hardware Design and Verification Methods (CHARME 1999). Berlin, Heidelberg: Springer-Verlag, 1999, 54-66.
[doi:10.1007/3-540-48153-2_6] |
[20] |
Lamport L. The temporal logic of actions. ACM Trans. on Programming Languages and Systems (TOPLAS), 1994, 16(3): 872-923. https://doi.org/10.1145/177492.177726
|
[21] |
Lamport L. Summary of TLA+. 2019. http://lamport.azurewebsites.net/tla/summary-standalone.pdf
|
[22] |
Lamport L. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 1978, 21(7): 558-565.
[doi:10.1145/359545.359563] |
[23] |
Fidge CJ. Timestamps in message-passing systems that preserve the partial ordering[Ph.D. Thesis]. Department of Computer Science, Australian National University, 1987.
|
[24] |
Burckhardt S. Principles of eventual consistency. Foundations and Trends in Programming Languages, 2014, 1(1-2): 1-150.
[doi:10.1561/2500000011] |
[25] |
Model-values and symmetry. 2019. http://tla.msr-inria.inria.fr/tlatoolbox/doc/model/model-values.html
|
[26] |
Nagar K, Jagannathan S. Automated parameterized verification of CRDTs. arXiv preprint arXiv: 1905.05684, 2019.
|
[27] |
Zeller P, Bieniusa A, Poetzsch-Heffter A. Formal specification and verification of CRDTs.In: Proc. of the Int'l Conf. on Formal Techniques for Distributed Objects, Components, and Systems. Berlin, Heidelberg: Springer-Verlag, 2014, 33-48.
|
[28] |
Zhang YQ, Wang L, Xiao GZ, Wu JP. Model checking analysis of needham-schroeder public-key protocol. Ruan Jian Xue Bao/ Journal of Software, 2000, 11(10): 1348-1352(in Chinese with English abstract).
http://www.jos.org.cn/jos/ch/reader/view_abstract.aspx?flag=1&file_no=20001013&journal_id=jos |
[29] |
Luo XY, Xuan AC, Sha ZL. Model checking Web services based on timed automata. Computer Science, 2010, 37(8): 139-142, 197(in Chinese with English abstract).
http://d.old.wanfangdata.com.cn/Periodical/jsjkx201008029 |
[30] |
Lamport L. Fast Paxos. Distributed Computing, 2006, 19(2): 79-103.
http://d.old.wanfangdata.com.cn/NSTLQK/NSTL_QKJJ024796761/ |
[31] |
Mukund M, Shenoy RG, Suresh SP. Optimized OR-sets without ordering constraints.In: Proc. of the Int'l Conf. on Distributed Computing and Networking. Berlin, Heidelberg: Springer-Verlag, 2014, 227-241.
|
[32] |
TLAPS Website. 2019. http://tla.msr-inria.inria.fr/tlaps/content/Home.html
|
[33] |
Chaudhuri K, Doligez D, Lamport L, Merz S. A TLA+ proof system. arXiv preprint arXiv: 0811.1914, 2008.
|
[34] |
Marić O, Sprenger C, Basin D. Cutoff bounds for consensus algorithms.In: Proc. of the Int'l Conf. on Computer Aided Verification. Springer-Verlag, Cham, 2017, 217-237.
|
[28] |
张玉清, 王磊, 肖国镇, 吴建平. Needham-Schroeder公钥协议的模型检测分析. 软件学报, 2000, 11(10): 1348-1352.
http://www.jos.org.cn/jos/ch/reader/view_abstract.aspx?flag=1&file_no=20001013&journal_id=jos |
[29] |
骆翔宇, 轩爱成, 沙宗鲁. 基于时间自动机的Web服务模型检测. 计算机科学, 2010, 37(8): 139-142, 197.
http://d.old.wanfangdata.com.cn/Periodical/jsjkx201008029 |