Model exceeded maximum number of branches

主线位置：主线 1 里 Path 的长度检查。每次在路径末尾新建分支都先断言没到上限（死锁、分支上限与位置信息）。上限限制的是一轮的分支数，不是交错总数。

flowchart TB
  e["Model exceeded maximum number of branches"] --> q{"调大 LOOM_MAX_BRANCHES 后"}
  q -->|还是同一轮报错| spin["有循环不会结束：自旋没 yield_now"]
  q -->|通过了| long["模型本身长：一轮里操作太多"]
  spin --> f1["循环里 yield_now / hint::spin_loop"]
  long --> f2["调大上限，或把模型缩短"]

现象

Model exceeded maximum number of branches. This is often caused by an algorithm requiring the processor to make progress, e.g. spin locks.

报错出自 path.rs:109-123 的 assert_path_len!，在 push_load、branch_spurious、branch_thread 三处新建分支前检查。消息只提自旋锁，实际有两种完全不同的来源。

来源一：自旋不让出

E11（死锁、分支上限与位置信息）：两个线程用 CAS 自旋锁保护一个 UnsafeCell。

调度器在当前线程还能跑时尽量不切换（DPOR），第 28 轮里持锁线程永远轮不到，自旋的线程把路径无限拉长；调大上限只是撞得晚一点。yield_now 让调度器优先选别的线程，也让这个线程不再读它让出前读过的旧值（load 的候选），循环才结束。

来源二：模型本身太长

本部分新测（exp-loom/pitfalls/tests/pit.rs 的 long_*，preemption_bound = Some(1)）：主线程对一个原子做 n 次 fetch_add，另一个线程做 1 次，最后断言总数。

每个 fetch_add 在路径上占两个分支：一个调度分支，一个 Load 分支（RMW 也要选读哪次写，rt/atomic.rs 的 rmw 里调 push_load，RMW 与释放序列）。所以 1000 的上限大约是 500 次原子操作。这一种调大上限就能通过，交错数也不会因此爆炸。

n = 1000 那一行报错之后进程 abort（退出码 134）：分支超限发生在主线程刚 spawn 完、还没切换过的时候，排队中的 spawn 闭包里有一个 loom Arc，在调度器状态撤走之后才 drop，第二次 panic。这和分支上限本身无关，见 panic 之后进程 abort。

怎么改

1. 先把 LOOM_MAX_BRANCHES 调大一个量级再跑。还是同一个交错报错，就是来源一；通过了，就是来源二。
2. 来源一：被测代码的每个自旋、重试循环里都要有让出。被测代码本来用 std::hint::spin_loop()，切换层换成 loom::hint::spin_loop() 即可，它在 loom 里就是 yield_now（hint.rs:3-6）。std 的 spin_loop 对 loom 不可见，起不了作用。
3. 来源二：调大上限，或者按 写一个好模型 把模型缩短：容量类常数调小，只把相互竞争的那几步放进模型。

小结

• 上限 1000 管的是一轮里的分支数；报错消息只提自旋锁，实际还有「模型太长」这种来源。
• 不 yield 的自旋：第 28 个交错报错，上限调到 10000 也一样；加 yield_now 后 189 个交错通过（E11）。
• 模型太长：每个 fetch_add 占两个分支，490 次通过、495 次报错；上限改 3000 后 1000 次也通过。
• 先调大上限做区分，再对症处理。