介绍：Nuwa团队近半年来持续投入Nuwa2.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。1.本质——只看Jepsen的特点在分布式系统测试领域，大家最熟悉的两个工具就是TLA+和Jepsen。这种关系类似于演绎和归纳，白盒和黑盒。TLA+要求编写测试的人能够真正抽象出需要验证的分布式系统，并在每一个细微的逻辑部分实现对真实系统的精细化和准确还原，然后在各个状态空间中遍历这个抽象系统。如果通过验证抽象系统总是满足定义的规则，就可以推断并保证真实系统的正确性，就像拥有一张地图，上面有详细的关键信息，在地图上画出路线图，也可以到达真实世界按照路线结束。Jepsen从系统提供的对外接口入手，通过实际构建系统、执行操作、注入错误、验证结果等一系列错误注入情况下系统行为的演练和分析，真正发现不符合既定规则的情况，通过历史记载的分析找到这些情况，就好像创造了很多零散的拼图，尝试了各种各样的东西，最后验证是否可以拼凑成合理规则的图形。由此我们不难看出两者的难度。TLA+的难点在于推导的正确性。TLA+编写的模型是建立在抽象系统与真实系统关键部分完全一致的前提下。如果与项目实现不匹配，会造成一些在实际系统中可能会遇到的问题。已验证。Jepsen最大的难点在于如何根据收集到的测试用例中的历史记录来断定系统是否存在相应的错误，而归纳本身的特性也决定了Jepsen测试无法覆盖所有的异常情况。在这个归纳过程中，线性一致性是最难归纳验证的，而系统线性一致性的验证也是Jepsen最大的特点。图1Jepsen提供的一致性验证能力一句话总结：Jepsen≈多进程测试程序+线性一致性验证多进程测试程序是生成系统在各种情况下的运行记录，线性一致性验证是对运行进行验证检查记录。Jepsen是一个黑盒测试。通过在一个节点上启动多个Client线程，向待测系统发送各种请求，然后收集请求结果，构建每一次请求操作的记录。我们一般都会对系统进行类似的测试。相比之下，Jepsen将整理操作记录的部分加入到History中，方便后续分析。线性一致性验证是Jepsen和Failover测试最大的区别。虽然在Jepsen中可以进行其他的非线性一致性验证，但是这些测试相对于线性一致性验证来说都比较简单直观，所以这里主要阐述一下线性一致性验证，以及与之相关的两个关键问题：什么是线性一致性，如何统一各种不同系统的验证转化为线性一致性的验证。1LinearConsistency前面提到的那篇文章已经对线性一致性提供了非常详细的纸质资料和直观的解释。你可以研究它。文章给出了一个顺序一致性和线性一致性的直观例子：图2顺序一致性和线性一致性顺序一致性和线性一致性最本质的区别在于是否存在确定的happen-before关系。由于Jepsen中的客户端都在同一个节点上，系统时间（没有fallback）可以用来记录客户端发出请求到客户端收到响应的时间点（对应最左边和图中最右边的一个矩形)，所以可以知道这两个操作之间是否存在直接的happen-before关系。如果一个操作的结束时间早于另一个操作的开始时间，则这两个操作具有一定的happen-before关系；如果两个操作的矩形在时间轴上重叠，那么它们的happen-before关系是平行的，sequential不确定，在线性一致性系统中可以任意调整顺序。如图2所示，Get2收到response的时间明明是在Set2发送请求之前，已经存在一定的happen-before关系，但是它却能先于自己拿到Set的数据，所以违反了线性一致性。Set3和Get2操作是并行的，但是无论顺序如何，都不能安排一个满足线性一致性的顺序。左图中的序列一致性不同。由于P1和P2可能是不同节点的client，它们的操作在时间轴上不具有相同的引用，所以只有在同一个client上的操作才能保证有严格的happen-before关系，因此可以通过排列得到一个满足顺序一致性的序列。2线性一致性和Jepsen验证Jepsen使用Model来验证线性一致性。Model是一个状态机，Jepsen测试生成的History是一个输入日志。日志之间会有happen-before关系，也会有并行关系。Checker需要做的是找到一个正确的日志顺序，这样状态机就可以在不违反happen-before约束的情况下，在每次应用日志。之后，行为仍然是正确的，一旦被违反，我们就会发现系统不符合线性一致性的证据。Jepsen内置了register/cas-register/multi-register/set/unordered-queue/fifo-queue等模型。比如我们要测试我们已经实现的分布式锁，我们有Lock和Unlock两个操作，那么我们可以直接申请cas-register（这里是为了说明，实际用的是mutex），register0是每次抢到锁成功设置为1，释放成功，寄存器1设置为0，那么在满足happen-before的情况下，一次正确的状态机输出（如下图左侧所示）)无论Log怎么排都获取不到，说明分布式锁实现的线性一致性不满足。图3.符合线性一致性的History示例。我们假设上述P1和P2操作都成功返回。然后，对于左图中的可能序列，我们将其输入到Model中：而对于右图，由于P2Lock操作与P1Unlock操作Parallel相同，所以History可以有Seq3这种排序。对于您要测试的其他系统和功能也是如此。在满足线性一致性的情况下，History会有各种可能的Log排列。如果History以任意顺序进入Model，由于不能满足Model本身的约束，可以反证系统不??满足线性一致性。实际上Jepsen的线性一致性方案中使用的knossos是不会这样遍历的。具体可线性化的验证算法——WGL，请参考《线性一致性理论》。2.结构——拆解Jepsen用于搭建分布式系统环境，对分布式系统进行一系列操作，收集操作的历史记录，验证操作结果是否符合预期，按需可视化，以及生成反映系统性能和可用性的图表。为了直观地描述系统如何响应注入错误。引文中Jepsen测试的三个步骤分别对应Jepsen结构中的DB、Generator、Checker模块。以我们在1.1中对Jepsen本质的理解，在实际的实践过程中，我们可能还是一头雾水。对于是否应该使用Jepsen、如何使用Jepsen等问题，就要从Jepsen的结构说起。根据前面的定义Jepsen=多进程测试程序+线性一致性验证，我们可以根据需要拆解Jepsen使用。我们可以使用Jepsen编写测试用例或者使用我们自己的测试框架生成类似Jepsen格式的History，最后代入到Jepsen验证器或者我们自己的验证器中。图4.Jepsen模块显示，和TIDB的混沌一样，Jepsen功能的测试框架用Go重新实现。使用Porcupine这个Go和线性一致性验证器，也可以完成和Jepsen一样的测试效果。对于实践来说，这两种方案都可以完成我们的功能，在选择技术的时候，我们还需要考虑以下几点：表1.Jepsen测试实践的选择从实践的角度来看，一方面，我们关注验证有效性，一方面是编写测试的难度。测试的有效性主要靠框架丰富的测试功能来保证，编写的难易程度直接影响到项目的效率和规模。直接使用开源框架Jepsen，功能齐全，认可度高。构建一个新的框架可以方便测试和扩展案例编写，更适合根据语言特性的某些测试场景（比如解决OOM，直接复用现有测试框架的代码）。所以当我们只需要测试Jepsen提供的验证模型如系统的线性一致性（包括register/cas-register/multi-register/mutex/set/unordered-queue/fifo-queue等）时，对于简单，我们可以直接ApplyingthemodelinJepsen，通过将自己系统提供的接口封装成语义等价于现有验证模型的运行，就可以直接使用Jepsen进行验证。更适合系统功能与现有Jepsen测试一致的情况。此时可以快速测试系统的各项功能。如果我们有很多场景想要定义新的测试，或者我们已经积累了一个功能丰富的测试框架，或者我们希望有一个团队可以快速上手的工具，那么构建一个新的框架是一个更高效的选择.比起给大家普及Clojure或者给个好用的模板，大家用旧锤敲新钉子更容易。三大功能——Nuwa以Jepsen为例，剖析本质和结构。不难看出，Jepsen并不局限于测试和验证一致性，它最大的特点是线性一致性。因此，所有需要线性一致性保证的系统都可以使用Jepsen的线性一致性验证能力。无论是基于共识协议的分布式锁，分布式队列，还是MySQL这样的主从复制数据库。如果我们直接使用Jepsen进行自定义测试，有两个部分的工作。1）封装接口2）CustomModel和Checker由于系统的接口是固定的，所以可以在Jepsen中进行封装。在对接口进行封装时，主要注意让接口快速收到响应，减少耗时操作，因为一旦耗时时间过长，会造成大量带有一定happen-before的操作关系变成平行，大大增加了不必要的计算，也容易出现OOM问题。比如restful接口使用curl和Clojure的http库调用，验证效率完全不同。最大的工作量是修改Model和Checker来适配我们系统特有的状态机。下面介绍一下女娲restful分布式锁的互斥和可用性验证。可以参考etcd的restfullock接口了解。Jepsen中已经实现了锁的互斥校验，比如etcd的分布式锁测试。我们只需要根据女娲的接口调用，做acquire和release的类似实现即可。而如果要测试锁的可用性，比如其他客户端是否必须在停止心跳后的超时时间内能够抢到锁，我们需要相应修改Model部分和Checker部分。1封装接口实现的操作如下，每个操作包含的接口和函数会依次调用：表2.Restful锁测试接口封装我们将这四个操作的处理封装到Client—LinearizableLockClient中，以及将每个操作的返回值添加到ClientProcess中，并根据成功、失败、超时三种情况在History中生成每个操作Response的Log，这样封装接口的操作就完成了。在后续的操作过程中，Jepsen会按照既定的规则（比如随机、定时……）调用每一个操作。如果只调用aquirerelease，Checker使用默认mutex的检查器，可以校验互斥，全部调用时使用自定义的Checker校验可用性。2CustomModelandChecker我们对锁进行校验，Model部分仍然使用Jepsen提供的mutex。事实上，Jepesen涵盖的模型已经基本涵盖了大部分场景。请参见knossos的model.clj。这里我们提取我们用来验证锁的互斥量：(defrecordMutex[locked?]Model(step[rop](condp=(:fop):acquire(iflocked?"ERROR:alreadylockedstillbegrabt"(不一致的“已经持有”)(Mutex.true)):release(iflocked?(Mutex.false)"ERROR:notheldThereisalockbutitcanberelease"(inconsistent"notheld"))))Object(toString[this](iflocked?"locked""free")))"锁在初始化时释放"(defnmutex"响应:acquire和:release消息的单个互斥量"[](Mutex.false))可以看到Mutex继承了Model，会根据每个op更新自己的状态，也就是正常的加锁和释放，加锁的时候还是可以抢到的。或者没有持有锁就可以释放，说明存在不一致，Model执行错误。Checker部分是验证锁可用性的关键。我们要验证的是，在租约到期之前，也就是在touch-leaseinterval内，锁不会被抢，超时时间lease-ttl后可以抢。所以我们根据已有的History虚拟出一个Client，它的开始时间会是一个release-lease操作的release-ttl时间之后的一个release操作。释放，取消History中这个虚拟Client的操作。因此，我们可以继续使用LinearConsistencyChecker来验证MutexModel来证明锁的可用性——在锁心跳到期前不会被其他客户端抢到，lease-ttl结束后才能抢到锁.由于我们锁的释放时间是一个动态范围，将Release的起止时间间隔加入到这个动态范围内，实际转换效果如下图所示。图5.锁可用性测试的历史转换由此可见，Model和Checker的转换可以非常灵活多样。我们得到一个History之后，可以根据业务状态机调整Model执行Log的结果，也可以ProcessHistory本身来应对一些扩展场景。如果不验证线性一致性而是其他函数（如最终一致性、watch等），也可以直接分析History——最终一致性需要读取某个寄存器的结果相同，而watch需要的是拼接各个客户端的watch结果的顺序是一致的，是一个比较容易实现的操作。四、总结最后，我们对Jepsen的使用做一个总结：与TLA+相比，Jepsen更容易应用于测试自己的分布式系统。当我们需要验证线性一致性时，只需要根据自己的业务状态机和流程History抽象出Model，就可以直接使用线性一致性验证器进行验证；当我们需要验证其他一致性时，可以使用History，可以很简单的写出相应的测试用例。如果在实际使用中想在生成History和校验时有自己的需求，可以按照结构拆分，只使用Jepsen的一部分或者自己搭建框架。比如使用自己的错误注入框架，自己生成History，交给Jepsen的一致性检查器；或者使用Jepsen生成History，写个简单的脚本，看完再分析；或者直接构建一个类似的框架来更高效地处理丰富性。功能和场景，快速编写更易用、更易读的测试代码。对于各种分布式系统，Jepsen是绝对必要的，而且易于编写和测试验证。以最低的成本帮助我们发现工程实施中的各种问题。参考文章：Jepsen测试：https://ata.alibaba-inc.com/a...当Messaging遇上Jepsen：https://developer.aliyun.com/...线性一致性理论：https://zhuanlan。zhihu.com/p/...原文链接本文为阿里云原创内容，未经允许不得转载。
