写一个好模型

主线位置：主线 1 的使用面。每一条建议都对应 02 运行时 里的一处机制：交错数由 DPOR 与抢占上限决定，分支数由 max_branches 截断，重放要求确定性。

flowchart TB
  q["要检查的性质"] --> shape["定形状：2～3 个线程，每线程 1～2 个关键操作"]
  shape --> small["把容量、间隔等常数调小，让几步就走到边界"]
  small --> spin["所有自旋循环里放 yield_now"]
  spin --> det["去掉不确定来源：随机数、时间、HashMap 迭代顺序、跨轮的全局状态"]
  det --> assert["在模型里 assert；需要统计结果时用 std 容器在模型外收集"]
  assert --> run["--release，LOOM_MAX_PREEMPTIONS=2 或 3 先跑"]
  run --> rev["反向验证：改错一处，确认会失败"]

线程数与操作数

交错数随线程数和每线程的操作数增长得很快。下表是 E2 的模型（exp-loom/survey/tests/bound.rs）：T 个子线程各做 O 次「fetch_add(1, AcqRel) + 加锁加一」，主线程 join 后断言计数；各列是不同的抢占上限（抢占上限与剪枝）。交错数是确定的，与机器和负载无关。

几条经验：

• 线程比操作贵：同样是 4 个「操作单元」，2 × 2 在上限 3 时 270 个交错，4 × 1 是 133 022 个。
• 主线程本身也算一个线程，最多 5 个线程（含主线程，线程、线程局部与 lazy_static）。能让主线程承担一个角色就别多 spawn 一个。
• 只把「需要互相竞争的那几步」放进模型：初始化、无竞争的准备工作放在 spawn 之前，loom 不在单线程阶段产生分支（只有一个可运行线程时没有选择）。

上游自己的测试大多是这个尺度。比如 tokio 1.54.1 registration_set.rs:190-223 的 deregister_races_with_prior_event_delivery：一个驱动线程分发事件后 release()，主线程同时注销并 drop 自己的句柄，join 后再 release() 一次，最后断言没有残留。两个线程，每边两三步，正好覆盖 reactor 一页里说的那个竞争。

把常数调小

数据结构的「边界情况」（队列满、块用完、袋子封口）通常要很多步才能走到，在 loom 里就是很长的路径。做法是在 #[cfg(loom)] 下换一组小常数：

调小常数不改变算法，只是让「满了要换块」这类分支在两三步之内就能被走到。

自旋要 yield_now

loom 的调度器在当前线程还能跑时尽量不切换（DPOR），一个不让出的自旋循环会一直跑下去，直到路径长度碰到 max_branches（默认 1000）。文档专门写了一节（lib.rs:167-175）：loom 的调度器「by design, not fair」，循环里必须调 loom::thread::yield_now，告诉 loom「要别的线程先往前走，我才能继续」。

E11（exp-loom/survey/tests/misc.rs）：两个线程用 CAS 自旋锁保护一个 UnsafeCell。

hint::spin_loop() 与 sync::atomic::spin_loop_hint() 在 loom 里就是 yield_now()（sync/atomic/mod.rs:20-23），所以被测代码的自旋循环里如果本来就有 spin_loop，切换层换掉后自然满足。yield_now 还影响 load 能读到的值（让出之前读过的旧值不再给，load 的候选），这是自旋能结束的另一半原因。

模型必须确定

loom 每一轮都从头重放闭包，靠 Path 里记下的选择走到上次的位置（Path：路径与深度优先）。重放时发现这一步的分支类型和记录的不一样，就 panic：

Reached unexpected exploration state. Is the model fully deterministic?

（rt/path.rs:211、232、323 三处）。常见来源：

• 随机数、时间、线程 id 的哈希（HashMap 的迭代顺序每个进程不同，同一进程里每个 HashMap 的种子也不同）。
• 跨轮保留的全局状态：std 的 static 计数器、OnceLock，在上一轮被改过，这一轮走了不同的分支。
• 被测库里的「自适应」逻辑：读 CPU 数、读环境变量。tokio 的切换层把随机种子固定为 1、CPU 数固定为 2（cfg(loom) 切换层）。

loom::lazy_static! 每轮重新初始化，loom::thread_local! 每线程每轮一份，正是为了这一条。

断言写在哪

• 模型里的 assert! 就是性质本身。失败时 panic 穿出 model，测试失败；loom 报告的是第一个失败的交错。
• 想看「跑过的交错一共出现了哪些结果」，用 std 的 Mutex<BTreeSet<_>> 之类放在 static 里，在模型里插入、模型结束后打印。std 类型对 loom 不可见，不产生分支，也不会被重置。本卷的 litmus 实验（SeqCst 与 load buffering）都是这么写的。这类收集只用来观察，不能拿来影响模型里的控制流，否则就违反了上一节的确定性。
• 数交错数：同样用一个 std 原子，每轮开头加一（本卷实验的 tick()）。

反向验证

一个通过的模型，只说明在这个形状、这个上限下没有找到失败。要知道模型「有没有咬到」要测的性质，把被测代码改错一处（去掉一个 Acquire、去掉一道 fence、把 while 改成 if），确认 loom 报错。crossbeam 卷 最小 EBR 对每个通过的模型都配了这样的改动，也记下了一个「改错了却没被抓到」的版本及原因：模型形状没有覆盖那条交错。

本卷 05 部分的例子：Condvar 的 if 写法 loom 通过（因为 loom 的 Condvar 不伪唤醒），换成 Notify 后第 5 个交错被抓到（Condvar、Notify 与 park）。没有这个对照，前一个「通过」很容易被误读成「if 写法没问题」。

skip_branch 与 stop_exploring

0.7.0 加的三个函数（#323）把路径上的分支标成不探索（抢占上限与剪枝）。E17（exp-loom/survey/tests/extra.rs，3 个线程各两次 fetch_add，不设上限）：

第二行没有效果，因为 spawn 不是调度点，被包住的那一段本来就没有分支。skip_branch 适合「前面这段的交错我已经单独检查过，现在只关心后面」的情况；它减少的是交错数，同时也就不再检查被跳过的那部分。

抢占上限

loom 文档的建议（lib.rs:283-292）：

In practice, setting the thread pre-emption bound to 2 or 3 is enough to catch most bugs while significantly reducing the number of possible executions.

用 LOOM_MAX_PREEMPTIONS=2 或 3（或 Builder::preemption_bound）。理由看交错数和耗时：上面的表里，3 × 1 的模型上限 2 是 732 个交错、上限 3 是 5 594 个、上限 4 是 29 500 个，不设上限是 1 393 998 个；4 × 1 上限 3 已经是 13 万多个。耗时见下一节。crossbeam 的 CI 用上限 2，注释说 epoch 的两个模型约 11 分钟。

先用 2 跑通、做完反向验证，再视耗时决定是否用 3。上限每加 1，交错数乘的因子在表里是 2.4～25 倍不等，取决于模型形状。

release 与 debug

文档建议用 --release（188-190 行）：loom 每一轮都要重新执行整个闭包，再加上调度、向量时钟、对象仓库的开销，优化与否差别很大。

实验 E20（exp-loom/speed/timing.sh，跑的是 exp-loom/survey 里 E2 的同一个模型；release 3 轮、debug 1 轮；拿 exp-loom/.timing.lock 独占运行。开始时 1 / 5 分钟负载 2.55 / 2.86，release 三轮期间 1 分钟负载升到 3.2–3.5，结束时 4.65 / 3.48，所以下表是「量级，负载约 3 时取得」。loom 只用一个 OS 线程，三轮之间相差不到 1%）：

• 交错数与 E2 一致，和负载无关。
• 每秒交错数随模型变化不大（7 000–9 000），总耗时基本正比于交错数：4 × 1 从上限 2 到 3，交错数乘 16，耗时也乘 16。估算一个模型要跑多久，先用小上限数出交错数再乘。
• 这个模型 debug 比 release 慢 2.5–2.7 倍。差距取决于被测代码本身的计算量，这里被测代码几乎没有计算，大部分时间花在 loom 的运行时上。

小结

• 线程比操作贵：2 × 2 上限 3 是 270 个交错，4 × 1 是 133 022 个；最多 5 个线程含主线程。只把竞争的那几步放进模型。
• 用 #[cfg(loom)] 把容量类常数调小（tokio 队列 4、BLOCK_CAP 2，crossbeam 袋子 4）。
• 自旋循环要 yield_now（或 spin_loop，loom 下等价）：不让出第 28 个交错撞分支上限，让出后 189 个交错通过（E11）。
• 模型必须确定，否则重放时报「Reached unexpected exploration state. Is the model fully deterministic?」。
• 在模型里断言；统计结果用 std 容器在模型外收集，只观察不影响控制流。
• 每个通过的模型配一个改错一处就失败的对照。
• skip_branch 放在 spawn 之后能把 116 319 降到 617；包住 spawn 的 stop_exploring 没有效果（E17）。
• 抢占上限按上游文档取 2 或 3，依据是交错数与耗时（E2、E20）：release 下每秒约 7 000–9 000 个交错，4 × 1 上限 3 的 133 022 个交错约 18.6 s；debug 慢 2.5–2.7 倍，用 --release 跑。