最小模型检查器

主线位置：主线 1「一次 model 的一生」与主线 3「一次数据竞争怎么被抓到」的骨架，去掉协程、DPOR 与弱内存之后的样子。对应 loom 的 Path、Execution 与 rt::Cell。代码在 exp-loom/hands-on/src/mini.rs。

flowchart TB
  start["check(prog)"] --> round["新的一轮：Exec::new，所有线程 pc = 0"]
  round --> pick{"还有可运行的线程？"}
  pick -->|"pos < path.len()：重放"| rep["取 path[pos] 的选择；可选项个数必须相同"]
  pick -->|"走到头：新建"| new["path.push((0, 可运行数))"]
  rep --> step["exec.step(t)：时钟自增；读写变量或单元格；判竞争"]
  new --> step
  step -->|"竞争"| fail["返回失败"]
  step --> pick
  pick -->|"都结束了"| fin["最终断言；失败就返回"]
  fin --> back["回溯：末尾已用尽的分支出栈，最后一个换下一个选项"]
  back -->|"path 空了"| done["返回：交错数"]
  back --> round

模型怎么写

线程是一串步骤，只有共享访问是调度点；SkipUnless 是线程本地的分支，紧跟在上一步之后执行：

pub enum Op {
  Load { var: usize, reg: usize, mo: Mo },
  Store { var: usize, val: Val, mo: Mo },
  FetchAdd { var: usize, add: u64, mo: Mo },
  CellRead { cell: usize, reg: usize },
  CellWrite { cell: usize, val: Val },
  /// Skip the next `n` steps unless `reg == eq` (an `if` around them).
  SkipUnless { reg: usize, eq: u64, n: usize },
}

消息传递（loom 的 E1）写成两个线程：线程 1 写单元格、置标志；线程 0 读标志，看到 1 才读单元格。

vec![
  vec![
    Op::Load { var: 0, reg: 0, mo: load },
    Op::SkipUnless { reg: 0, eq: 1, n: 1 },
    Op::CellRead { cell: 0, reg: 1 },
  ],
  vec![Op::CellWrite { cell: 0, val: Val::Const(42) }, Op::Store { var: 0, val: Val::Const(1), mo: store }],
]

这就是 loom 要用协程的原因：真实的 Rust 代码不能写成步骤列表。loom 让被测代码原样跑在协程里，每个 loom 操作前调一次 branch，等于在运行时把代码「切」成了步骤（协程调度器）。

重放与回溯

path 里每个调度点一项：选了可运行线程里的第几个、当时有几个可选。每一轮都从初始状态重新执行：

let choice = if pos < path.len() {
  // Replaying: the same choices must meet the same alternatives.
  assert_eq!(path[pos].1, runnable.len(), "model is not deterministic");
  path[pos].0
} else {
  path.push((0, runnable.len()));
  0
};

一轮结束后从末尾往前找第一个还有选项的分支，把它之后的路径截掉：

loop {
  match path.last_mut() {
    None => return Report { interleavings, failure: None },
    Some(last) if last.0 + 1 < last.1 => {
      last.0 += 1;
      break;
    }
    Some(_) => {
      path.pop();
    }
  }
}

和 loom 的 Path::step 是同一个形状，区别是 loom 的分支有三种（Schedule、Load、Spurious），Schedule 里不是「第几个」而是每个线程一个状态，DPOR 往里面登记要回溯的线程（DPOR）。重放那行 assert_eq! 对应 loom 的「Is the model fully deterministic?」（坑）。

向量时钟判竞争

每个线程一个向量时钟，每次共享访问先给自己那一格加一（loom 的 synchronize）。Release 写把写者的时钟存到变量上，Acquire 读把它并进读者的时钟；单元格记最后一次写的时钟和此后所有读的时钟之并：

Op::CellRead { cell, reg } => {
  if !le(&self.cell_write[cell], &self.clock[t]) {
    return Err(format!("data race: thread {t} reads cell {cell} concurrently with a write"));
  }
  let c = self.clock[t].clone();
  join(&mut self.cell_reads[cell], &c);
  self.regs[t][reg] = self.cells[cell];
}

「上一次写的时钟不 ≤ 当前线程的时钟」就是「那次写没有 happens-before 这次读」，和 loom rt/cell.rs 的判定一样。所以和 loom 一样，竞争不靠「两次访问恰好交错到一起」：只要某一轮里读发生时写还没有通过同步传过来，就当场报出。

测试与 loom 对照

tests/mini.rs 的 6 个测试全部通过；tests/vs_loom.rs 把同样的模型写成 loom 版本（线程 0 是主线程，其余 spawn，不设抢占上限）。

前五行是两种枚举方式的差别。最小检查器把所有步骤全排列，交错数正好是多项式系数（counts_match_multinomial 逐个断言相等）；loom 的 DPOR 看出不同变量上的写互不相关，[2, 2, 2] 只剩 3 个。[1, 1, 1, 1] loom 反而多两个，推测来自 loom 模型里 join 这类步骤列表里没有的分支点。

后四行反过来，loom 的数字更大或更早：

• 消息传递 loom 是 6 个交错。最小检查器的线程 0 看到标志为 0 就结束；loom 的模型里还有 spawn、join、Arc 计数，load 还多一个「读哪次写」的分支（一次 model 的一生 逐轮列出了这 6 个）。
• 拆开读写的计数器，loom 第 1 个交错就丢更新：子线程排在主线程之后跑，但它的 Relaxed load 仍可以读到初值 0，因为主线程的写没有 happens-before 它（load 的候选）。最小检查器的内存是顺序一致的，load 永远读最新的写，要等到第 2 个交错两个 load 都排在两个 store 之前才出现。
• 三个 fetch_add：最小检查器只排三个 RMW 的顺序，3! = 6；loom 还要排 Arc 的引用计数、线程结束与 join，Arc 换成 Box::leak 后从 253 降到 94。

反向验证

第二行说明竞争检测确实依赖同步关系，而不是对所有并发访问一律报错。第三行是更值得记住的一种失败：枚举不完整的检查器不会报错，它只会少跑几个交错然后说「通过」。最小检查器靠 counts_match_multinomial 这种和公式对数的测试发现它；loom 这边对应的是本卷各章对交错数的逐个核对（一次 model 的一生）。

省掉了什么

小结

• 两百来行能写出 loom 的骨架：每轮从头重放、只记分支选择、从末尾回溯、向量时钟判竞争。
• 最小检查器的交错数是多项式系数（[2, 2, 2] 是 90），loom 的 DPOR 把它降到 3；反过来 loom 的分支点更多、还模拟弱内存，拆开读写的计数器第 1 个交错就丢更新。
• 消息传递：Release / Acquire 通过，Relaxed 第 3 个交错被报成竞争，和 loom 的 E1 一致。
• 反向验证：Acquire 不并时钟，正确的模型被误报；回溯提前停止，bug 全部漏过而且显示「通过」。
• 线程写成步骤列表是最大的简化，也是 loom 要用协程的原因。