Jepsen 的使用与线性一致性
背景
对于分布式系统的测试是整个系统开发过程中重要的部分，我们需要对系统进行完整的正确性测试才能确保系统符合我们的设计。Jepsen是Kyle Kingsbury使用Clojure编写的分布式系统测试框架，Jepsen通过并发运行一组Client对系统进行操作，再利用验证模块knossos对操作的History进行正确性的验证。Jepsen也会生成关于性能和可用性的图表，帮助使用者确认系统响应不通的注入错误时的状态。这里的正确性定义为线性一致性，即分布式领域著名的CAP定理中的C。
Jepsen的架构
Jepsen测试系统由一个Control node和多个DB node组成。Jepsne需要使用者将待测DB系统的启动部署和Client的连接和DB操作等模块预先编写至测试脚本中。
Jepsen的测试脚本:
Operation
Operation指Client对待测DB系统的操作调用，常用的包括
read,write和compare-and-setClient
Client模块由使用者编写，每个Client封装了
setup!，invoke!和close!函数，setup!是连接DB的函数，invoke！是对DB的Operation调用，close!是关闭连接DB
DB模块封装了待测系统的部署，启动，关闭接口，由Jepsen的os模块预先优化配置环境，通过调用DB模块中的
setup!一键启动。(我们提交了对Jepsen支持Centos的PR，目前已被作者合进最新版0.1.9使用)
Jepsen测试框架的核心模块:
generator
嵌入至Client模块，生成一系列的随机操作。
nemesis
Jepsen的核心模块，与generator搭配，对DB node引入一系列的错误故障，包括网络分区，丢包，延迟，DB系统的宕机和节点时钟修改。
checker
由作者编写的另一个库knossos来验证整个Operation的History是否符合线性一致性。
下面是三个核心模块混合搭配使用的例子:
1 | (defn create-partition-node-test |
分布式系统的正确性测试
对于分布式系统来说，正确性是最重要的特性，而正确性是很难证明的，尤其是分布式系统的正确性。所以我们对于分布式系统的测试往往从形式化验证和软件工程的测试方法:
形式化验证
对于分布式系统的算法模型，需要进行形式化验证，利用数学语言证明算法满足正确性。目前比较常用的是TLA+，TLA+是图灵奖得主Leslie Lamport发明的专门用来描述并验证复杂系统行为的形式化方法，使用TLA+可以帮助我们在设计时，基于系统层面的抽象对系统的正确性做形式化、规范的描述，并且定义出设计的正确性属性，自动化地加以验证，以正确性为驱动进行系统建模和设计。
工业化测试
而在实际的生产环境里，多节点，交互复杂的分布式系统中，节点异常，网络异常，配置变更等场景不常发生但不可避免。为了应对这些可能出现的场景，我们对系统的测试必须尽可能提高这些事件发生的概率，比如Leadership changes, Partial network outage，从而测试整个系统的正确性。所以常见的做法如下：
- 让系统的某些参数设置的不合理, 但是不违反正确性, 这样可以让那些极端的场景下的问题暴露出来。比如Election timeout 设置成非常低, Heartbeat 的间隔非常高 这样就导致更频繁的Leader Changes. 更频繁的快照等等这些操作.
- 让运行的环境出现频繁的外部环境变化, 比如频繁进程随意启停, 网络丢包, 断网, 频繁Membership change 等等
- 长时间的压力测试运行，引入稳定性压力测试和极限负载情况下导致系统崩溃的破坏性压力测试。
而在错误注入这个方向，Jepsen是一个很强有力的工具。
正确性
既然要测试一个系统的正确性，我们先来定义什么是正确性。这里的正确性就定义为Linearizability Consistency，即CAP定理中的C。
Linearizability Consistency是Maurice P. Herlihy与Jeannette M. Wing在1987年共同提出的关于并行对象行为正确性的一个条件模型，两人在1990年发表了关于Linearizability的论文。在论文中讨论了关于Linearizability的定义和形式化证明, 其中对线性一致性的系统的正确性，作者给出了两点要求:
- each operation should appear to “take effect” instantaneously
- the order of nonconcurrent operations should be preserved.
即每一个操作都会立即生效，非并行的情况下的Operation结果会对下一个Operation产生影响。
在论文中引入了一个FIFO(first in, first out)的队列操作来讲述这个观点:
上图中的Enq代表入列，Deq代表出列，x，y，z,均为操作的值，A，B为操作的进程. 即E(x) A ,D(x) B分别代表A进程将x值入列，B进程将x值出列。一个时间轴代表操作的invoke和resp的返回时间片，在一个线性一致性的系统里面，任何操作都可能在调用或者返回之间原子和瞬间执行。通过标明线性一致性的点，我们可以得出结论上图是符合线性一致性的。
这个例子是很明显不符合线性一致性的，即D(y) A是非法的操作，因为根据FIFO队列的原理，x在y之前入列，但y却在x还没有被出列之前被dequeue。
Locality(局部性)
如果每一个独立的对象是线性线性一致性的，那么这个系统也是符合线性一致性的。即将各个独立的对象的线性历史组合起来也是符合线性一致性的。
Nonblocking(非阻塞性)
整个操作过程中不会被阻塞,即任意一个Operation无需等待其他的Operation的完成。
为什么一个分布式系统需要具备线性一致性? Linearizability站在Client的角度上来说，假如一个系统是符合线性一致性的，那么多个Client在指定的一个时间点所读到value是一致的，这就符合了CAP理论中的C。
在利用Jepsen测试我们的系统的过程中，我们对分布式系统的测试有了更全面的认识和实际的测试经验，关于Jepsen的使用我们也有以下几点经验之谈:
- 丰富的故障类型引入，方便使用者全面的测试系统。在实际的生成环境中，网络分区，时钟同步，节点失效都是很容易发生的故障，Jepsen测试分布式系统在这些故障模型下的行为。
- 黑盒测试，不需要接触系统的源码。
- 假如配置的参数
time-limit过长容易造成Jepsen的分析过程发生OOM的情况。 - Clojure的使用门槛过高，函数式编程让自定义协议的系统无法引用现成的测试用例，必须重新编写测试脚本。
- Jepsen对系统的并发压力有限，所以这里仅仅验证了系统的算法正确性。
在完全通过一致性测试框架Jepsen后，我们后续也将从引入形式化验证即TLA+验证算法的正确性。
分布式系统测试的思考
关于分布式系统测试是一件复杂的事情，在测试分布式系统的正确性时，使用错误注入是一个很必须的手段。在工程验证方面已经有Jepsen等框架，而形式化证明也能够保证一个分布式系统的正确性，比如Raft目前已经有了用TLA+编写的形式化证明。
虽然我们这里使用Jepsen框架完成系统的正确性测试，但系统的测试内容不仅仅限于正确性，即使协议算法被证明是正确的，也仍然很难在实现中避免Bug。而其他的测试内容，包括系统的性能测试和可靠性测试，因为分布式系统中的并发情况造成的不确定性，使系统的问题往往在高并发的压测环境下才有可能触发。所以对于系统的其他方面测试，我们还需要对系统引入上述所说的多种故障类型的同时，提高对整个系统的并发压力，才有可能在一些极端情况下发现系统的问题。最后对于分布式系统的测试，我们还需要完整的覆盖率测试，通过实际的业务场景对整个系统进行白盒测试，从而提高系统的代码质量和鲁棒性。