Reached unexpected exploration state. Is the model fully deterministic?

主线位置：主线 1 的「重放」那一步。loom 每轮从头执行闭包，前缀按 Path 里的记录选（Path：路径与深度优先）；记录只有「第几个分支点选了什么」，前提是同样的选择得到同样的执行。

flowchart TB
  src["行为依赖 loom 看不见的东西：std static、HashMap 顺序、时间、随机数"] --> div["第 k 轮重放时走了另一条路"]
  div --> kind{"第 pos 个分支点的类型"}
  kind -->|"和记录不同（Schedule 对 Load）"| e1["Is the model fully deterministic?（path.rs 三处 expect）"]
  kind -->|"相同，但读值、写历史不同"| e2["可能撞上 assertion left != right（atomic.rs 752 / 805）"]
  kind -->|"相同，结果也碰巧一致"| e3["不报错，探索的不是你以为的交错"]

现象

前几轮就失败，消息是下面两种之一：

Reached unexpected exploration state. Is the model fully deterministic?

assertion `left != right` failed
  left: VersionVec { versions: [7, 0, 0, 0, 0] }
 right: VersionVec { versions: [7, 0, 0, 0, 0] }

第二种出自 loom 内部（rt/atomic.rs:752 或 805），看起来像 loom 自己的 bug，其实是同一个问题。

最小复现

exp-loom/pitfalls/tests/pit.rs，主线程与一个子线程，共享一个 loom 原子：

02 Path 的实验是第一行的另一个版本（std static 计数器，只在第一轮多一次 load），同样在第一次重放时报错。

源码出处

重放时 branch_load、branch_spurious、branch_thread 把路径上这个位置的分支 downcast 成需要的类型，类型不对就 expect 失败，报第一种消息（211、232、323 行）。第一行的模型在第 1 轮比之后多一次 store，第 2 轮同一个位置上要的分支类型变了。

HashMap 那组里，load 和 fetch_add 在路径上都是「一个调度分支 + 一个 Load 分支」（RMW 也要选读哪次写），所以迭代顺序变了，分支类型照样对得上，第一种检查拦不住。重放时 Load 分支直接用记录里的下标，不重新计算候选；这一轮的写历史和记录时不一样，状态就自相矛盾，到了要新建 Load 分支、比较写的修改顺序时，撞上两个写的 modification_order 相等的断言。atomic.rs:751 那条断言旁边就有一行注释「TODO: this sometimes fails」（load 的候选）。推测：这条注释说的情况里，至少有一部分就是不确定的模型。

还有第三种情况，不报任何错：类型对得上、状态也没自相矛盾，loom 只是没有按你以为的顺序探索。这一种只能靠写模型时排除不确定来源。

常见来源

• std 的 HashMap / HashSet 迭代顺序：每个 RandomState 的种子不同，同一进程里每轮新建的 map 顺序也不同。上面实测每次运行失败在哪一轮都不一样。
• 被测代码里没走切换层的全局状态：std 的 static 原子、OnceLock、Once，上一轮改过，这一轮走了另一条路。
• 时间、随机数、CPU 数、环境变量。tokio 的切换层把随机种子固定为 1、CPU 数固定为 2（cfg(loom) 切换层）。

怎么改

• 模型里用 BTreeMap / Vec，或给 HashMap 一个固定的 hasher。
• 被测代码里的一次性初始化在 loom 下换成 loom::lazy_static!（每轮重新初始化）；计数器之类的 std static 要么换成 loom 类型，要么确认它不影响控制流。
• 看到 atomic.rs:752 / 805 的 left != right，先按不确定的模型排查，再怀疑 loom。
• 统计用的 std 容器（本卷实验收集结果集的写法）只写不读，不能用来决定模型里走哪条分支（写一个好模型）。

小结

• 重放只记选择，要求同样的选择得到同样的执行；行为依赖 std 静态量、HashMap 顺序、时间时就会走偏。
• 分支类型对不上：「Is the model fully deterministic?」（path.rs 三处）；对得上、内容对不上：可能是 atomic.rs:752 / 805 的「assertion left != right failed」。
• 实测：std 一次性初始化标志在第一次重放时报第一种；HashMap 迭代顺序 12 次运行都报第二种，失败轮次 2–6 不等；换 BTreeMap 279 个交错通过。