写历史与 coherence

主线位置：主线 2 的数据结构。一次 load 要从「这个原子变量的哪些写」里挑一个读，这一页讲这些写存在哪、怎样排出先后。挑的规则在下一章 load 的候选。

原子变量不存值，存一段历史

loom::sync::atomic::AtomicUsize 只有一个字段，是对象仓库里的下标（02 Execution 与对象仓库）。真正的状态是 rt/atomic.rs:77-127 的 State，字段分两组：

每次写是一个 Store（atomic.rs:141-161）：

struct Store {
    /// The stored value. All atomic types can be converted to `u64`.
    value: u64,

    /// The causality of the thread when it stores the value.
    happens_before: VersionVec,

    /// Tracks the modification order. Order is tracked as a partially-ordered
    /// set.
    modification_order: VersionVec,

    /// Manages causality transfers between threads
    sync: Synchronize,

    /// Tracks when each thread first saw value
    first_seen: FirstSeen,

    /// True when the store was done with `SeqCst` ordering
    seq_cst: bool,
}

• value：所有原子类型都转成 u64 存（rt/num.rs:12-52），整数用 as，bool 存 0 / 1，*mut T 也是 as u64。这是 loom 原子「内存表示和 std 不同」的另一半原因：值根本不在 AtomicUsize 本身里。
• happens_before 与 sync：前者只用于 coherence，后者才传给 acquire 读者，区别见 向量时钟与同步点。
• modification_order：这次写在修改顺序里的位置，下一节。
• first_seen：[u16; MAX_THREADS]，初值全是 u16::MAX；某个线程第一次读到或写出这个值时，把它当时自己的时钟分量记进去（touch，atomic.rs:873-877）。
• seq_cst：只给 SeqCst load 的一条规则用（fence 与 SeqCst）。

first_seen 派生出整套模型里最常用的判断 is_seen_by_current（atomic.rs:879-889）：只要有某个线程 T，first_seen[T] <= 当前线程.causality[T]，就算「当前线程已经看到这次写」。也就是说，不必是当前线程自己读过，只要某个线程读到或写出它的那一步，发生在当前线程之前就算。

环形数组

写入位置是 cnt % 7（atomic.rs:929-931），第 8 次写覆盖第 1 次的槽位。被覆盖的写从模型里彻底消失：它不再是任何 load 的候选，它的修改顺序也不再参与比较。要按时间顺序遍历时用 stores_mut（atomic.rs:821-826）从最老的槽位开始。

State::new 把初值当作一次 Release 写放进第 0 格（atomic.rs:402-433），之前先调一次 track_unsync_mut，表示「之后的所有访问都必须发生在构造之后」。所以初值和其他写一样占一个槽位，也一样会被挤出去。

Execution 里另有一个 max_history: 7 字段，只存不用；起作用的是常量 MAX_ATOMIC_HISTORY（rt/mod.rs:64-65），见 02 Execution 与对象仓库。

修改顺序是一个偏序

C11 要求每个原子变量的所有写有一个全序（modification order），所有线程对它的观察都要一致。loom 不直接维护这个全序，而是给每次写一个向量时钟 modification_order，用 VersionVec 的偏序比较：mo_i < mo_j 表示「i 一定在 j 之前」，不可比表示「还没定」。store 的前半段：

        // The modification order is initialized to the thread's current
        // causality. All reads / writes that happen before this store are
        // ordered before the store.
        let happens_before = threads.active().causality;

        // Starting with the thread's causality covers WRITE-WRITE coherence
        let mut modification_order = happens_before;

        // Apply coherence rules
        for i in 0..self.stores.len() {
            // READ-WRITE coherence
            if self.stores[i].first_seen.is_seen_by_current(threads) {
                let mo = self.stores[i].modification_order;
                modification_order.join(&mo);
            }
        }

新写的位置 = 写者的 causality 并上「写者已经看到的每一次写」的位置。因为 synchronize() 在写之前把写者自己的分量加了一，新写在这个分量上严格大于它之前的一切，所以它排在所有「已看到的写」之后。两个线程互不知情的两次写，各自只在自己的分量上增长，结果不可比：loom 此刻不决定它们的先后。

先后是读的时候才补上的。apply_load_coherence：

    fn apply_load_coherence(&mut self, threads: &mut thread::Set, index: usize) {
        for i in 0..self.stores.len() {
            // Skip if the is current.
            if index == i {
                continue;
            }

            // READ-READ coherence
            if self.stores[i].first_seen.is_seen_by_current(threads) {
                let mo = self.stores[i].modification_order;
                self.stores[index].modification_order.join(&mo);
            }

            // WRITE-READ coherence
            if self.stores[i].happens_before < threads.active().causality {
                let mo = self.stores[i].modification_order;
                self.stores[index].modification_order.join(&mo);
            }
        }
    }

线程读了第 index 次写：凡是它已经看到的写（READ-READ），凡是发生在它之前的写（WRITE-READ），都被并进 index 的位置，也就是被定在 index 之前。之后任何线程再比较这几次写，看到的都是这个更细的偏序。

flowchart LR
  subgraph before["读之前：两次写互不知情，不可比"]
    a1["A（1 号线程）写 1，mo = [0, 3]"]
    b1["B（0 号线程）写 2，mo = [4, 0]"]
  end
  subgraph after["B 写过 2 之后读到 A 写的 1"]
    b2["B 写 2，mo = [4, 0]"]
    a2["A 写 1，mo 并入 [4, 0] 变成 [4, 3]"]
    b2 -->|"mo_2 < mo_1"| a2
  end
  before --> after

（时钟数值是示意，只写前两个分量。）B 读的时候，自己写的 2 已经「被看到」，READ-READ 规则把 2 的位置并进 1，于是 2 排在 1 之前。之后 B 再读 x，2 有了一个更新的、已看到的写压着它，就不再是候选。

规则清单：哪些实现了

文件头按 CDSChecker 论文的图 7、9、10 列了一张清单（atomic.rs:1-55），有说明的只有前四条。对照代码：

清单是 #220（2021-09）加的，规则名照抄论文；空着的条目不等于「完全没有处理」，表里最后一列写了各自的去向。

实验 E6：7 次写的窗口

断言：每个原子变量只保留最近 7 次写；更早的写不再是任何 load 的候选，包括初值。

方法（exp-loom/memory-model/tests/history.rs）：子线程对 x 依次 store(1..=n, Relaxed)，再 flag.store(true, Relaxed)；主线程 flag.load(Relaxed) 读到 true 时 x.load(Relaxed) 一次，用 std 的 Mutex<BTreeSet> 在模型外收集所有轮里读到的值。因为 flag 是 Relaxed，主线程读到 flag 并不意味着「看到」了 x 的任何一次写，所以 x 的每一次写都可以是候选，只受窗口限制。

• 窗口里正好 7 个值：初值加 6 次写时初值还在（n = 6），第 7 次写把初值挤出去（n = 7）。这也是 Path 的 Load 分支最多 7 个候选的原因（02 Path）。
• 对照：同一个模型、n = 9，把 flag 改成 Release / Acquire，6 个交错，读到 flag 之后 x 只可能是 9。主线程 acquire 之后，x 的 9 次写都「已被看到」，只有最新的那次没有更新的写压着它。
• 方向：C11 允许 Relaxed 版本读到 0 … 9 中的任何一个，loom 只给其中 7 个。被挤掉的值在 loom 里永远读不到，依赖「读到很旧的值」才出错的代码，loom 不会报。这一条汇总在 07 能力边界。

cnt 是 u16，记的是写的总次数，用来算下一次写的槽位和遍历范围（atomic.rs:910-927）。

小结

• loom 原子的值不在原子对象里：State 存最近 7 次写，每次写记值（统一为 u64）、写者时钟、修改顺序、同步点、first_seen、是否 SeqCst。
• is_seen_by_current：某个线程读到或写出它的那一步发生在当前线程之前，就算已看到。
• 修改顺序是向量时钟的偏序：写的时候排在所有已看到的写之后，读的时候再把已看到的、发生在之前的写定在被读的写之前。
• CDSChecker 清单的前四条 coherence 规则有实现；SeqCst 相关两条为空；RMW 原子性由 match_rmw_to_stores 实现；SC fence 用全局时钟另行建模。
• E6：连写 7 次后初值不再是候选，n 次写只剩最近 7 个值可读；用 Release / Acquire 时只剩最新值。