作者 | 僧泉
来源 | 阿里技术公众号
女娲团队在过去大半年时间里持续投入女娲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绝对是必要的且易于编写测试验证的，最低成本帮助我们发现工程实现中各种各样的问题。
参考文章：
- 当 Messaging 遇上 Jepsen：https://developer.aliyun.com/article/727886
- 线性一致性理论：https://zhuanlan.zhihu.com/p/338057286
EMR Studio 大数据处理最佳实践课程
EMR Studio 是 阿里云 E-MapReduce 最新推出的用于开源大数据开发场景的集群类型，提供交互式开发、作业提交、作业调试和工作流一站式数据开发体验。能够无缝对接 EMR 计算集群，自动适配多种计算引擎协同工作。覆盖了大数据处理ETL、交互式数据分析、机器学习和实时计算等多种应用场景。
本系列课程旨在让你对EMR Studio 有初步的了解，同时通过一些落地的最佳实践，助你摆脱技术小白称号！
