这里介绍数据库相关的测试，包括了基准、分布式、混沌工程等。

简介 #

包含了质量相关的技巧、能力，因为在测试过程中同时需要依赖监控之类的能力，所以将监控系统也附带上了。

分布式 #

相对单机来说，分布式系统的正确性要更难保证，需要考虑各种异常场景，例如网络延迟、报文重复、乱序、丢失、主机异常等等，同样也导致异常检测非常麻烦。

当前最常见的有 TLA+ 和 Jepsen 两个工具，类似于白盒和黑盒的区别：

• TLA+ 形式化建模语言，以数学形式精确描述系统的状态变迁和行为，借助 TLC 检查器可以发现潜在错误。
• Jepsen

TLA+ #

Temporal Logical of Actions, TLA+ 是 2013 年图灵奖获得者 Lamport 提出，用于程序的设计、建模、验证等，特别是并发和分布式系统，在 TLA+ 有很多不错的仓库，含 示例 和 可视化 等。

使用时需要先定义标准，然后通过 TLC 工具进行检查，检查过程中会遍历所有可能的行为，并检查是否有违反标准的异常场景出现。另外，为了简化定义，同时还提供了 PlusCal 的实现，不过如下还是以 TLA+ 作为示例。

基础示例 #

可以从 ToolBox 下载工具，通过 File->Open Sepc->Add New Spec... 添加模块，注意，文件名和模块名应该保持一致；运行通过 TLC Model Checker->New Model... 打开，有对应的运行按钮。

每个模块通过 ---- MODULE Simple ---- 开始，以 =========== 结束，如下是一个简单的硬币组合策略。

------------------------------- MODULE Money -------------------------------
EXTENDS Integers

CONSTANT MONEYS, TOTAL
VARIABLES money

Init == money = 0
Add(i) == /\ money + i <= TOTAL
          /\ money'= money + i
Terminating == /\ \A i \in MONEYS: money + i > TOTAL
               /\ UNCHANGED<<money>>
Next == \/ \E i \in MONEYS: Add(i)
        \/ Terminating
Invariant == money <= TOTAL

=============================================================================

标准定义 #

其中的每个变量或者常量都是一个集合而非单个值，而且 TLA+ 是通过文本进行描述的，很多特殊的符号需要进行转义：

• 逻辑运算，/\ 表示与、\/ 表示或。

一些常用的表达方式。

----- Record 类似于 C++ 中的结构体
p = [name |-> "Andy", age |-> 42]  # 指定结构体成员变量初始值
p' = [p EXCEPT ![age] = 20]        # 返回 p 但是会将 age 成员变量修改为 20

Jepsen #

该检查器内置 Elle 用来检查事务一致性，通过 Knossos 检查分布式线性一致性，在 JepsenIO 仓库中有很多相关的示例。

其中分布式线性一致性需要使用顺序规范和并发操作历史来判断是否满足要求，不过这一验证是 NP 问题，详见 Testing Distributed Systems 中的介绍，作者推荐使用 Procupine，相比来说效率要更高。

其核心包括了三种测试场景：

• Bank 不停的进行转账，最后统一计算总金额，需要确保总金额不变；
• Set 数据写入到表中，确保所有返回成功的数据存在；
• Register 在表中插入一条数据，不停对该记录执行 Read Write CAS 等操作。

参考 #

• TLA+ 官方的文档，以及相关的 查询手册 。
• Jepsen 官方提供的 Tutorial 教程，包括 中文翻译 文档；其中 ETCD 相关可以参考 etcd.io 和 jepsen-etcd。
• ETCD Robustness Testing 关于 ETCD 的质量体系建设，有很多不错的策略可供参考。