怎样证明系统在故障中仍然正确：故障注入与 Jepsen

一个分布式 KV 在网络分区中持续运行十分钟，测试结束后五个副本的最终值完全相同。这个结果不能证明过程中没有读到旧值，也不能证明两个客户端没有分别成功写入互相冲突的数据。故障恢复可能覆盖中间错误，最终状态会把已经发生的违约藏起来。

验证分布式正确性需要三样东西：系统对外承诺的模型、并发操作的完整历史、能够判断该历史是否属于模型的 checker。故障注入负责扩大有问题的执行路径出现概率，Jepsen 把部署、负载、故障、历史记录和检查组织成一次可重复实验。

本文回答的问题是：怎样把“系统应该正确”变成可执行的不变量，在进程崩溃、网络分区、时钟跳变和结果未知中采集证据，再判断一次并发历史是否违背线性一致性或事务隔离承诺？ Jepsen 可以找到反例，却不能从有限测试证明所有可能执行都正确。这里的“证明”指对一份观测历史给出可复核结论，并通过系统化探索不断提高发现反例的能力。

一、先写承诺，再设计故障

测试前要明确对象和模型。对单寄存器 KV，可以承诺 linearizable read/write/CAS；对任务队列，可以承诺任务不丢、同一任务最多一个有效 owner，业务效果允许幂等重试；对事务数据库，可以承诺 serializable、snapshot isolation 或 read committed。不同模型允许的历史不同。

Jepsen 的一致性模型页面把模型定义为一组合法历史。线性一致性要求每个操作看起来在调用与返回之间某个瞬间原子生效，并尊重真实时间顺序；顺序一致性保留每个进程内顺序，不要求跨进程的真实时间；串行化关注事务能否排列成某个串行顺序，strict serializability 还加入真实时间约束。

“最终一致”不足以作为多数测试的唯一不变量。只要停止写入后最终收敛，大量丢更新、读旧值和短期双主都可能被允许。系统应该列出更具体的业务约束，例如余额不为负、已确认订单不会消失、唯一用户名不能属于两人、单调版本不会倒退。

Safety 与 Liveness 分开验证

Safety 表示坏事从未发生，例如两个节点没有在同一日志位置提交不同命令；Liveness 表示好事最终发生，例如分区恢复后请求重新成功。一次运行没有发现 safety 反例，只能说明当前历史合法；可用性则可以用成功率、延迟和恢复时间统计。

系统在少数派分区中拒绝所有写，可能保持线性一致却可用性很差。一个 checker 报 valid? true 不能代替 SLO。Jepsen 通常同时输出正确性检查和性能图，评审时应分别解读。

二、历史是验证的核心证据

Jepsen 将一次逻辑操作记录为 invoke 与 completion。completion 有三种重要结果：

:ok 表示操作确定成功，必须出现在逻辑历史中；
:fail 表示操作确定没有生效，不能出现在逻辑历史中；
:info 表示结果未知，checker 必须考虑它可能生效，也可能没有生效。

Jepsen History给出的结构还包括逻辑进程、函数、值、时间和索引：

{:type :invoke, :process 3, :f :write, :value 1, :time 102000}
{:type :info,   :process 3, :f :write, :value 1, :time 403000}
{:type :invoke, :process 7, :f :read,  :value nil, :time 410000}
{:type :ok,     :process 7, :f :read,  :value 1,   :time 430000}

写 1 超时后记为 :info。后续读到 1 时，checker 可以选择把未知写解释为已经生效。若客户端错误地把超时记成 :fail，checker 会认为读到了凭空出现的值；若所有异常都记成 :info，checker 的搜索空间扩大，还可能掩盖本可确定的失败。Client 适配层必须理解数据库错误码和请求阶段。

时间戳用于建立操作的调用与完成区间，不要求不同机器时钟完全同步，因为 Jepsen 控制进程记录客户端历史。真实生产 trace 若由各节点本地时钟记录，需要先处理时钟偏差，否则错误的真实时间边会制造或掩盖线性一致性结论。

三、Jepsen 测试由五个部件组成

Jepsen 测试在控制节点运行，通过 SSH 或其他控制方式管理数据库节点。官方仓库的设计说明将测试拆成 OS、DB、Client、Generator、Nemesis 和 Checker；其中 OS/DB 负责环境，后四个构成操作与验证闭环。

Jepsen 从负载与故障生成到历史检查的闭环

Client 把抽象操作映射为真实 API，并把异常分类为 ok、fail 或 info。Generator 决定并发进程在何时执行什么操作。Nemesis 是特殊进程，注入网络、进程、时钟或存储故障。Checker 在运行结束后读取 history，判断模型、业务不变量和可用性指标。

环境安装也属于测试。版本、配置、复制因子、持久化模式和客户端一致性选项必须进入测试结果。若本来要验证线性一致读，却误用了数据库明确标注的 stale read API，测试失败说明配置不满足目标，不一定是产品 bug。

四、Workload 要让错误可观察

高 QPS 随机读写不一定是好 workload。测试操作要让隐藏状态通过返回值暴露，并形成 checker 可以推理的关系。

Register 检查单键线性一致性

CAS register 支持 read、write 和 compare-and-set。CAS 对并发顺序约束强，适合验证协调存储和元数据服务。状态模型很小，Knossos 可以搜索是否存在一条合法线性化顺序。

只测一个 key 会集中竞争，容易触发日志与选主边界；按多个独立 key 分组可以提高吞吐并分别检查。若系统承诺跨 key 事务原子性，把每个 key 单独检查会漏掉跨对象异常。

Set 检查丢失与凭空出现

客户端向集合添加唯一元素，最后读取全集。成功 add 的元素必须存在，明确失败的元素不能出现，info 元素可出现或不出现。这个 workload 易扩展到大量操作，适合发现 acknowledged write 丢失，但对操作顺序和陈旧读的约束较弱。

Bank 检查业务不变量

多个账户初始总额固定，事务在账户间转账，任意一致快照中总额应保持不变且余额不能违反规则。它能发现部分提交和隔离异常。若读取所有账户不是一个原子快照，测试自身会把合法并发误报为总额变化，因此 Client 必须使用待验证的事务 API。

List-append 为 Elle 提供依赖证据

每个事务读取若干 key，并向列表追加全局唯一值。读结果暴露“事务看见了哪些先前写入”，checker 可以推导 write-read、write-write 和 read-write 依赖。Elle通过事务图中的环检测 G0、G1、G-single、G2 等异常，适合检查 read committed、snapshot isolation、serializable 和 strict serializable 等模型。

Workload 的数据模型要避开系统的未承诺区域。用自增 ID 测线性一致性却经由异步只读副本查询，得到的是错误接口的预期行为。测试报告应写明调用端点、读写选项和模型来源。

五、Generator 控制并发形状

Generator 产生各逻辑进程的操作。并发度太低，所有操作几乎串行，很多竞争窗口不会出现；并发度过高，大量请求只在客户端连接池排队，真正到达系统的交错反而单一。应根据节点数、连接数和操作延迟逐步选择并发度。

操作分布也有影响。纯写入容易验证丢失，却无法观察读路径；读写各半可能缺少 CAS 冲突；事务键完全随机会降低竞争，所有事务都打一个 key 又只覆盖热点路径。可以把稳定随机、热点、分区键和长事务组合成多个独立测试，而不是用一个混合比例代替全部场景。

故障恢复后要保留一段 heal phase。Nemesis 停止故障，Generator 继续少量操作并做最终读取，用于观察系统能否恢复活性、复制是否收敛以及积压操作的结果。立即结束测试会漏掉恢复阶段 bug。

六、Nemesis 应命中协议窗口

Jepsen 把故障注入者称为 Nemesis。它不绑定普通客户端节点，可以按 Generator 的时间表开始和停止故障。Jepsen 教程展示了随机二分网络分区与线性一致性检查的组合。

网络分区要有拓扑

随机断开一条连接未必影响 quorum。应根据协议设计多数派与少数派、Leader 单独隔离、环形不对称分区、跨机房断链和客户端到节点的局部中断。iptables 规则要验证实际生效方向，TCP 已建立连接也要被覆盖。

进程故障不止 kill

kill -9 测崩溃恢复；SIGSTOP 暂停进程但保留连接和内存，能模拟长 GC 或调度停顿，恢复后尤其容易暴露旧 Leader、过期租约和 fencing 问题；滚动重启测试版本和状态迁移；同时停止多数节点验证少数派是否拒绝提交。

时钟与存储故障要服从系统假设

依赖租约、TTL 或 last-write-wins 的系统需要时钟跳变、漂移和暂停测试。Raft 的安全核心不依赖物理时钟准确，但超时会影响选举活性。存储故障可以包括磁盘满、fsync 失败、延迟、进程在写入窗口崩溃和未同步数据丢失；直接随机改数据文件是在测试校验与修复能力，和测试共识协议的故障模型不同。

多种故障同时发生更接近事故，也更难定位。测试套件通常先让单一 nemesis 建立归因，再组合进程、网络和时钟故障。每次注入都要写入 history，报告才能把异常操作与故障时间窗口对齐。

七、Knossos 怎样检查线性一致性

线性一致历史必须满足两类顺序：每个操作在 invoke 与 completion 之间某个点生效；若操作 A 完成后 B 才开始，A 必须排在 B 前面。并发重叠的操作可以按任一符合状态机的顺序排列。

Knossos 接收历史和一个顺序状态机模型，例如 CAS register。它尝试从当前状态选择一个可线性化的已完成操作，应用到模型并继续搜索。若所有分支都无法解释某个成功返回值，历史无合法线性化。

并发历史怎样转成真实时间约束与候选线性化顺序

图中写 1 与写 2 重叠，因此二者顺序可选；读操作在写 2 完成后才开始，必须排在写 2 后。若读返回 1，而写 2 确定成功，且没有其他写可以解释，就形成反例。真实 checker 还要处理 info 操作的可能生效分支。

线性化搜索最坏复杂度很高，并发越多、未知操作越多，候选分支越大。可以缩短每段历史、按独立 key 分区检查、提高错误分类精度，并保留触发失败的最小历史。checker 超时或 OOM 不是 valid? true，应作为无法判定报告。

八、Elle 怎样检查事务异常

事务历史的合法顺序比单寄存器复杂。Elle 不枚举所有串行顺序，而是从唯一追加值和读取结果推导事务依赖图。节点是事务，边表示一个事务必须在另一个之前，例如 B 读到了 A 追加的值，得到 A 到 B 的 write-read 边。

如果依赖关系形成特定环，就可以证明对应隔离模型被破坏。两个事务分别读取对方旧值，再写不同 key，可能形成 read-write 反依赖环，这是 write skew 一类异常的基础。Elle README 列出了它可检测的 Adya 异常，并明确说明 checker 并不完备：未观测事务和为保持近线性性能而限制的推理，会让某些真实异常无法被识别。

这条限制很重要。valid? true 表示“在当前 workload 暴露的信息和 checker 推理范围内没有找到违约”，不是数据库已经被数学证明满足某模型。提高覆盖需要改变事务模板、键分布和故障，而不是把同一个测试多跑几小时。

九、一次 Raft KV 测试怎样设计

目标系统是五节点 Raft KV，对外宣称默认 read、write 和 CAS 线性一致。测试使用一个控制节点和五个数据库节点，客户端只通过公开 API 访问。

DB 组件安装固定版本，清理旧数据，写入明确的 fsync、选举超时和快照配置，再启动五节点集群。
Client 为每个逻辑进程建立连接。连接拒绝且请求确定未发送记 :fail；发送后超时记 :info；服务端明确返回 CAS 比较失败是正常 :ok 结果的一种。
Generator 混合 read、write、CAS，使用高竞争单 key 与多 key 两组测试，并控制 20 个并发进程。
Nemesis 每隔一段时间随机选择 Leader 隔离、多数/少数分区、SIGSTOP Leader、kill 并重启节点；每次恢复后留出稳定窗口。
Checker 用 CAS register 模型检查每个 key 的线性一致性，同时统计请求成功率、延迟和无 Leader 时间。
测试结束执行最终一致读，保存 history、日志、网络规则、节点 term/commitIndex 和 checker 产物。

若出现 stale read，先检查 Client 是否调用了 follower stale API，再定位最小反例：哪次写已在真实时间上完成，哪次读随后返回旧值，期间哪个分区或 Leader 变化发生。复现时固定随机种子、故障计划和版本，缩短无关操作，而不是先根据日志猜根因。

十、调度系统和支付系统怎样写 Checker

Jepsen 不只测试数据库。分布式调度器可以生成带唯一 ID 的任务，Worker 执行时向一个可查询集合追加 (task_id, owner, token, effect_id)。Checker 验证每个已确认任务最终有结果、同一资源的 token 单调、低 token 不在高 token 后产生副作用，以及业务 effect_id 没有重复。

“任务最多执行一次”若通过进程日志判断，很容易误报。Worker 可能打印两次开始日志，但业务存储只接受一次条件更新；也可能只打印一次，却在超时重试中调用外部 API 两次。Checker 要观察承诺所在的副作用边界。

支付链路可用业务号创建订单、模拟请求超时和多入口补偿，再从订单状态、钱包流水和权益记录构建历史。不变量包括：一个 trade_order_no 最多一笔有效扣款；订单 PAID 必须有扣款证据；退款后净权益符合状态机；任何成功响应对应可查询终态。资金系统通常还需要离线对账，Jepsen 历史适合验证协议反例，不能替代全量账务核对。

十一、故障注入与混沌工程的边界

故障注入是一种手段。Jepsen 倾向于在隔离环境里高强度探索一致性反例，保留完整历史并由 checker 判定；生产混沌工程更关注真实依赖、可用性、告警和人员响应，必须控制爆炸半径。二者可以共享故障模型，但验收问题不同。

在生产环境直接做网络二分和磁盘损坏，若没有业务隔离、停止条件和恢复方案，测试本身会成为事故。协议正确性测试应先在可重建集群完成；生产演练验证流量治理、观测、自动恢复和 runbook，通常不需要让用户数据承担未知一致性风险。

故障注入也不同于 mock 一个异常返回。真正的协议窗口包括请求已到服务端但响应丢失、进程持久化后立刻崩溃、旧连接跨越 Leader 切换、网络单向可达、节点暂停后恢复。代理、iptables、进程控制和存储 fault injection 才能覆盖这些时序。

十二、避免测试工具自己制造错误

Client 必须线程安全或每个逻辑进程独占连接，连接池不能静默重试非幂等请求。操作值要全局唯一，序列化与反序列化不能丢精度。控制节点时间和资源要稳定，历史写盘不能成为系统吞吐瓶颈。

Nemesis 停止时要确认故障真的恢复，例如清理全部网络规则并验证节点互通。测试清理不完整会让下一轮继承旧分区。DB setup/teardown 必须删除旧状态，否则“新集群”可能带着上次 term、成员和数据。

Checker 也需要用已知正确和已知错误的模拟历史做单元测试。history.sim可以生成确定性历史供 checker 验证。自定义业务 checker 若只看最终计数，很可能漏掉中间违约；若忽略 info 操作，又会制造错误结论。

十三、怎样提高发现反例的概率

随机测试有价值，但完全均匀的随机经常错过短窗口。可以根据协议状态定向触发：观察到新 Leader 后立即隔离它；日志刚复制一部分时 kill；租约即将过期时暂停 owner；快照安装中断开连接；成员处于 joint configuration 时失去节点。系统暴露的 term、commitIndex 和租约时间可作为 nemesis 触发信号。

并行运行不同随机种子能扩大覆盖，失败后必须保存种子和完整环境。发现反例后做 shrinking：减少节点、操作和故障，保留仍能触发的最小历史。一个 20 条操作的反例比十小时日志更容易交给开发者修复和加入回归测试。

版本升级要重跑历史套件。共识库、存储引擎、JDK、内核、客户端和配置变化都可能改变时序。把 Jepsen 当发布门禁时，区分稳定短套件与夜间长套件：前者覆盖已有反例和核心故障，后者探索更多组合。

十四、怎样阅读一次测试报告

先看测试目标、版本和配置，确认 checker 模型与产品承诺一致。再看 valid? 的具体状态：true、false、unknown 或 checker error 含义不同。若 false，找到最小异常操作、真实时间边和模型无法继续的位置；随后对齐 nemesis 时间线和节点日志。

正确性之外再读可用性：故障期间成功率、P95/P99、最长不可用窗口、恢复后吞吐与错误。一个保持线性一致但网络轻微抖动就停写十分钟的系统，协议可能安全，生产表现仍不可接受。

报告还应公开限制：没有测试哪些 API，未覆盖哪些故障，Client 如何分类异常，运行了多少次、每次多久，checker 是否完备。单次通过不应写成“证明数据库绝对正确”；一个清晰反例则足以推翻对应承诺。

十五、从不变量开始建立团队测试套件

第一步不必搭建完整 Jepsen 集群。先选一个高价值对象，写出操作模型和两三条不变量，用应用集成测试记录 invoke/complete 历史。随后加入进程 kill 和网络延迟，确认 UNKNOWN 能被正确记录。历史格式稳定后，再接入 Knossos、Elle 或自定义 checker。

可以按下面的顺序评审测试设计：

系统公开承诺哪个一致性或隔离模型，业务不变量是什么？
Workload 的返回值是否暴露了足够顺序与依赖信息？
Client 能否准确区分成功、明确失败和结果未知？
Nemesis 是否命中 quorum、租约、持久化、快照和成员变更窗口？
Checker 检查的是中间历史还是只看最终状态，它有哪些不完备性？
故障恢复后是否继续运行，观察活性与收敛？
失败能否用种子、版本、配置和最小历史复现？
正确性与可用性是否分别报告？

故障注入不会替系统选择正确模型，Jepsen 也不会从日志里自动猜出业务承诺。测试的起点是把承诺写成状态机、依赖图或不变量；之后每个请求和故障都成为历史证据。checker 一旦找到无法解释的操作组合，就得到一个具体、可复现、足以推翻承诺的反例。