动手

前面十章读的是 loom 怎么做。这一部分反过来：先自己写一个最小的模型检查器，看 loom 的骨架（重放、回溯、向量时钟）去掉协程、DPOR 和弱内存之后还剩多少；再站到使用者一侧，给一个小库加上 loom 切换层和模型，确认改错一处 loom 会报。页面只放思路和关键片段，完整工程在 exp-loom/hands-on/：

src/mini.rs：最小模型检查器，228 行（去掉注释和空行 190 行）；
src/spsc.rs、src/sync.rs：有界 SPSC 环形队列与它的切换层；
tests/mini.rs：检查器自身的 6 个测试（不需要 --cfg loom）；
tests/vs_loom.rs：同样的模型写成 loom 版本，对照交错数；
tests/spsc_loom.rs、tests/spsc_std.rs：队列的 loom 模型与真实线程压测。

依赖只有 loom =0.7.2，而且只在 [target.'cfg(loom)'.dependencies] 下：不开 --cfg loom 时整个工程不依赖 loom。本机 M2 Max，macOS，rustc 1.99.1，--release --offline。

最小模型检查器：线程是步骤列表，内存是顺序一致的，每轮从头重放一条记录下来的路径，深度优先回溯；单元格访问用向量时钟判竞争。交错数与多项式系数逐个相等；Release / Acquire 的消息传递通过，Relaxed 被报成数据竞争，两个线程拆开读写的计数器丢一次更新。反向：Acquire 不并时钟，正确的模型被误报；回溯提前停止，6 个测试里 5 个失败。
给 SPSC 队列加 loom：mod sync 切换层、with / with_mut、loom 模型（容量 2、3 个元素，上限 2 / 3 / 不设分别 157 / 473 / 6 096 个交错）。反向：消费者读 tail 改成 Relaxed、生产者读 head 改成 Relaxed，loom 都在第 1 个交错报竞争；同样的改动在真实线程上压测，300 次里分别失败 6 次和 0 次。

flowchart TB
  mini["最小检查器：步骤列表 + SC 内存"] --> replay["路径重放 + 深度优先回溯（loom 的 Path）"]
  mini --> vv["向量时钟判竞争（loom 的 rt::Cell）"]
  replay --> rev1["反向：回溯提前停 → 5/6 测试失败"]
  vv --> rev2["反向：Acquire 不并时钟 → 正确模型被误报"]
  spsc["SPSC 环形队列"] --> layer["mod sync：loom / std 二选一"]
  layer --> model["loom 模型：157 / 473 / 6 096 个交错"]
  model --> rev3["反向：任一侧 Acquire 改 Relaxed → 第 1 个交错报竞争"]
  rev3 --> stress["同样的改动在真实线程上：300 次失败 6 次 / 0 次"]

怎么跑

cd exp-loom/hands-on
cargo test --release --offline                                  # tests/mini.rs、tests/spsc_std.rs
RUSTFLAGS="--cfg loom" CARGO_TARGET_DIR=target/loom \
  cargo test --release --offline -- --nocapture --test-threads=1 # tests/vs_loom.rs、tests/spsc_loom.rs
# 反向验证，各用一个 feature、各一个 target 目录
cargo test --release --offline --features broken_acquire --test mini
cargo test --release --offline --features broken_backtrack --test mini
RUSTFLAGS="--cfg loom" cargo test --release --offline --features broken_pop --test spsc_loom
RUSTFLAGS="--cfg loom" cargo test --release --offline --features broken_push --test spsc_loom

和 loom 的关系

最小检查器刻意省掉了 loom 最难的三样：协程（所以线程只能写成步骤列表，真实的 Rust 代码放不进去）、DPOR 与抢占上限（所以交错数是全排列）、弱内存（所以 load 永远读最新的写）。它保留的是 loom 的骨架：一轮一轮从头执行、只记分支选择、从末尾往前回溯、用向量时钟而不是「恰好交错到一起」来判竞争。两个模型的交错数对照见第 1 页，正好能看出 DPOR 去掉了什么、loom 的分支点又比步骤列表多了什么。

SPSC 那一页的重点不是队列本身，而是 06 用法与调试里那几条在一个真实的小库上是什么样子：切换层怎么写、API 差别落在哪、模型多大、反向验证怎么做。它也和 parking_lot 卷的动手形成对照：那里的代码用真实原子和系统调用，loom 帮不上，只能压测；这里的代码全部走切换层，loom 第 1 个交错就抓到的错误，压测 300 次只抓到 6 次或一次也抓不到。

动手

怎么跑

和 loom 的关系

💬 关联讨论

登录