一次 load 的候选

主线位置：主线 2 全程。一次 model 的一生 讲的是「哪个线程先跑」，本页讲另一种分支：同一个调度顺序下，一次原子 load「读到哪一次写」。loom 给每个原子保存最近 7 次写，load 时按 coherence 规则排除不可能读到的，剩下的每一个都作为一个分支依次试。细节在 03 内存模型。

flowchart TB
  l["AtomicUsize::load(Relaxed)（sync/atomic/int.rs）"] --> b["rt::Atomic::load：branch(Load) → schedule()（调度点）"]
  b --> sy["synchronize：本线程 causality 自增"]
  sy --> q{"路径走到头？"}
  q -->|是| m["match_load_to_stores：在 stores[0..7] 里排除不可能的写 → push_load(候选)"]
  q -->|否：重放| bl
  m --> bl["branch_load：取 Load 分支当前选中的写下标"]
  bl --> st["State::load：track_load（竞争检查）→ apply_load_coherence → first_seen.touch → sync_load(ordering)"]
  st --> v["返回那次写的值"]

模型与结果

把 一次 model 的一生 的模型改两处：数据从 UnsafeCell 换成 AtomicUsize（这样不会有单元格竞争报错，只看读到的值），flag 的写和读换成 Relaxed（exp-loom/pathdump/tests/oneload.rs，副本只加了打印）：

loom::model(move || {
  let data = Arc::new(AtomicUsize::new(0));
  let flag = Arc::new(AtomicBool::new(false));
  let (d2, f2) = (data.clone(), flag.clone());
  let th = thread::spawn(move || {
    d2.store(42, Relaxed);
    f2.store(true, Relaxed);
  });
  if flag.load(Relaxed) {
    assert_eq!(data.load(Relaxed), 42, "stale data");
  }
  th.join().unwrap();
});

第 3 个交错失败：flag 读到 true，数据读到 0。前 2 个交错和原模型一样，flag 都读到 false。第 3 个交错的调度和 原模型的第 3 轮 相同：1 号线程先跑完（写数据、写 flag、drop、notify、结束），0 号线程再读 flag，Load 分支选第 2 个候选（true），然后读数据。

一步一步

1. 调度点

AtomicUsize::load 经过 sync::atomic::Atomic 一层，到 rt::Atomic::load：

pub(crate) fn load(&self, location: Location, ordering: Ordering) -> T {
    self.branch(Action::Load, location);

    super::synchronize(|execution| {
        let state = self.state.get_mut(&mut execution.objects);

        // If necessary, generate the list of stores to permute through
        if execution.path.is_traversed() {
            let mut seed = [0; MAX_ATOMIC_HISTORY];

            let n = state.match_load_to_stores(&execution.threads, &mut seed[..], ordering);

            execution.path.push_load(&seed[..n]);
        }

        // Get the store to return from this load.
        let index = execution.path.branch_load();

        T::from_u64(state.load(&mut execution.threads, index, location, ordering))
    })
}

先 branch(Action::Load)：登记操作、schedule()，也许被切走（DPOR）。被选中之后才进入 synchronize：本线程 causality 的自身分量加一（rt/mod.rs:137-146），然后在执行上下文里做后面的事。

2. 那一刻的写历史

数据原子的状态（第 3 个交错，0 号线程正要读数据时；打印自副本）：

0 号线程此刻的 causality 是 [3, 0]（向量只列前两个分量，其余为 0；— 表示「还没看到」，代码里是 u16::MAX）。

• stores 是一个 7 格的环形数组，第 k 次写（初值算第 0 次）放在 k % 7 号槽，cnt 记总共写了几次（atomic.rs:121-125、atomic.rs:910-931）。值一律存成 u64。
• 初值也是一次写：State::new 用 Release 做了一次 store（atomic.rs:402-433）。
• modification_order 是这次写在修改顺序里的位置，用向量时钟表示的偏序：写的时候从本线程的 causality 开始，再并入本线程已经看到的写的位置（atomic.rs:456-500）。[0, 0] < [0, 2]，所以 42 在修改顺序上比 0 新。
• first_seen[t] 是线程 t 第一次看到这次写时自己的时钟分量（atomic.rs:164、866-905）。写的人在写时就算看到了；读到它的人在读时记一次。

3. 算候选

路径走到头，调 match_load_to_stores。核心是一个双重循环：对每个写 i，看有没有一个修改顺序上比它新的写 j，满足下面任一条，有就排除 i：

if mo_i < mo_j {
    if store_j.first_seen.is_seen_by_current(threads) {
        // Store `j` is newer, so don't store the current one.
        continue 'outer;
    }

    if store_i.first_seen.is_seen_before_yield(threads) {
        // Saw this load before the previous yield. In order to
        // advance the model, don't return it again.
        continue 'outer;
    }

    if is_seq_cst(ordering) && store_i.seq_cst && store_j.seq_cst {
        // There is a newer SeqCst store
        continue 'outer;
    }
}

第一条是关键：有更新的写已经在本线程的因果历史里，旧的就不能再读（coherence）。is_seen_by_current 的判断是：存在某个线程 t，first_seen[t] ≤ 本线程 causality[t]，即「有人看到过 j，而且那件事 happens-before 我」。

对上表：i = 0（值 0），j = 1（值 42），mo_0 < mo_1。stores[1].first_seen 只有 1 号线程的分量 2，0 号线程的 causality[1] 是 0，2 ≤ 0 不成立：42 这次写不在 0 号线程的因果历史里。第二条（没有 yield 过）、第三条（不是 SeqCst）也不成立。所以 0 不被排除。42 没有比它更新的写，也是候选。

副本打印的候选正是 [0, 1]，push_load 建一个 Load { values: [0, 1], len: 2, pos: 0 }。branch_load 取 values[pos] = 槽 0，读到 0，断言失败。

如果没有失败，下一轮 step 会把这个 Load 的 pos 换成 1，读到 42（Path）。候选的排列顺序是槽号，不是新旧顺序。

4. 读完之后

State::load：

fn load(&mut self, threads: &mut thread::Set, index: usize, location: Location, ordering: Ordering) -> u64 {
    self.loaded_locations.track(location, threads);
    // Validate memory safety
    self.track_load(threads);

    // Apply coherence rules
    self.apply_load_coherence(threads, index);

    let store = &mut self.stores[index];

    store.first_seen.touch(threads);
    store.sync.sync_load(threads, ordering);
    store.value
}

• track_load：和 with_mut / unsync_load 之间的非同步访问检查（UnsafeCell 与原子的非同步访问）。
• apply_load_coherence：把「本线程已看到的写」和「happens-before 本线程的写」的修改顺序并进被读的这次写，保证之后的 load 不会读到比它更旧的（写历史与 coherence）。
• first_seen.touch：记下本线程第一次看到这次写。
• sync_load(ordering)：只有 Acquire / AcqRel / SeqCst 才把那次写存的时钟并进本线程的 causality（synchronize.rs:23-37）。Relaxed 什么也不做。

对照：Release / Acquire

同一个模型 flag 改回 Release / Acquire，第 3 个交错 0 号线程读 flag 读到 true 时，sync_load(Acquire) 把 1 号线程写 flag 时的时钟并进来，0 号线程的 causality 从 [2, 0] 变成 [3, 3]（其中 0 号分量的加一来自读数据前的 synchronize）。再读数据时：stores[1].first_seen[1] = 2 ≤ 3，42 已在因果历史里，初值 0 被第一条规则排除，候选只有 [1]，读到 42。副本打印的路径里，这一轮数据 load 的 Load 分支就是 L[1]，只有一个候选。

两种写法的区别全在一行：Relaxed 的 sync_load 是空的，Acquire 的会 join。loom 不模拟缓存、不模拟乱序执行，「Relaxed 读到旧值」在它这里就是「旧写没被排除，作为一个候选被枚举到」。

只留 7 次写

MAX_ATOMIC_HISTORY = 7（rt/mod.rs:64-65）。第 8 次写覆盖第 1 次所在的槽，被覆盖的写就不再是任何 load 的候选。

实验 E6：7 次写的窗口

断言：每个原子只保留最近 7 次写；更早的写，loom 不会让任何 load 读到。

方法（exp-loom/runtime/tests/history.rs）：1 号线程对 x 连写 1、2、…、n（Relaxed），再 Relaxed 置 flag；0 号线程 Relaxed 读 flag，为真则 Relaxed 读 x，把读到的值收集起来。flag 是 Relaxed，0 号线程和 1 号线程之间没有同步，按 C11，x 的任何一次写（包括初值 0）都可能被读到。

结果（交错数确定）：

n = 9 时，副本打印的数据原子（cnt = 10）：

初值 0 和前两次写 1、2 已被覆盖。7 个槽全是候选（[0, 1, …, 6]），按槽号枚举，所以第一个被试的值是 7，不是最旧的 3。

反向验证：n = 5 那一行。写的次数加初值不超过 7 时，初值 0 仍在候选里，说明 n = 7、9 时少掉的值是窗口造成的，不是模型本身读不到。

这个窗口意味着：一个依赖「读到很久以前的值」才会出错的算法，如果中间同一个原子被写了 7 次以上，loom 在这里不会给出那个值。代价和取舍在 写历史与 coherence 与 07 能力边界。

小结

• 一次原子 load = 一个调度点（branch）+ 一个 Load 分支；候选在路径第一次走到这里时由 match_load_to_stores 一次算好，之后每轮重放时按 pos 依次换。
• 候选规则的核心：修改顺序上更新的写已经在本线程因果历史里（first_seen[t] ≤ causality[t]），旧写就排除；另有 yield 与 SeqCst 两条。
• Relaxed 读到旧值 = 旧写没被排除；Acquire 读把对方的时钟并进来，旧写随之被排除。消息传递模型里，flag 为 Relaxed 时数据 load 的候选是 [0, 42]，为 Acquire 时只剩 [42]。
• 每个原子是一个 7 格环形数组，候选按槽号枚举；更早的写被覆盖后不再是候选（E6：写 9 次后只可能读到 3–9）。