分布式系统 16：从故障轨迹到有限状态搜索

一条测试通过，说明具体输入与调度没有触发已检查的错误。它没有回答：另一个消息先到会怎样，恢复恰好发生在两次授票之间会怎样，以及是否存在更短的失败过程。

第 15 篇 已用独立历史检查器判断有限客户端历史。本篇继续使用累计 Go Raft 核心，枚举一个明确受限的选举环境。目标是找出漏保存 votedFor 的最短反例，同时说明“穷尽”“最短”和“没有发现错误”分别依赖什么条件。

课程结构对应 MIT 6.5840 当前公开日程中的验证与 IronFleet 讨论，Stanford CS244B 则提供原始论文研讨路径。本篇的 BFS 和事件模型为原创实验，没有运行课程证明或照搬作业实现。MIT 2026 日程与验证讲义、Stanford 2024 日程

三种检查各自回答什么

确定性故障注入控制实现的一条执行轨迹：在哪一步丢消息、在哪一步重启、哪份状态保存错误。历史检查把外部调用与返回交给独立规格，判断这些结果是否能解释为合法顺序。状态搜索则枚举环境允许的不同动作，探索可达状态，再检查性质。

flowchart TB
  CODE["实际核心 + 受控环境"] --> RUN["确定性执行一条轨迹"]
  RUN --> API["客户端调用与返回"]
  API --> HIST["历史checker：能否匹配顺序规格"]
  CODE --> ACTION["枚举所有允许的下一动作"]
  ACTION --> GRAPH["搜索有限可达图"]
  GRAPH --> INV["逐状态检查指定不变量"]

三者的 oracle 也不同。日志复制检查不能替代客户端返回语义；线性一致性历史通过，也不能证明未被客户端观察的内部状态一定满足全部协议约束。第 15 篇最初的 Add 错误对照仍可线性化，就说明启用变异不等于已经证明这个观察必然非法。

IronFleet 将高层规格、协议与实现之间的对应关系分别证明，并声明可信组件和环境前提。本篇没有这些完整证明。直接调用 Go 核心只能减少一层另写协议模型的偏差，仍须解释环境限制、状态摘要与搜索实现是否保留目标行为。IronFleet，SOSP 2015，§2.5、§3、Figure 3

把搜索范围写成可核对的参数

模型固定三个成员，日志为空，任期只允许 0 和 1。节点 1、2 只有在本地 term=0 时才能各 Timeout 一次；节点 3 最多执行一次 CrashRestart。没有日志复制、读请求、配置变更或快照，也没有后台时间推进。

允许的动作只有三类：触发一个合法 Timeout，投递队列里的一条真实消息，重启节点 3。一个核心输入事件及随后的全部保存、确认作为一个原子模型动作，不探索事件内部崩溃窗口。Crash 与恢复合并成一个动作，所以最短长度以这一粒度计算。

flowchart TB
  S["当前完整模型状态"] --> T["Timeout 1或2：仅term0且未用额度"]
  S --> D["Deliver：选择真实队列中的消息"]
  S --> R["CrashRestart 3：最多一次"]
  T --> NEXT["事件及全部保存确认结束"]
  D --> NEXT
  R --> NEXT
  NEXT --> CHECK["检查状态与历史不变量"]

只要暂不投递某条消息，就能表达有限安全性坏前缀所需的延迟与重排，因此没有额外 Drop 动作。模型不要求最终送达，也不据此评价活性。没有重发或重复生成：两次 Timeout 至多产生四个 RequestVote，每个请求最多产生一个回复，加上一次恢复，总动作数至多为 11。这个上界只属于本模型。

Timeout 不能简单解释成“随时强行进入任期 1”。如果节点 2 在竞选前先收到任期 1 的请求，它已经离开 term0，不再满足本模型的 Timeout 条件。搜索必须找到合法的竞选与交付顺序，不能人工修改任期来构造预期反例。

故障发生在保存适配器

核心的 Step 若返回 Persist，适配器必须保存对应映像，再调用 AdvancePersisted。核心会检查确认参数是否与待保存状态相等。本篇的故意错误并非把坏映像传入这个接口而期待它接受。

错误适配器把节点 3 的磁盘模型中的 Vote 存成 0，却把原来的正确映像作为确认参数传回核心。核心看到的确认一致，便释放成功投票回复；重启从错误磁盘映像恢复后，节点 3 才遗失已投出的票。term 仍正常保存。

flowchart TB
  WANT["应保存：term1，vote1"] --> DISK["坏适配器：disk保存term1，vote0"]
  WANT --> ACK["却以原正确映像确认成功"]
  ACK --> REPLY["核心释放给候选1的成功回复"]
  DISK --> RESTART["重启后恢复vote0"]
  RESTART --> AGAIN["可在term1再次授票给候选2"]

这是存储接口契约被违反后的故障注入，不是合法 Raft 前提下出现反例，也不是操作系统或设备真实丢写观察。正常适配器保存与确认完全一致，其他代码路径不变。

审计同时记录两种历史性质：同节点同任期不得投给不同候选者，同任期不得有不同节点曾当选。历史记录跨重启保留；只检查现在有哪些角色等于 Leader，可能遗漏已经退位的历史 leader。搜索双当选时，也不能在更早的双投位置剪枝，否则永远无法到达后续性质违反。

不克隆 Node，重放每个前缀

State.Clone 只复制持久映像；New 恢复后产生 Follower，并不会恢复原来的候选者票集或待释放效果。Status 也不是 Node 全部私有状态的序列化格式。因此实验没有用 State 加 Status 冒充完整克隆。

每条 BFS 后继路径都从独立初态构造三个节点，重新执行完整动作前缀。重复计算换取了清楚的状态隔离：分支不会共享 Node、队列或审计容器，不需要为搜索大改核心。

visited 的键为完整规范 JSON 字符串，包含三个 Status、三个磁盘 State、精确票集、完整消息多重集合、Timeout/重启额度、两类历史位集和完整观察序列。Go map 可以在内部使用散列，但键仍按完整字符串比较；没有只保存一个短指纹。CMC，OSDI 2002，§3.3–3.4

候选票集必须保留身份，不能只保留数量。两张票来自 {1,3} 或 {1,2}，对后续重复回复的效果可能不同。wrapper 根据实际输入和自投观察重建集合，每一步还与 Status.Votes 计数比较。计数断言只是辅助检查，不能代替身份进入状态键。

可以省略哪些私有字段，也需要逐项说明。pending 在每个动作边界已经全部确认；日志和快照为空；不执行 Replicate，因此 progress、inflight 和复制序号不会影响后继；不执行 BeginRead，也不改变配置。允许这些新动作后，当前状态摘要就不能直接沿用。消息排序之所以安全，是因为选择依据是稳定消息身份，不是队列下标。

BFS 的最短性与三种未发现结果

初态深度为 0，每个动作成本为 1。FIFO 队列先处理浅层状态，再处理深层状态；后继第一次入队时登记 visited。若后继枚举完整、状态合并保持未来行为与判定，首次找到的坏状态就不存在更短的模型动作路径。

flowchart TB
  L0["深度0：初态"] --> L1["深度1：全部合法后继"]
  L1 --> L2["深度2 …"]
  L2 --> L4["深度4：无双投违反"]
  L4 --> L5["深度5：首次双投反例"]
  L5 --> L6["继续搜索另一个目标"]
  L6 --> L7["深度7：首次双当选反例"]

图中的继续搜索表示双当选任务允许通过双投状态；两种目标分别执行 BFS。工具还针对反例长度 L 重新搜索到 L−1，作为遍历实现的自检。它不能弥补状态键漏字段或后继枚举漏分支。

输出区分四种状态：COUNTEREXAMPLE 表示找到反例；EXHAUSTED_NO_COUNTEREXAMPLE 表示有限图完整穷尽；NO_COUNTEREXAMPLE_WITHIN_DEPTH 表示深度边界仍有可展开前沿；UNKNOWN 表示状态预算不足。异常终止、解析失败或资源不足都不能写成安全性通过。

TLC 固定版本文档同样区分 BFS、深度受限 DFS 与模拟；安全性 BFS 最短反例的性质不能直接套到其他搜索模式。这里没有安装或执行 TLC，而是对小型搜索器直接使用分层论证。TLA+ Toolbox 1.7.1，Checking Mode

实际找到的五步与七步

固定目录 race 程序的搜索结果如下。状态数包含本实现保守保留的完整审计序列，不是协议固有常数；改变动作排序或等价状态表示后，不应期待计数不变。

目标与适配器	结果	搜索证据
正常：双投、双当选分别搜索	完整有限图无反例	各访问870状态、展开862状态
漏票：双投	最短5步	找到时访问137状态
漏票：双投，限制深度4	边界内无反例	访问112状态、前沿74
漏票：双当选	最短7步	找到时访问627状态
漏票：双当选，限制深度6	边界内无反例	访问548状态、前沿248

实际七步轨迹先让节点 1、2 各自竞选并自投。节点 3 收到 1 的请求、产生成功回复，但这条回复可以继续留在网络中；3 重启忘票后，再收到 2 的请求并产生另一条成功回复。最后两条回复分别送到候选者，两者才先后被核心观察为当选。

sequenceDiagram
  participant A as 节点1
  participant B as 节点2
  participant C as 节点3
  Note over A: 1 Timeout，自投term1
  Note over B: 2 Timeout，自投term1
  A->>C: 3 投递RequestVote
  Note over C: 易失vote1；disk vote0；成功回复暂存
  Note over C: 4 CrashRestart，恢复vote0
  B->>C: 5 投递RequestVote，授票2
  C-->>A: 6 交付成功回复，1当选
  C-->>B: 7 交付成功回复，2当选

五步已经违反“一任期一票”，但此时两个成功回复尚未交付，历史上还没有 leader 当选。漏保存、双投和双当选是三个不同位置，不能把它们混成同一个事件。

这个结果还可以用下界交叉核对。两个不同候选者需要两次 Timeout；节点 3 向两者授票，需要两次请求投递；在保持易失授票检查的变异中，中间还需一次恢复，合计至少五步。两个候选者要真正当选，还需各收到一条成功回复，至少再加两步。候选者已经自投，不能互相提供另一个成功票；可被遗忘的多数交点只有节点 3。因此实际搜索的 5 与 7 达到这个模型内的下界。

回放的是事件与状态，不是保存好的结论

证据 JSON 包含模型参数、结果类型、动作、每步实际交付消息、状态与审计，以及最终违反。回放先检查动作在当前状态是否允许，重新运行核心，再逐步比较实际消息载荷与状态。篡改节点身份或最终磁盘记录必须被拒绝；只打印文件中已经保存的 COUNTEREXAMPLE 不算回放。单条回放不校验 Visited、Expanded 或 Frontier 统计，也不认证最短性；这些结论来自实际 BFS、L−1 搜索及其实现审查，不能仅靠导入 JSON 取得。

正常适配器的对照还有一个容易混淆的地方：坏轨迹第二条投票回复是 Granted=true，正常环境生成的对应回复会是 false。动作选择使用 type/from/to/term/campaign 的稳定身份，轨迹另存完整载荷。正常对照消耗自己真正生成的拒绝票，不能把坏分支的成功票注入正常系统，再把失败解释为正常实现也不安全。

本模型无重发，同一稳定身份唯一。若增加重发或多个并发请求，就需要新的消息尝试身份；不能把当前 selector 当成一般网络消息 ID 方案。

flowchart TB
  TRACE["保存的调度：选择哪个消息身份"] --> BAD["坏适配器重放"]
  TRACE --> GOOD["正常适配器同调度"]
  BAD --> TRUE["实际产生Granted=true"]
  GOOD --> FALSE["实际产生Granted=false"]
  TRUE --> EXACT["与坏证据完整payload逐步相符"]
  FALSE --> SAFE["真实拒绝票不能产生第二多数"]

FoundationDB 的模拟把网络、磁盘、时间和伪随机来源纳入受控环境，才使轨迹可重复。单独保存随机 seed 并不能自动控制所有非确定性。本篇没有随机源，节点、消息和动作均稳定排序；版本、模型参数和实际事件仍须随证据保存。FoundationDB 论文，SIGMOD 2021，§4

证据能够支持的结论

源码位于 examples/distributed-systems/verify16/，直接导入累计 raft 包，不修改核心。程序默认写出正常搜索报告、两个反例、L−1 检查和小预算 UNKNOWN；证据可用相同产物单独回放。

cd examples/distributed-systems
mkdir -p .build/tmp
GOTMPDIR="$PWD/.build/tmp" GOCACHE=/private/tmp/ds-go-cache go build -race -o .build/verify16 ./verify16
./.build/verify16
./.build/verify16 -replay .build/verify16-results/broken-election.json

2026-09-20 已实际完成固定目录 race 搜索、反例回放自检和正常对照，完整运行退出 0。详细命令和输出见 验证记录，原始资料见 论断核验。搜索结果只能证明这组参数、动作和性质下的有限事实，不能扩大成全部 Go Raft 或容错 KV 已被形式化验证。实际 五步双投轨迹 与 七步双当选轨迹 也随文保存。命令示例先运行默认搜索生成本地文件；附件以 .json.txt 保留原始 JSON；下载后可直接把路径传给 -replay，无需改后缀。

安全违反有有限坏前缀；活性通常涉及无限执行与公平性。如果环境一直不交付消息，有限步内没有 leader 并不能证明活性实现错误。本篇没有检测公平循环或活性 lasso。IronFleet 的活性结论也依赖存活 quorum 最终同步等前提，并不承诺永久分区下任意请求都完成。Specifying Systems，Chapter 8、IronFleet，§4

反向核验读取了 Lamport 的书籍勘误与 Known Toolbox Problems；后者封面日期为 2009-11-17，不能因为文件仍在线，就把当年的工具问题写成当前版本仍有的缺陷。未找到新的问题也不等于实现已被证明正确。书籍勘误、历史工具问题记录

两道练习

练习一：把 Crash 与 Recover 拆开，七步还是最短吗？

原路径中合并的一步会变成两步，相同过程至少增加一个动作。搜索范围还可能允许节点停机期间投递消息或发生其他事件，需要重新定义转移并搜索。最短长度属于模型动作粒度，不能脱离它比较两个工具的数字。

练习二：正常搜索耗尽状态预算，却没找到反例，能否输出通过？

不能。未展开状态可能包含目标违反，应返回 UNKNOWN，并记录预算与剩余前沿。只有队列真正耗尽且没有资源截断，才能声明该有限图内无指定反例；即使如此，也不能推广到更多节点、任期或未建模操作。

下一篇将进入 ZooKeeper 的服务模型，讨论 znode、版本、顺序节点、session 与 Watch，并区分默认一次性通知和可回放事件日志。