能力边界
前面各章在遇到 loom 与真实语义不一致的地方都标了方向。这一部分把它们放在一起。两个方向的含义：
- 假阳性：loom 报错，代码在真实环境里没问题。代价是误报和绕路，不会让错误溜过去。
- 假阴性：代码在真实环境里有问题，loom 通过。代价是「通过」的含义变窄，要靠别的手段补。
flowchart LR
subgraph fp["假阳性：loom 报错、代码没问题"]
a1["SeqCst 访问当 AcqRel"]
a2["wait_timeout 不超时"]
a3["子线程 panic 穿出模型"]
a4["RwLock 同线程嵌套读"]
a5["mpsc 断开被报成死锁 / 泄漏"]
end
subgraph fn["假阴性：代码有问题、loom 通过"]
b1["不做 load buffering"]
b2["每个原子只留 7 次写"]
b3["CAS weak 不伪失败"]
b4["Condvar / park 不虚假唤醒"]
b5["RwLock 没有写者优先"]
end
subgraph out["看不见"]
c1["std 类型、系统调用、FFI、没走切换层的依赖"]
end
总表
| 限制 | 方向 | 出处 | 本卷实验 | 怎么绕 |
|---|---|---|---|---|
| SeqCst 访问当作 AcqRel | 假阳性 | rt/thread.rs:336-341；README「Unsupported features」 | E5：SB 全 SeqCst 访问仍给出 (0,0)，30 个交错；改成 fence(SeqCst) 后消失 | 改写成 Relaxed / Rel-Acq 访问 + fence(SeqCst) |
| 不做 load buffering | 假阴性 | lib.rs:294-320；tests/litmus.rs 的 #[ignore] | E5：LB 永远没有 (1,1)；Relaxed RMW 版 SB 没有 (0,0) | 让正确性依赖 Acquire / Release，而不是「读不到将来的写」 |
| 每个原子只保留最近 7 次写 | 假阴性 | MAX_ATOMIC_HISTORY = 7（rt/mod.rs:64-65） | E6：写 9 次后只可能读到 3–9 | 模型里同一原子的写不要超过 7 次 |
compare_exchange_weak 不伪失败 | 假阴性 | sync/atomic/int.rs:94-104 | E16：单线程、无循环的 compare_exchange_weak 通过 | 代码审查：_weak 必须在循环里 |
Condvar、park 不虚假唤醒 | 假阴性 | rt/condvar.rs:39-60、rt/mod.rs:86-114 | E9：if 写法 8 个交错通过；换成 Notify 第 5 个交错被抓到 | 在 loom 下把等待原语换成 Notify |
wait_timeout 永不超时 | 假阳性 | sync/condvar.rs:44-53 | E9：无人通知时报死锁 | 超时分支不放进模型 |
lazy_static! 一轮内可能初始化两次、每轮 drop | 与真实行为不同 | lazy_static.rs:43-67 | E13：初始化里有 yield_now 时执行 2 次，去掉后 1 次 | 初始化函数不要有依赖「只执行一次」的副作用 |
RwLock 没有写者优先 | 假阴性 | rt/rwlock.rs:56-79 | 写者等待时新读者照样进（9 个交错里 3 个） | 写者饥饿、嵌套读死锁要另找手段 |
RwLock 同线程嵌套读报内部错误 | 假阳性 | rt/rwlock.rs:103-106 | E14：「invalid internal loom state」后 abort；不嵌套 9 个交错通过 | 模型里改成不嵌套 |
子线程 panic 穿出模型，join 恒 Ok | 假阳性 | thread.rs:163-170 | E15：模型以子线程 panic 失败；std 下 join 返回 Err | 子线程里自己 catch_unwind |
mpsc 发送方断开后 recv 报死锁、接收方 drop 后 send 报泄漏 | 假阳性 | rt/mpsc.rs:103-133 | 第 1 个交错报「deadlock」/「Messages leaked.」；std 返回 Err | 显式发结束消息 |
| 最多 5 个线程（含主线程） | 限制 | rt/mod.rs:61-62 | E12：spawn 5 个触发断言 | 主线程承担一个角色 |
没有 compiler_fence | 可能假阴性 | sync/atomic/mod.rs:25-28 只导出 fence | — | crossbeam 用 fence 代替（更强） |
Barrier、recv_timeout 是桩；没有 OnceLock、thread::scope、Weak | 不可用 | sync/barrier.rs、sync/mpsc.rs:63-70 | 调用即「not implemented: … is not supported yet in Loom.」 | 不放进模型，或在切换层里 mock |
| 侵入式：只看得到 loom 类型 | 看不见 | lib.rs:253-269 | E8：forget(std::sync::Arc) 通过 | 切换层覆盖到要测的代码；其余靠压测、Miri、TSan |
两章
- SeqCst 与 load buffering：E5 的四种 SB、LB、CoRR 并排对照 C11；
seq_cst()为什么是空函数、历史上两次提交各改了什么；loom 为什么给不出 LB 的 (1,1)；同一原因下 Relaxed RMW 版 SB 也没有 (0,0)。 - 「loom 通过」意味着什么：一次通过覆盖的是四层边界的交集（可见的操作、模型形状、探索边界、内存模型），每层的出处与实测，以及和压力测试、Miri、TSan 怎么分工。
各条限制在哪一章首次出现：内存模型的几条在 03 内存模型，检测器相关的在 04 检测器，原语语义的在 05 同步原语的模型，运行参数相关的在 06 用法与调试。按「报错原文 → 怎么改」组织的版本见 09 常见坑。
💬 关联讨论
发起讨论加载中...