全景

这一部分先回答「loom 是什么、和其他办法差在哪」，再用同一个两线程的消息传递模型把两条主线从头到尾走一遍。每一步只写到「调用了哪个函数、路径上多了什么分支、哪个值被排除」，细节留给后面的部分，每一步都链过去。

1. loom 解决什么问题：罕见交错与弱内存序两类难题；确定性重放加系统枚举；和压力测试、Miri、TSan 的对照；CDSChecker 出处；本站里谁在用。
2. 一次 model 的一生：消息传递模型 6 个交错，逐轮列出 13 个分支的状态、DPOR 在哪里登记回溯、step 回退到哪；6 个交错从哪来；换成 Relaxed 后第 3 个交错报错。
3. 一次 load 的候选：一次 Relaxed load 怎样经过调度点、算候选、选一个写、做 coherence 与同步；那一刻的写历史；每个原子只留 7 次写。

flowchart LR
  why[loom 解决什么问题] --> model["一次 model 的一生：Schedule 分支、DPOR、step"]
  why --> load["一次 load 的候选：Load 分支、coherence、Acquire"]
  model -->|"第 2、3 轮的 Load 分支"| load

两条主线在同一个模型里交汇：一次 model 的一生 的 6 个交错里有 4 个来自「0 号线程读 flag 时有两个候选」，这两个候选怎么算出来，是 一次 load 的候选 的内容。主线 3（数据竞争怎样被抓到）在第 2 页「换成 Relaxed」一节露一面，全程在 04 检测器；主线 4（看到什么、看不到什么）在第 1 页给出轮廓，汇总在 07 能力边界。