SeqCst 与 load buffering

主线位置：主线 2「一次 load 能读到什么」的边界。03 内存模型 讲了 loom 怎么算候选写；这一章用 litmus 测试把「loom 给出的结果集」和「C11 允许的结果集」并排放，看两者在哪里不一致、往哪个方向不一致。

flowchart LR
  subgraph sb["SB：store buffering"]
    t1["T1：x = 1；r1 = y"]
    t2["T2：y = 1；r2 = x"]
  end
  subgraph lb["LB：load buffering"]
    u1["T1：r1 = y；x = 1"]
    u2["T2：r2 = x；y = 1"]
  end
  sb -->|"SeqCst 访问：C11 禁止 (0,0)，loom 给出 (0,0)"| fp["假阳性"]
  lb -->|"Relaxed：C11 允许 (1,1)，loom 从不给出"| fn["假阴性"]

两个方向

上游 README 的「Unsupported features」一节只有两条，正好一个方向一条：

• SeqCst 访问（load、store 等）被当作 AcqRel：同步变弱，会产生「false alarms」。fence(SeqCst) 是支持的。
• load buffering：C11 允许的某些执行 loom 不探索，「there can be a bug in the checked code even if Loom says there is no bug」，见 tests/litmus.rs 里的 load_buffering。

上游自己的测试印证了第二条：tests/litmus.rs:10-35 的 load_buffering 断言结果集里包含 1，带着 #[ignore] 和注释「Loom currently does not support load buffering.」。

实验 E5：四种 SB、一种 LB、一种 CoRR

（exp-loom/survey/tests/litmus.rs）主线程与一个子线程，两个 loom AtomicUsize 初值 0。每一轮把 (r1, r2) 插进模型外的一个 std BTreeSet，跑完打印集合。交错数是确定的。

逐行读：

• 前两行正确：Release / Acquire 不约束「先写后读不同变量」的顺序，(0,0) 是合法结果，真实的 ARM 和 x86 都能观察到。
• 第三行是假阳性：所有访问都是 SeqCst 时，C11 要求存在一个所有 SeqCst 操作的全序，两个读不可能都排在对方的写之前。loom 照样给出 (0,0)，交错数也和 Relaxed 一样是 30，说明 SeqCst 访问在 loom 里没有比 AcqRel 多任何约束。
• 第四行：同样的 SB 换成 Relaxed 访问加 fence(SeqCst)，(0,0) 消失，交错数减半（15）。loom 0.7.2 实现了 SeqCst fence 的语义，crossbeam 卷 Chase-Lev 的 E5 依赖的正是这一点。
• 第五行是假阴性：LB 里两个线程都是「先读后写」，C11 允许两个读都读到对方「之后」的写，得到 (1,1)。loom 永远给不出。
• 第六行是对照：同一线程对同一变量的两次读不会倒序（coherence），loom 给出的恰好是 C11 允许的六种。loom 没有乱给结果，问题只出在上面两处。

为什么 SeqCst 访问被降级

rt/thread.rs:336-341：

pub(crate) fn seq_cst(&mut self) {
    // The previous implementation of sequential consistency was incorrect (though it's correct
    // for `fence(SeqCst)`-only scenario; use `seq_cst_fence` for `fence(SeqCst)`).
    // As a quick fix, just disable it. This may fail to model correct code,
    // but will not silently allow bugs.
}

Synchronize::sync_load / sync_store 遇到 SeqCst 时先按 Acquire / Release 同步，再调这个空函数（rt/synchronize.rs:23-54），所以 SeqCst 访问 = AcqRel。fence(SeqCst) 走另一个函数 seq_cst_fence，把当前线程的时钟与一个全局 seq_cst_causality 双向合并（343-349 行）。

历史：「As a quick fix, just disable it」来自 fd8680c（「Relax how SeqCst is modelled」，#108，2020-02）；seq_cst_fence 与括号里那句来自 ffb2672（「Implement Release, AcqRel, and SeqCst fences」，#220，2021-09，0.5.2）。在 #220 之前，rt::fence 只接受 Acquire，其他序直接断言失败「only Acquire fences are currently supported」。逐条规则见 fence 与 SeqCst。

注释里的取舍说得很清楚：宁可误报正确代码，也不放过错误。这个方向的代价落在用户身上：

• 用 SeqCst 访问实现的正确算法（Dekker、Peterson 式的互斥，「我先举手、再看对方有没有举手」）在 loom 下会失败。
• 绕法一：改成 Relaxed（或 Release / Acquire）访问加 fence(SeqCst)，这是 loom 能正确建模的形式，在 C11 里也成立。第四行就是这个改写。
• 绕法二：确认失败交错正是 SB 型的 (0,0)，判定为 loom 的限制，不在 loom 下测这一段。
• Mutex::new、Notify 构造时的 seq_cst 参数、RwLock 里四处 execution.threads.seq_cst() 也因此都是空操作，锁只提供 acquire / release（Mutex 与 RwLock）。

为什么 LB 的 (1,1) 不出现

loom 自己的解释在 crate 文档「Relaxed Memory Ordering」一节（lib.rs:294-320）：

Unfortunately, it is not possible for loom to completely model all the interleavings that relaxed memory ordering allows. This is because the relaxed memory ordering allows memory operations to be re-ordered within a single thread -- B can run before A -- which loom cannot emulate.

loom 按程序顺序一个操作一个操作地执行。一次 load 的候选只能是「已经执行过的写」（load 的候选）。LB 要得到 (1,1)，T1 的读必须读到 T2 的写，而 T2 的写在 T2 的读之后；T2 的读又要读到 T1 的写，T1 的写在 T1 的读之后。两个读都执行时，对方的写都还没执行，不可能是候选。CDSChecker 用「推测性地读一个将来的写，之后再验证」处理这种情况，loom 没有实现这一部分。

LB 型的错误在实际代码里少见：要有两个线程各自「读一个变量、再写另一个变量」，且正确性依赖于「不可能读到对方稍后的写」。但这类代码确实存在，loom 通过不能作为它们正确的证据。

同样的原因：Relaxed RMW 的 SB

把 SB 里的两个 load 换成 fetch_add(0, ord)（tokio #1788 那种「用 RMW 读最新值」的写法）。实测（exp-loom/primitives/tests/sb_rmw.rs）：

loom 里 RMW 只从「修改顺序上没有更新写」的写里选（RMW 与释放序列），而且仍然按程序顺序执行：一个线程的 RMW 执行时，如果对方的 store 已经执行过，就一定读到它。两个 RMW 不可能都读到 0。

• SeqCst 那一行与 C11 一致：全序禁止 (0,0)。
• Relaxed 那一行与 C11 不一致：两个线程之间没有任何 happens-before，C11 允许每个 RMW 在各自变量的修改顺序上排在对方的 store 之前，(0,0) 是合法结果。loom 不给出它，和 LB 是同一类原因，方向是假阴性。

所以在 loom 里，fetch_add(0) 不论用什么序，都表现得像「读到最新值」；用它补「SeqCst load 不够」的问题时，loom 只能验证 SeqCst 的版本，换成更弱的序 loom 也会通过。

实际影响

小结

• SB：Relaxed、Rel/Acq、SeqCst 访问三种写法 loom 都给出四种结果、各 30 个交错；只有 Relaxed + fence(SeqCst) 去掉了 (0,0)，15 个交错。SeqCst 访问那一行是假阳性。
• 原因：seq_cst() 是空函数（fd8680c #108 关掉，ffb2672 #220 另加了 seq_cst_fence），SeqCst 访问 = AcqRel；SeqCst fence 是真的。
• LB：Relaxed 下只给出三种结果、永远没有 (1,1)，15 个交错，假阴性；上游 tests/litmus.rs 里对应的测试是 #[ignore]。原因是 loom 按程序顺序执行，load 只能读已经执行的写。
• 同一原因下，Relaxed RMW 版的 SB 也不出现 (0,0)（10 个交错），C11 允许它；SeqCst 版本与 C11 一致。
• CoRR 的六种结果与 C11 完全一致，说明 loom 在它建模的范围内给出的候选是对的。