简介： 女娲团队在过来大半年工夫里继续投入女娲2.0研发，将一致性引擎和业务状态机解耦，一致性引擎可反对Paxos、Raft、EPaxos等多种一致性协定，依据业务需要撑持不同的业务状态机。其中的一致性引擎模块是要害，研发一致性引擎时，保障一致性引擎的正确性是一大挑战，所以咱们用了TLA+、Jepsen等工具保障一致性引擎的正确性。这里分享一些Jepsen利用方面的领会。

作者 | 僧泉
起源 | 阿里技术公众号

女娲团队在过来大半年工夫里继续投入女娲2.0研发，将一致性引擎和业务状态机解耦，一致性引擎可反对Paxos、Raft、EPaxos等多种一致性协定，依据业务需要撑持不同的业务状态机。其中的一致性引擎模块是要害，研发一致性引擎时，保障一致性引擎的正确性是一大挑战，所以咱们用了TLA+、Jepsen等工具保障一致性引擎的正确性。这里分享一些Jepsen利用方面的领会。

目前网上曾经有了对于Jepsen的介绍，比方《Jepsen测试》《当 Messaging 遇上 Jepsen》,从原理和用法都有详尽的阐明，做到了致宽广而尽轻微。大家能够先浏览这些文章，对Jepsen有一个全面的理解，也能够在某些细节没搞懂时去看看文章中具体的论述。本文相当于是摘要、总结和补充，一方面给大家对Jepsen的一个直观的意识，一方面通过介绍女娲在应用Jepsen时的例子，理论阐明Jepsen的作用与特点，给大家实际过程中应用Jepsen一些参考。

这里咱们依照实质、构造、作用 的程序扼要地形容Jepsen。

一 实质——只看Jepsen的特色

在分布式系统的测试畛域，最耳熟能详的两大工具，就是TLA+和Jepsen了，其关系相似于演绎与演绎，白盒与黑盒。TLA+要求编写测试的人可能实在地形象出须要验证的分布式系统，在每一个轻微的逻辑局部做到对实在零碎精炼而精确的还原，而后对这个形象零碎在各种状态空间进行遍历，如果验证形象零碎始终满足定义的规定，则可推断并保障实在零碎的正确性，就好比有了一份要害信息详实的地图，在地图上画通了路线图，真实世界按路线走也能够走到起点。Jepsen则是从零碎对外提供的接口动手，通过理论构建零碎、进行操作、注入谬误、验证后果这一系列在谬误注入状况下对系统行为的演练和剖析，实在地撞出不合乎既定规定的状况，通过对历史记录的剖析找到这些状况，好比造出了一大堆散乱的拼图，各种尝试，最初验证能不能拼成一个正当而规定的图形。

由此咱们不难看出两者的难点。TLA+的难点在演绎的正确性，用TLA+写的模型，前提是形象零碎与实在零碎要害局部实现都要完全符合，如果与工程实现不符，就会导致一些实在零碎中可能会遇到的问题不能被验证到。而Jepsen最大的难点，则是依据收集测试用例中的历史记录，如何演绎出零碎是否呈现相应的谬误，而且演绎自身特点也决定，Jepsen测试不能涵盖所有异常情况。在这个演绎的过程中，线性一致性是最难演绎验证的，零碎线性一致性的验证也是Jepsen最大特色。


图1. Jepsen提供的一致性验证能力

一句话总结：Jepsen ≈ 多过程测试程序 + 线性一致性验证

多过程测试程序是为了生成零碎在各种状况下的操作记录，线性一致性验证则是对操作记录的查看。Jepsen是黑盒测试，通过在一个节点上起多个Client线程，看待测试零碎发送各种申请，而后收集申请后果，以此构建各个申请操作的记录。咱们个别对系统都会有相似测试，相比而言，Jepsen减少了把操作记录组织为History供后继剖析这一部分。

线性一致性验证是Jepsen同Failover测试最大的差别。Jepsen中尽管能够进行其余非线性一致性的验证，但这些测试绝对线性一致性的验证会比较简单直观，所以这里次要具体论述线性一致性验证，其中相干的两个关键问题：
什么是线性一致性

各种不同零碎的验证如何对立为线性一致性的验证。

1 线性一致性

之前提到的文章曾经对线性一致性提供很详尽的论文材料和直观阐明，大家能够钻研一下。文章里给出了程序一致性和线性一致性直观的例子：


图2 程序一致性与线性一致性

程序一致性和线性一致性最本质区别，在于不同Client间的操作，有没有一个确定的happen-before关系。

因为Jepsen中的Client都在同一个节点上，所以能够用零碎工夫(不会回退)记录一个申请从Client收回到Client收到响应的工夫点(对应图中一个矩形的最右边和最左边)，因而能晓得两个操作之间是不是间接有happen-before关系。如果一个操作的完结工夫在另一个操作开始工夫之前，则两个操作有确定happen-before关系；如果两个操作的矩形在时间轴上有重叠，则它们的happen-before关系则并行的，程序不确定，在线性一致性零碎中能够任意调整先后顺序。

如图2中的Get2收到响应的工夫显著是在Set2发出请求之前的，曾经有了确定的happen-before关系，却可能Get到在本人之前Set的数据，所以违反线性一致性。Set3 和 Get2操作是并行的，但无论其先后顺序如何，均不能排列出满足线性一致性的序列了。

而左图的程序一致性则不同，因为P1 P2可能是不同节点的Client，其操作在时间轴上并没有一个雷同的参考，故只能保障同一Client上的操作有严格happen-before关系即可，因而是能够通过排列失去一个满足程序一致性的序列的。

2 线性一致性与Jepsen验证

Jepsen中用Model来验证线性一致性，Model就是一个状态机，而Jepsen测试产生的History是一条条输出的Log。Log之间会有happen-before关系，也会有并行关系，Checker所要做到，便是找到一个正确的Log程序，能够在不违反happen-before的束缚下，让状态机在每个工夫利用Log后放弃行为正确，而一旦违反，则找到了零碎不合乎线性一致性的证据。

Jepsen内置了register/cas-register/multi-register/set/unordered-queue/fifo-queue这些Model。

比方咱们想测试本人实现的分布式锁，咱们有Lock和Unlock两种操作，便能够间接套用cas-register(这里用作阐明，理论应用的是mutex)，每次抢锁胜利将register 0置1，开释胜利将register 1置0，那么在满足happen-before的状况下，一旦呈现无论如何排列Log，都无奈失去一个正确的状态机输入(如下图右边)的状况，就阐明实现的分布式锁不满足线性一致性。


图3 History合乎线性一致性的例子

咱们假如上述P1 P2的操作都返回胜利，则对于左图中可能的程序，咱们将其输出Model:

而对于右图则因为P2 Lock操作与P1的Unlock操作是并行的，所以History能够有Seq3这一排序。

对于想要测试的其余零碎和性能也是如此，在满足线性一致性的条件下，History会有各种可能的Log排列。若History在任何程序下输出Model，都因为不能满足Model本身的束缚，则能够反证零碎不满足线性一致性。理论在Jepsen的线性一致性求解用的knossos，不会这样全副排列遍历的，具体用的可线性化验证算法——WGL，可参考《线性一致性实践》。

二 构造——拆开Jepsen来应用

  • 构建一个分布式系统环境
  • 对分布式系统进行一系列操作
  • 收集操作的历史记录，验证操作后果是合乎预期的

依据须要能够可视化，生成反映零碎性能和可用性的图，以便直观形容零碎对于注入谬误有哪些响应。

引文中Jepsen测试的这3个步骤，别离对应Jepsen构造中的DB、Generator、Checker模块。有了1.1咱们对Jepsen实质的意识，理论实际过程中可能还有所困惑，像是应不应该应用Jepsen、如何应用Jepsen等问题，则要从Jepsen的构造说起。依照之前的定义Jepsen = 多过程测试程序 + 线性一致性验证，咱们能够依据须要将Jepsen拆解开来应用。咱们能够

  • 全副应用用Jepsen来编写测试用例
  • 也能够用本人的测试框架，生成相似Jepsen格局的History，最初代入到Jepsen验证器或本人的验证器中。


图4. Jepsen模块示意

像TIDB的chaos，用Go从新实现了Jepsen性能的测试框架，应用了porcupine这个Go和线性一致性验证器，也能实现和Jepsen一样的测试成果。对于实际而言，这两种计划都能够实现咱们的性能，而在技术选型时，则还须要思考以下几点:


表1. Jepsen测试实际上的抉择

从实际的角度来看，咱们一方面关怀验证有效性，一方面在意编写测试的难度。

测试有效性次要靠框架丰盛的测试性能保障的，而编写难度间接影响着我的项目效率和规模化。间接应用开源框架Jepsen，则是看重它已有性能齐备，认可度高。搭建新框架，则测试上手简略、编写case易规模化，同时依据语言个性能够更适宜某些测试场景(如解决OOM、间接复用已有测试框架的代码)。

所以当咱们只须要测试零碎线性一致性等Jepsen已提供的验证model(包含register/cas-register/multi-register/mutex/set/unordered-queue/fifo-queue等)时，为了简便起见，能够间接套用Jepsen中的model，通过将本身零碎提供的接口封装为和已有验证model的操作等价的语义，便能够间接使用Jepsen进行验证。比拟适宜零碎性能与已有Jepsen测试相符的状况，此时能够迅速测试零碎的各项性能。

如果咱们有很多想要新定义测试的场景，或者曾经积攒了功能丰富的测试框架，或者心愿有一个团队都能很好很快上手的工具，则搭建新框架是更有效率的抉择。相比于给所有人遍及Clojure或者给出一个易用的模板，还是让大家用老锤子砸新钉子更加棘手。

三 作用——女娲应用Jepsen的例子

从实质和构造剖析下来，咱们不难看出，Jepsen不限于测试并验证一致性，但其最大特点就是线性一致性。所以所有须要有线性一致性保障的零碎，都能够应用Jepsen的这种线性一致性验证能力。无论是依靠一致性协定的分布式锁、分布式队列，还是像MySQL这种主从复制的数据库。

咱们如果间接应用Jepsen来进行自定义测试的话，有两局部工作。

1）包装接口

2) 自定义Model和Checker

因为零碎的接口都是固定的，在Jepsen中包装进去即可。包装接口时，次要留神让接口可能疾速收到响应，缩小操作的耗时，因为一旦耗时工夫过长，会导致大量本有确定happen-before关系的操作变成并行，极大减轻了不必要的计算，也容易产生OOM问题。比方restful接口应用curl和应用Clojure的http库两种形式调用，验证的效率截然不同。

最大的工作量是在Model和Checker处做革新，来适配咱们零碎特有的状态机。上面我来介绍一下女娲的restful分布式锁的互斥性和可用性验证，大家能够参考etcd的restful锁接口了解。锁的互斥性验证，在Jepsen中已有实现的例子，比方etcd的分布式锁测试，只须要咱们依照女娲的接口调用做出相似实现acqure和release即可。而如果想测试锁的可用性，比方进行心跳后是否在timeout工夫内肯定有其余client能够抢到锁这种逻辑，则须要咱们对Model局部和Checker局部进行相应的革新。

1 封装接口

实现的操作如下，每一个操作中包含的接口和函数会被顺次调用：


表2. restful锁测试接口封装

咱们将这对四个操作的解决封装进Client——LinearizableLockClient, 在Client外面退出解决每个操作返回值，依据胜利、失败、超时三种状况，生成History中各个操作Response的Log，这样封装接口的操作便实现了。后继运行时，Jepsen会依照既定规定(比方随机、定时···)对各个操作进行调用。如果只调用aquire release，Checker应用默认mutex的checker，能够验证互斥性，全副都调用时应用自定义Checker来验证可用性。

2 自定义Model和Checker

咱们验证锁，Model局部依然应用的是Jepsen提供的mutex。事实上Jepesen中涵盖的model根本已涵盖大部分场景，见knossos的model.clj,这里摘取咱们验证锁用到的mutex:

(defrecord Mutex [locked?]  Model  (step [r op]    (condp = (:f op)      :acquire (if locked?                  "ERROR:已加锁仍能够抢到"                 (inconsistent "already held")                  (Mutex. true))      :release (if locked?                 (Mutex. false)                  "ERROR:未持有锁却能够开释"                 (inconsistent "not held"))))    Object  (toString [this] (if locked? "locked" "free")))"初始化时锁为开释状态"(defn mutex  "A single mutex responding to :acquire and :release messages"  []  (Mutex. false))

能够看到Mutex继承了Model，会依据每一个op更新本身状态，即失常的加锁和开释，当已加锁仍能够抢到或者未持有锁却能够开释，则阐明有不统一，Model执行出错。

Checker局部则是验证锁可用性的要害，咱们想验证的是当lease过期之前，即touch-lease的间隔时间内，锁不会被抢到，在timeout工夫——lease-ttl后则能够被抢到。于是咱们依据已有的History，虚构出一个Client，它的开始工夫会在一个release-lease操作的lease-ttl工夫后，进行一个release操作，如果过程中锁又被抢到或者被另一个Client本人开释，则在History中勾销这个虚构Client的操作。由此咱们能够持续应用线性一致性Checker对Mutex Model的验证，来证实锁的可用性——在锁心跳过期之前不会被其余Client抢到，锁lease-ttl完结之后能够被抢到。因为咱们锁的开释工夫是一个动静范畴，所以将Release的起始和完结工夫距离加上这个动静范畴，理论的转换成果如下图。


图5. 锁可用性测试的History转换

由此咱们能够看出，通过对Model和Checker的革新是能够很灵活多样的，咱们失去一个History之后，能够依据业务状态机调整Model执行Log的后果，也能够对History自身进行解决应答一些延长的场景，如果不验证线性一致性而是其余性能(比方最终一致性、watch等)，还能够间接剖析History——最终一致性要求最初操作全副实现后读某个寄存器后果雷同，watch要求各个Client本人watch后果拼接成的序列统一，都是比拟容易实现的操作。

四 总结

最初咱们对如何应用Jepsen做个总结：

绝对TLA+,Jepsen是更容易利用在测试本人的分布式系统中的。咱们在须要验证线性一致性的时候，只须要依据本身业务状态机形象出Model，解决History，就能够间接应用线性一致性验证器进行验证；须要验证其它一致性时，则通过History，能够很简略地写出相应的测试case。

如果心愿理论应用中，在生成History和验证时有本人的须要，能够按构造拆分，只应用Jepsen的一部分或者本人搭建框架。比方应用自有谬误注入框架，本人生成History，给到Jepsen的一致性Checker；或是应用Jepsen生成History，本人写简略的脚本读取后进行剖析；或是间接搭建相似框架，更高效地应答丰盛的性能、场景，疾速编写更易上手、更具备可读性的测试代码。

对于各种分布式系统，Jepsen相对是必要的且易于编写测试验证的，最低老本帮忙咱们发现工程实现中各种各样的问题。

参考文章：

Jepsen测试：https://ata.alibaba-inc.com/a...
当 Messaging 遇上 Jepsen：https://developer.aliyun.com/...
线性一致性实践：https://zhuanlan.zhihu.com/p/...

原文链接
本文为阿里云原创内容，未经容许不得转载。