设计取舍
主线位置：四条主线的汇总。第 1–4 条是主线 1「一次 model 的一生」的骨架，第 5 条是主线 2「一次 load 能读到什么」的边界，第 6 条是主线 3「一次数据竞争怎么被抓到」，第 7 条横跨所有检测器；第 1、5 条合起来就是主线 4「看到什么、看不到什么」。机制都在前面各章，这里每条只写做法、换来什么、代价，证据链到有数字的那一页。
flowchart TB lib["1 做成库：替换类型 + 重放闭包"] --> c1["侵入式；被测库自己维护切换层"] co["2 单 OS 线程 + 有栈协程"] --> c2["依赖 generator；spawn 不是调度点；Send 约束丢失"] rp["3 每轮从头重放，只记分支选择"] --> c3["模型必须确定；每轮重跑全部前缀"] dp["4 DPOR + 可选抢占上限"] --> c4["交错数仍随线程数爆炸，上限要用户选"] mm["5 有意简化的内存模型"] --> c5["SeqCst 访问误报；LB、第 8 次以前的写漏报"] vv["6 检测器共用一套向量时钟"] --> c6["只覆盖 loom 类型；逃出守卫的指针不查"] pn["7 所有发现都是 panic"] --> c7["二次 panic 时进程 abort；失败上下文靠重放"]
1. 做成库，而不是编译器插桩或解释器
做法：loom 不改编译器、不解释执行，只提供一套和 std 同名的类型。被测代码通过一层 #[cfg(loom)] 把 std::sync::atomic、Mutex、thread::spawn、UnsafeCell 换成 loom 的；测试写成 loom::model(|| { ... })，loom 反复执行这个闭包（lib.rs:4-96）。每个 loom 类型只是对象仓库里的一个下标，状态都在当轮的 Execution 里（Execution 与对象仓库）。
换来：普通的 cargo test 就能跑，结果是确定的；不依赖 nightly、不依赖平台的 sanitizer。被测代码的每一次同步操作都经过 loom 自己的代码，所以调度、读值、竞争检测都能精确控制。
代价：
- 侵入式。loom 只看得见换成 loom 类型的操作（
lib.rs:253-269）。std 的原子、系统调用、没走切换层的依赖对它都不存在，parking_lot_core 这类直接用真实原子和系统调用的库放不进模型（「loom 通过」意味着什么）。 - API 不完全相同。原子不能
const构造（static里写AtomicUsize::new在--cfg loom下是 E0015）、UnsafeCell只能通过with/with_mut访问、锁恒为Ok（cfg(loom) 切换层）。 - 维护成本落在被测库。tokio 的
src/loom/共 1 071 行，bytes 为 loom 另写了一份非const的Bytes::new；依赖里写裸cfg(loom)的库在下游开--cfg loom时会被一起换掉，在模型外用到就 panic（坑：在模型外用 loom 类型）。
2. 一个 OS 线程，模型线程是有栈协程
做法：每个模型线程是一个 generator crate 的有栈协程，每一轮重新创建；切换线程就是从当前协程 yield 回调度循环，再 resume 另一个（协程调度器）。thread::spawn 只把闭包放进 queued_spawn，等当前协程让出后才建协程。
换来：调度完全由 loom 决定，交错数与核数、负载无关。本卷所有「第 N 个交错」「共 N 个交错」在任何机器上都能复现（怎么读这一卷）。真实的 Rust 代码可以原样跑在协程里，这正是 11 动手 那个「线程写成步骤列表」的最小检查器做不到的。
代价：
- 依赖
generator的平台相关实现（上下文切换、栈分配），每轮都要重建全部协程栈。 spawn不是调度点，被stop_exploring包住也没有效果（E17，写一个好模型）；spawn 之后、第一次切换之前出的错，排队中的闭包要在调度器状态已经撤走之后才 drop，见第 7 条。- 所有模型线程在同一个 OS 线程上，loom 的
spawn不要求Send：模型里传Rc能编译、能通过，换回 std 才编不过（线程、线程局部与 lazy_static）。 - 线程表与向量时钟都是
MAX_THREADS = 5长的定长数组，含主线程最多 5 个（坑）。
3. 每轮从头重放，只记分支选择
做法：loom 不保存程序状态的快照。Path 只记每个分支点选了什么（调度给谁、load 读哪次写、要不要伪唤醒）；下一轮从头执行闭包，走到记录的末尾之前按记录选，之后新建分支；一轮结束 step 从末尾往前找下一个还有选项的分支（Path：路径与深度优先）。
换来：不需要复制栈、堆、协程，实现简单；路径小到可以存盘。checkpoint 文件就是序列化的 Path，E3 里是 1 607 到 3 223 字节（checkpoint、日志与位置），拿它能精确重放失败的那一轮。
代价：
- 模型必须确定。闭包的行为只要依赖 loom 看不见的东西（std 的
static、HashMap的迭代顺序、时间），重放就会走偏：报「Is the model fully deterministic?」，或者直接撞上 loom 内部的一致性断言（坑）。 - 每一轮都把公共前缀重新执行一遍。耗时和交错数基本成正比，本机约每秒 7 000–9 000 个交错；3 个线程、不设抢占上限的 E2 模型 1 393 998 个交错要约 154 秒（抢占上限与剪枝）。
4. DPOR，加一个可选的抢占上限
做法：每个线程即将做的操作，在对象上找上一次「相关」的访问，两者没有 happens-before 就在那个路径位置登记回溯；选线程时尽量不抢占（DPOR）。LOOM_MAX_PREEMPTIONS 在此之上限制一条路径里的抢占次数，并为此补额外的回溯点（抢占上限与剪枝）。
换来：互不相关的操作不再两两换序。11 动手 里同一组模型对照：3 个线程各写两次自己的原子，朴素枚举是 90 种交错（多项式系数），loom 是 3 个；4 个线程各写一次，朴素枚举 24 个，loom 反而是 26 个（推测：多出来的来自 loom 模型里 join 这类朴素枚举里没有的分支点）。
代价：相关的操作仍然要全排，交错数随线程数和操作数增长很快：E2 里 4 个子线程各一步，上限 2 是 8 230 个、上限 3 是 133 022 个（写一个好模型）。上限取多少要用户选，上游文档的建议是 2 或 3；同一个模型里还有 max_branches、max_permutations 等截断（「loom 通过」意味着什么）。
5. 有意简化的内存模型
做法：每个原子只保留最近 7 次写（MAX_ATOMIC_HISTORY），load 按 coherence 规则在其中列候选；SeqCst 访问按 AcqRel 处理，只有 fence(SeqCst) 做全局同步；按程序顺序逐个执行，load 只能读已经执行过的写（03 内存模型）。
换来：每个 load 的候选数有上界，状态空间小；实现上只需要每线程几套向量时钟加一个 7 格的环形数组。注释里写明了取向：SeqCst 的旧实现不对，「just disable it. This may fail to model correct code, but will not silently allow bugs」（rt/thread.rs:336-341）。
代价：两个方向都有。SeqCst 访问写的 SB 照样给出 (0,0)，正确的算法被误报（坑）；LB 的 (1,1) 永远不出现、同一原子写超过 7 次后更早的值不再是候选，这两条是漏报（SeqCst 与 load buffering、写历史与 coherence）。
6. 检测器共用同一套向量时钟
做法：UnsafeCell 与原子 with_mut / unsync_load 的竞争检测，直接比较内存模型那套 causality 时钟；泄漏在每轮结束时查对象仓库；死锁在调度时查线程状态（04 检测器）。
换来：不需要额外的执行，也不需要「两次访问恰好交错到一起」：单元格访问不是调度点，竞争在第一个交错就能判出来（E7：两个线程直接 with_mut，第 1 个交错报错，UnsafeCell 与原子的非同步访问）。11 动手 的最小检查器用同样的办法，几十行就能抓到 Relaxed 消息传递里的竞争。
代价：只覆盖 loom 类型。mem::forget 一个 std Arc 不报泄漏（E8）；从 ConstPtr / MutPtr 拿出去的裸指针、守卫结束后还在用的指针都不受检查（UnsafeCell 与原子的非同步访问）。
7. 所有发现都以 panic 报告
做法：竞争、泄漏、死锁、分支超限、用户断言失败，全部是 panic，从模型线程的协程一路传出 model。没有别的报告渠道。
换来：和 #[test]、#[should_panic]、catch_unwind 天然配合；第一个失败的交错立刻停下，不必跑完。
代价：
- panic 之后要展开栈、drop 对象，这时 loom 的执行状态可能已经不在了。栈上或排队中的 spawn 闭包里有 loom
Arc，drop 时再碰执行状态就是第二次 panic，进程 abort（退出码 134）：死锁之后、以及 spawn 之后第一次切换之前的任何失败都会这样（坑）。#[should_panic]写的死锁测试因此会失败。 - 一个 abort 带走整个测试进程，同一个二进制里排在后面的测试都不跑。
- 失败只给出最后一条消息。要看失败那一轮怎么走到这里，得用 checkpoint 把它存下来，再开
LOOM_LOG重放（checkpoint、日志与位置）。
小结
- 做成库换来普通
cargo test下的确定性，代价是侵入式：只看得到 loom 类型，被测库要自己维护切换层。 - 单 OS 线程加有栈协程让交错数与机器无关，代价是依赖
generator、spawn不是调度点、Send约束丢失、最多 5 个线程。 - 每轮重放只记分支选择，路径几 KB 可以存盘重放；代价是模型必须确定、耗时与交错数成正比。
- DPOR 去掉互不相关的换序（朴素枚举 90 个，loom 3 个），相关操作仍然要全排，抢占上限由用户取 2 或 3。
- 内存模型有意简化：SeqCst 访问误报、LB 与 7 次写窗口漏报，方向各不相同。
- 检测器搭在同一套时钟上，第一个交错就能判竞争，但只覆盖 loom 类型。
- 一切以 panic 报告，代价是某些情况下二次 panic 让进程 abort，失败上下文要靠 checkpoint 重放。