一次 model 的一生

主线位置：主线 1 全程。loom::model(f) → Builder::check → 每轮 Scheduler::run 跑一遍闭包，每个 loom 操作前 branch → Execution::schedule（DPOR、选线程）→ Path 记录或重放 → 一轮结束 step 找下一条路径。本页用一个 6 个交错的小模型把这条链从头走到尾，每一步的细节链到 02 运行时与调度。

sequenceDiagram
  participant C as check 主循环
  participant S as Scheduler
  participant T0 as 0 号线程（闭包）
  participant T1 as 1 号线程
  participant E as Execution::schedule
  participant P as Path
  C->>S: run(execution, f)
  S->>T0: tick → resume
  T0->>E: branch（Arc clone、load flag…）
  E->>P: branch_thread：走到头就新建 Schedule，默认 0 号接着跑
  T0->>E: join：阻塞
  E->>P: 新建 Schedule，换 1 号
  E-->>T0: switch
  S->>T1: tick → resume
  T1->>E: branch（store flag）
  E->>P: backtrack(位置 2, 1 号)：那里的 1 号 Skip → Pending
  T1->>E: 线程结束 → 换回 0 号
  S->>T0: tick → resume，跑完
  C->>C: check_for_leaks
  C->>P: step：从末尾往前，位置 2 的 Pending → Active，截掉之后的分支
  C->>S: 下一轮 run，重放前 3 个分支，第 3 个分支选 1 号

模型

exp-loom/runtime/tests/mp_trace.rs（实验 E1 的第一组）：

loom::model(move || {
  let data = Arc::new(UnsafeCell::new(0usize));
  let flag = Arc::new(AtomicBool::new(false));
  let (d2, f2) = (data.clone(), flag.clone());
  let th = thread::spawn(move || {
    d2.with_mut(|p| unsafe { *p = 42 });
    f2.store(true, Release);
  });
  let seen = flag.load(Acquire);
  if seen {
    let v = data.with(|p| unsafe { *p });
    assert_eq!(v, 42);
  }
  th.join().unwrap();
});

Arc、AtomicBool、UnsafeCell、thread 都是 loom 的。1 号线程写数据再 Release 置 flag；0 号线程 Acquire 读 flag，读到 true 再读数据。这是正确的消息传递，loom 跑完 6 个交错，全部通过，最后打印「Completed in 6 iterations」。

哪些操作会产生调度分支（Execution 与对象仓库）：

线程	操作	分支？
0	`data.clone()`、`flag.clone()`：`Arc` 的 `RefInc`	各一个 `Schedule`
0	`thread::spawn`	不是分支，只登记 1 号线程（协程调度器）
0	`flag.load(Acquire)`	一个 `Schedule` + 一个 `Load`
0	`data.with(...)`	不是分支，只做竞争检查
0	`th.join()`：等 1 号线程结束时的 `Notify`	一个 `Schedule`（等不到就阻塞）
0	闭包结束 drop `flag`、`data`：两次 `RefDec`；线程结束	各一个 `Schedule`
1	`d2.with_mut(...)`	不是分支
1	`f2.store(true, Release)`	一个 `Schedule`
1	drop `d2`、`f2`；线程结束时 `notify` join 句柄；线程结束	各一个 `Schedule`

加起来每轮 13 个分支：12 个 Schedule、1 个 Load。

怎么看到每一轮

两种办法，结果一致：

原版 loom + 日志：LOOM_LOG=trace，再加 LOOM_CHECKPOINT_INTERVAL=1 和一个 LOOM_CHECKPOINT_FILE。间隔为 1 时每轮开头都打「Iteration N」横幅、都写一次 checkpoint，闭包开头读出这个文件，就得到「这一轮要重放的前缀」。trace 日志在 6 轮里共 295 行 TRACE / INFO，每轮 44–48 行，线程切换的「~~~~~~~~ THREAD n ~~~~~~~~」依次是 2、2、2、4、4、4 次。
只加了打印的副本（exp-loom/pathdump/，见 02 部分的实验表）：每轮结束时把完整的 Path 打成 JSON，schedule() 开头打一行「位置、当前线程、它挂着的操作」，backtrack 前打一行。下面的表都来自它，再和上一种的前缀、切换次数逐轮对过。

第 1 轮：每个线程尽量跑到底

路径上的 13 个分支（状态是这一轮结束时的；A = Active、S = Skip、P = Pending、D = Disabled、V = Visited，两个字母依次是 0 号、1 号线程）：

位置	谁在登记什么	分支	说明
0	0 号：clone `data` 的 `Arc`	`Schedule [A D]`	1 号还不存在
1	0 号：clone `flag` 的 `Arc`	`Schedule [A D]`	之后 spawn，1 号登记为可运行
2	0 号：load flag	`Schedule [A P]`	默认 0 号接着跑；1 号本来是 `S`，位置 5 时被 DPOR 改成 `P`
3	（load 本身）	`Load [写 0]`	flag 只有初值一次写，1 个候选：`false`
4	0 号：join	`Schedule [D A]`	1 号还没 notify，0 号阻塞，换 1 号
5	1 号：store flag	`Schedule [D A]`	回溯：flag 上次被 0 号在位置 2 访问，二者无先后，`backtrack(2, 1 号)`
6、7	1 号：drop 两个 `Arc`	`Schedule [D A]` ×2
8	1 号：notify join 句柄	`Schedule [D A]`
9	1 号结束	`Schedule [A D]`	也登记了一次 `backtrack(8, 0 号)`，但 0 号在位置 8 是 `D`，那里也没有 `S`，无效
10、11	0 号：drop 两个 `Arc`	`Schedule [A D]` ×2
12	0 号结束	`Schedule [D D]`	全部结束

0 号线程读到 false，不读数据。step 从位置 12 往前找：位置 12–4 都没有 P，位置 3 的 Load 只有 1 个候选，到位置 2 找到 P：0 号改 V、1 号改 A，截掉 3 以后的全部记录。

6 轮一览

轮	和上一轮从哪里开始不同	这一轮的执行顺序	load 的候选	flag 读到	抢占数	结束后 `step` 回退到
1	—	0 号 clone、clone、load、join 阻塞 → 1 号 store、drop、drop、notify、结束 → 0 号 drop、drop、结束	`false`	`false`	0	位置 2：1 号 `P → A`
2	位置 2 选 1 号	0 号 clone、clone → 1 号 store、drop、drop、notify、结束 → 0 号 load、join、drop、drop、结束	`false`、`true`（位置 8）	`false`	1	位置 8：`Load` 换第 2 个候选
3	位置 8 读第 2 个候选	同第 2 轮	同上	`true`，读数据得 42	1	位置 6：0 号 `P → A`
4	位置 6 选 0 号	0 号 clone、clone → 1 号 store、drop、drop → 0 号 load、join 阻塞 → 1 号 notify、结束 → 0 号 drop、drop、结束	`false`、`true`（位置 7）	`false`	2	位置 7：`Load` 换第 2 个候选
5	位置 7 读第 2 个候选	同第 4 轮	同上	`true`，读数据得 42	2	位置 3：0 号 `P → A`
6	位置 3 选 0 号	0 号 clone、clone → 1 号（写数据，停在 store 前）→ 0 号 load、join 阻塞 → 1 号 store、drop、drop、notify、结束 → 0 号 drop、drop、结束	`false`（位置 4）	`false`	2	找不到，结束

几个 Pending 是在哪里登记的：

第 1 轮位置 2 的 1 号：1 号的 store 和 0 号的 load 冲突（上一节）。
第 2 轮位置 3 的 0 号：1 号在位置 3 store 之后，0 号挂着的 load 每次调度都和这次 store 比一次，没有先后，登记 backtrack(3, 0 号)（打印里连续 4 次，同一个位置，效果相同）。
第 2 轮位置 6 的 0 号：0 号的 join（等 Notify）和 1 号在位置 6 的 notify 冲突。那时 0 号能跑（它的 load 还挂着，没有阻塞），所以只标 0 号。

这些 Pending 被消费的顺序就是深度优先：先消费最深的（第 2 轮登记在位置 6 的，第 4 轮用掉），再消费浅的（位置 3 的，第 6 轮用掉）。每个 Load 的第二个候选总是紧接着下一轮就用掉。

6 个交错从哪来

按「0 号的 load 落在 1 号线程的哪一段」分：

0 号的 load 在	候选	交错数	是哪几轮
1 号 store 之前	只有初值 `false`	1 + 1	第 1 轮（1 号还没开始）、第 6 轮（1 号已写了数据、停在 store 之前）
1 号 store 之后、notify 之前	`false`、`true`	2	第 4、5 轮
1 号全部结束之后	`false`、`true`	2	第 2、3 轮

共 6 个。后两类里读到 false 的那一轮（第 2、4 轮）说明：即使 store 已经发生，Acquire load 仍然可以读到旧值，因为 0 号线程和那次 store 之间没有任何 happens-before；loom 把它作为一个合法的候选列出来。为什么是这两个候选、为什么读到 true 之后数据一定是 42，是一次 load 的候选的内容。

第 1 轮和第 6 轮在 load 与 store 的先后上相同，区别是第 6 轮里 1 号线程先跑了一段：它的 with_mut 不是调度点，所以「写数据」这一步在 loom 看来没有单独的位置，1 号从开始一直跑到 store 前的那个分支，才在位置 3 被换下。

换成 Relaxed

同一个模型把 flag 的写和读都换成 Relaxed（E1 的另一组，exp-loom/runtime/tests/mp.rs）：

flag 的写 / 读	结果
`Release` / `Acquire`	6 个交错，通过
`Relaxed` / `Relaxed`	第 3 个交错 panic：「Causality violation: Concurrent read and write accesses.」
`Release` / `Relaxed`	同上
数据改用 `AtomicUsize`（`Relaxed` 读写），flag `SeqCst` / `SeqCst`	6 个交错，通过
数据改用 `AtomicUsize`，flag `Relaxed` / `Relaxed`	第 3 个交错 `assert_eq!` 失败：读到 0

第 3 个交错就是上表的第 3 轮：0 号读到 flag 为 true，接着读数据。flag 是 Relaxed 时，读到 true 不会把 1 号线程的时钟并进来，1 号写数据（with_mut）在 0 号看来和自己的读没有先后，UnsafeCell 的检查当场报错（UnsafeCell 与原子的非同步访问）。数据换成原子时没有竞争可报，但 load 会多出一个「读到初值 0」的候选，第 3 个交错正好选它。这个过程在一次 load 的候选里逐步展开。

把错误抓到在第 3 个交错，靠的是第 1 轮在位置 2 登记的那个回溯；如果设 LOOM_MAX_PREEMPTIONS=0，这条回溯会被拒绝（它需要一次抢占），整个模型只跑 1 轮，Relaxed 版本也会通过（抢占上限与剪枝）。

小结

一轮 = 从头跑一遍闭包；每个 loom 的同步操作前一个 Schedule，每次原子 load 再加一个 Load。这个模型每轮 13 个分支。
第 1 轮按「尽量不抢占」跑：每个线程跑到阻塞或结束才换人；DPOR 在冲突的访问之间登记 Pending。
step 深度优先：从末尾往前，Load 换下一个候选，Schedule 把下一个 Pending 变成 Active，截掉之后的记录。
6 个交错 = load 在 store 之前（2 轮，各 1 个候选）+ store 之后 notify 之前（2 个候选）+ 1 号结束之后（2 个候选）；抢占数依次是 0、1、1、2、2、2。
用 LOOM_LOG=trace 加 LOOM_CHECKPOINT_INTERVAL=1 可以逐轮看到前缀和线程切换；本页的表与只加打印的副本逐轮核对一致。