简介：女娲团队在过来大半年工夫里继续投入女娲 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/…
原文链接
本文为阿里云原创内容，未经容许不得转载。