「loom 通过」意味着什么
主线位置:主线 4「横线:loom 看到什么、看不到什么」的收尾。前面各章在遇到限制时分别标了方向,这一章按「一次通过到底覆盖了什么」把它们排成四层。
flowchart TB code["被测程序的全部并发行为"] --> l1["① 只有换成 loom 类型的操作:std 类型、系统调用、FFI、没走切换层的依赖都看不见"] l1 --> l2["② 只有这个模型写出来的线程、操作、初始状态"] l2 --> l3["③ 只在给定的探索边界内:抢占上限、max_branches、max_permutations / max_duration、最多 5 个线程"] l3 --> l4["④ 只按 loom 的内存模型:SeqCst 访问 = AcqRel、不做 LB、每个原子 7 次写、CAS weak 不伪失败"] l4 --> pass["在这个交集里没有找到失败的交错 = 通过"]
① 只看得到 loom 类型
loom 不插桩、不解释执行,它看到的只有对它自己的类型的调用。文档「Intrusive Implementation」一节(lib.rs:253-269):
Any code that does not use loom's replacement types is invisible to loom, and thus won't be subject to the loom model's permutation.
Note that loom still works if some concurrent operations are hidden from it (for example, if you use
std::sync::Arcinstead ofloom::sync::Arc). It just means that loom won't be able to reason about the interaction between those operations and the other concurrent operations in your program, and thus certain executions that are possible in the real world won't be modeled.
看不见的东西:
| 看不见的 | 本站的实例 |
|---|---|
std 的原子、Arc、锁 | E8:mem::forget(std::sync::Arc) 通过,换成 loom Arc 报「Arc leaked.」(泄漏检测) |
| 没有走切换层的依赖 | tokio、bytes 只在 cfg(all(test, loom)) 下切换,下游开 --cfg loom 时它们内部仍是 std(cfg(loom) 切换层);crossbeam 的 deque、channel、queue 不走切换层,loom 查不到(怎么验证并发代码) |
| 用真实原子和系统调用实现的库 | parking_lot_core 不能放进 loom 模型,parking_lot 卷的信号量只能靠压测和反向验证(用 parking_lot_core 写信号量) |
| 线程池类库 | rayon-core 源码里没有任何 cfg(loom),没有 loom 测试 |
| 时间、超时、系统调用 | Condvar::wait_timeout 不超时、recv_timeout 是桩(Condvar、Notify 与 park);I/O、信号、FFI 只能在切换层里 mock |
看不见不等于出错:std 类型上的操作照常执行,只是不产生分支、不参与 happens-before 的计算、不做竞争检查。本卷实验用 std 的 Mutex<BTreeSet> 在模型外收集结果,就是利用这一点(写一个好模型)。
② 只检查这个模型的形状
loom 检查的是 loom::model 闭包这一段程序,不是被测库的全部用法。线程数、每个线程调哪几个方法、以什么顺序、初始状态是什么,都由写模型的人决定。
crossbeam 卷 最小 EBR 记下了一个具体例子:去掉一道 fence 的版本在某个模型下没有被抓到,原因是那个模型里写者和推进纪元的是同一个线程,fence 两侧的操作恰好在同一线程上,换一个分工的模型才能暴露。结论是「一个改动没被抓到不等于它安全」,反向验证的结论依赖模型的形状。
再加上 05 部分的几个例子:
Condvar的if写法 loom 通过,换成Notify第 5 个交错就被抓到(E9):同样的形状,等待原语的建模不同,结论就不同。RwLock的写者饥饿:loom 的读写锁没有写者优先,模型里永远不会出现「写者排队挡住新读者」这个状态(Mutex 与 RwLock)。
③ 只在给定的边界内
每一项边界都是运行参数或常量,跑测试时可以知道自己用了什么:
| 边界 | 出处 | 作用 |
|---|---|---|
抢占上限 LOOM_MAX_PREEMPTIONS | Builder.preemption_bound,默认不设 | 设了以后,抢占次数超过上限的交错不探索(抢占上限与剪枝) |
LOOM_MAX_BRANCHES | 默认 1000 | 一轮的分支数达到上限就 panic「Model exceeded maximum number of branches…」;这是报错,不会静默截断 |
LOOM_MAX_PERMUTATIONS、LOOM_MAX_DURATION | 默认不设 | 达到后提前结束并报告通过;只在每 LOOM_CHECKPOINT_INTERVAL 轮检查一次,E4:上限设 10,默认间隔下照样跑满 3 160 轮,间隔改成 100 后停在第 99 轮(model 与 Builder) |
| 线程数 | MAX_THREADS = 5,含主线程 | 超过就断言失败(E12) |
skip_branch / stop_exploring | 模型代码里的调用 | 被标记的分支不探索(E17) |
| 残留的 checkpoint 文件 | LOOM_CHECKPOINT_FILE 指向的文件存在 | 从文件里的路径开始,之前的不再跑;一个通过的模型留下的文件让重跑 1 轮就「通过」(checkpoint、日志与位置) |
最后两行容易被忽视:max_permutations / max_duration 到点就当作通过返回,残留文件让探索从中途开始,两者都不会在输出里提醒。
④ 只按 loom 的内存模型
loom 实现的是 C11 内存模型的一个子集。逐条见 SeqCst 与 load buffering 和 03 内存模型:
- SeqCst 访问当作 AcqRel(假阳性,E5)。
- 不做 load buffering(假阴性,E5);Relaxed RMW 也按「读最新」执行。
- 每个原子只保留最近 7 次写,更早的写不再是任何 load 的候选(E6,写历史与 coherence)。
compare_exchange_weak不伪失败(E16,RMW 与释放序列)。- 没有
compiler_fence。
和其他工具怎么配合
下表只写本站已有实测或代码出处的内容。
| 工具 | 本站的证据 | 补 loom 的哪一层 |
|---|---|---|
| 压力测试 + 反向验证 | parking_lot 卷的信号量、crossbeam 卷的多个实验:真实线程、真实原子,故意改错一处必须失败 | ①:std 类型、系统调用、真实依赖都在里面;但只能看到「跑到了」的交错 |
| 不同内存模型的硬件 | crossbeam 的 CI 在 armv7、powerpc64le 等弱内存序平台上跑普通测试(怎么验证并发代码) | ④:真实硬件上的重排;同样依赖「跑到了」 |
| Miri、ThreadSanitizer | crossbeam 的 CI 对 deque、channel 等 loom 不覆盖的 crate 跑 Miri 与三种 sanitizer(同上页) | ①:不需要切换层,直接看被测代码 |
loom 的长处在 ② ③ 的交集里:给定形状和边界,按 DPOR 系统地枚举调度与读值的选择,失败可以确定地重放。另外几种工具的长处是不需要改代码、看得到真实环境。两边的覆盖面不同,结论也不能互相替代。
小结
- 一次通过 = 在「loom 类型可见的操作 × 这个模型的形状 × 给定的探索边界 × loom 的内存模型」这个交集里,没有找到失败的交错。
- ①:std 类型、没走切换层的依赖、真实原子实现的库、时间与系统调用都看不见;看不见的操作照常执行但不参与检查。
- ②:模型形状决定能暴露什么;crossbeam 卷「没被抓到」的例子、
Condvar与Notify的对照都是形状或建模的问题。 - ③:抢占上限、分支上限、
max_permutations/max_duration(整 interval 才检查,E4)、5 个线程、skip_branch、残留 checkpoint 文件;其中提前结束和残留文件都不会提醒。 - ④:SeqCst 访问降级、不做 LB、7 次写窗口、CAS weak 不伪失败、没有
compiler_fence。 - 压力测试、弱内存序硬件、Miri 与 TSan 补 ① 和 ④;loom 补「系统地枚举、可确定重放」。