用 SeqCst 写的正确算法，loom 报断言失败

主线位置：主线 2「一次 load 能读到什么」的边界。SeqCst 访问在 loom 里只做 Acquire / Release 同步，没有全序（fence 与 SeqCst）。

sequenceDiagram
  participant A as 线程 A
  participant X as x / y
  participant B as 线程 B
  A->>X: x.store(1, SeqCst)
  B->>X: y.store(1, SeqCst)
  A->>X: y.load(SeqCst) 读到 0
  B->>X: x.load(SeqCst) 读到 0
  Note over A,B: C11 禁止两个都读到 0；loom 给出这个结果，于是「两边都进了临界区」

现象

一段只用 SeqCst 原子访问实现的互斥或握手（「我先把自己的标志置 1，再看对方的标志；对方没置就进去」），在 C11 下是对的，loom 却报两边同时进入临界区、或者某个「不可能」的断言失败。

最小复现

E5（SeqCst 与 load buffering，exp-loom/survey/tests/litmus.rs）：SB，两个线程各写自己的变量再读对方的，收集 (r1, r2)。

第一行就是误报：(0,0) 是 C11 禁止的结果，loom 给出了。第二行是改写之后：同一个算法用 fence 表达，loom 与 C11 一致。

源码出处

rt/thread.rs:336-341：seq_cst() 是空函数，注释写着旧实现不对，「As a quick fix, just disable it. This may fail to model correct code, but will not silently allow bugs」。SeqCst load / store 先按 Acquire / Release 同步，再调这个空函数，所以等于 AcqRel。fence(SeqCst) 走另一个函数 seq_cst_fence，与全局时钟双向合并，是真的（343-349 行）。README 的「Unsupported features」把这一条列在第一位。

怎么改

• 改写成 fence 形式：访问用 Relaxed（或 Release / Acquire），在「写自己的标志」和「读对方的标志」之间插一道 fence(SeqCst)。这在 C11 里同样成立，loom 能正确建模。crossbeam 的 Chase-Lev 就是这个形式（crossbeam 卷 Chase-Lev）。
• 或者确认后排除：用 checkpoint 把失败那一轮存下来、开 LOOM_LOG 重放（checkpoint、日志与位置），确认失败的交错正是 SB 型「两个 load 都读到了对方写之前的值」，再判定为 loom 的限制，这一段不在 loom 下测。
• 方向：这一条限制只会让 loom 多报，不会少报。SeqCst 访问的版本在 loom 里通过时，这条限制不影响结论（其他限制照旧，见 07 能力边界）。反方向要小心的是 fetch_add(0) 写法：Relaxed 版本在 loom 里也通过，但 C11 不保证（SeqCst 与 load buffering）。
• 锁不受影响：Mutex、RwLock 只需要 acquire / release，loom 里 Mutex::new 传的 seq_cst = true 本来就是空操作（Mutex 与 RwLock）。

小结

• loom 0.7.2 的 SeqCst 访问 = AcqRel：seq_cst() 是空函数，只有 fence(SeqCst) 做全局同步。
• E5：全 SeqCst 的 SB 30 个交错给出 (0,0)，C11 不允许，这是假阳性；Relaxed 加 fence(SeqCst) 15 个交错，(0,0) 消失。
• 改法：写成 fence 形式；或确认失败交错是 SB 型后排除。