load 的候选

主线位置：主线 2 的核心。AtomicUsize::load → branch(Load) → synchronize → match_load_to_stores 列出候选 → Path 记成 Load 分支 → branch_load 取本轮的候选 → State::load 做 coherence 与 acquire。前一章讲了候选从哪来（最近 7 次写），这一章讲怎么筛。

一次 load 的全过程

rt/atomic.rs:227-250：

    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();

            trace!(state = ?self.state, ?ordering, "Atomic::load");

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

sequenceDiagram
  participant U as 用户代码
  participant A as rt::Atomic::load
  participant P as Path
  participant S as State
  U->>A: load(ordering)
  A->>A: branch(Load)：调度点，可能先切到别的线程
  A->>A: synchronize：本线程分量加一
  alt 路径已走到头（is_traversed）
    A->>S: match_load_to_stores
    S-->>A: 候选槽位，最多 7 个
    A->>P: push_load：新建 Load 分支，pos = 0
  end
  A->>P: branch_load：取 values[pos]
  A->>S: State::load(index)：track_load、coherence、first_seen、sync_load
  S-->>U: 值

两个要点：

• 候选只在第一次走到这里时算。 之后的轮次重放同一段前缀时，is_traversed() 为假，branch_load 直接按记录取第 pos 个候选（path.rs:205-217）。如果这次取到的分支不是 Load，就 panic「Reached unexpected exploration state. Is the model fully deterministic?」。
• 轮换候选靠 Path::step。 一轮结束后，step 从路径末尾往前找，遇到 Load 分支就 pos += 1，还没到 len 就从这里重新开始（path.rs:438-449），详见 02 Path。候选按槽位下标排列，不是按新旧排列；环形数组还没绕回时，槽位顺序恰好是写入顺序，所以第一次走到这里时读的是最老的候选。

三条排除规则

match_load_to_stores 对每一个真实存在的写 i，看有没有另一个写 j 在修改顺序上严格晚于它（mo_i < mo_j）。只有存在这样的 j，i 才可能被排除；排除的理由有三种：

                // TODO: this sometimes fails
                assert_ne!(mo_i, mo_j);

                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;
                    }
                }

修改顺序不可比的两次写互不排除，两者都留作候选。assert_ne! 旁的「TODO: this sometimes fails」是 #220 加的注释，代码没有说明在什么情况下失败，本卷的实验里没有触发过。

规则一：已经看到更新的写

j 比 i 新，且 j 已被当前线程「看到」（is_seen_by_current：某个线程读到或写出 j 的那一步发生在当前线程之前）。这就是 coherence：看到过新值之后不能再读旧值。

实验 E5 的 CoRR（exp-loom/survey/tests/litmus.rs）：子线程 x.store(1, Relaxed)、x.store(2, Relaxed)；主线程连读两次 x（Relaxed）。44 个交错，结果集合是：

{(0, 0), (0, 1), (0, 2), (1, 1), (1, 2), (2, 2)}

没有 (1, 0)、(2, 0)、(2, 1)。第一次读到 1 时，State::load 给 1 的 first_seen 记上主线程；第二次读时 1 已被看到，而 0 在修改顺序上早于 1（同一线程先写的、初值又在一切写之前），0 被规则一排除。六种结果全部是 C11 允许的，倒序一种都没有。

上一章 E6 的对照组也是这条规则：flag 改成 Release / Acquire 后，主线程读到 flag 时已经通过 acquire「看到」了 x 的最后一次写 9，窗口里更老的 6 次写都被排除，只剩 9。

规则二：yield 之前读过的旧值

    fn is_seen_before_yield(&self, threads: &thread::Set) -> bool {
        let thread_id = threads.active_id();

        let last_yield = match threads.active().last_yield {
            Some(v) => v,
            None => return false,
        };

        match self.0[thread_id.as_usize()] {
            u16::MAX => false,
            v => v <= last_yield,
        }
    }

（atomic.rs:891-903）yield_now 时把本线程当时的时钟分量记进 last_yield（thread.rs:128-132）。之后这个线程再读同一个原子，凡是它自己在 yield 之前就读到过、并且已经有更新的写的值，不再给它。注释说明了目的：「In order to advance the model」。一个 while flag.load(Relaxed) == 0 { yield_now() } 的循环，如果 yield 之后还能一直读到旧的 0，模型永远走不完。这条规则从 0.1.0 就在（a2dcce6，2018-12）。

实验（exp-loom/memory-model/tests/yield_.rs）：子线程 x.store(1, Relaxed)，紧接着置一个 std 的标志 STORED；主线程读两次 x（Relaxed），两次之间有或没有 yield_now，第二次读完立刻看 STORED。loom 的所有模型线程跑在同一个 OS 线程上，子线程只能在调度点插进来，第二次读之前最后一个调度点就是这次读自己的 branch，所以 STORED 如实反映「第二次读挑值时，子线程的写是否已经执行」。

只少了一种：「子线程已经写了 1，第二次仍读到 0」。C11 允许这个结果（Relaxed 读可以一直读旧值），所以这条规则是少探索的方向：yield 之后才读到旧值才会出错的代码，loom 不会报。好处是自旋等待的模型能结束，04 死锁、分支上限与位置信息 的 E11 就靠它：同一个自旋锁不 yield 第 28 个交错撞分支上限，加上 yield_now 189 个交错通过。

规则三：SeqCst load 跳过旧的 SeqCst 写

load 是 SeqCst、i 和 j 都是 SeqCst 写、j 比 i 新，i 就被排除，不管当前线程有没有看到 j。这是 0.7.2 里 SeqCst 访问唯一比 AcqRel 多出来的东西（另一处 threads.seq_cst() 是空函数，见 fence 与 SeqCst）。

实验（exp-loom/memory-model/tests/seqcst_load.rs）：主线程 x.store(1, SeqCst)、x.store(2, SeqCst) 后置 std 标志 DONE；子线程读一次 x，读完看 DONE。

两次写都执行之后，SeqCst load 不再读 1，但仍然能读 0：初值是构造时的一次 Release 写（State::new），seq_cst 为假，规则三管不到它。规则只比较「两次都是 SeqCst 的写」，所以它能做的事很有限：SB（store buffering）里两个线程读的是对方写的另一个变量，每个变量上只有初值和一次 SeqCst 写，规则三从不生效，(0, 0) 照样出现（E5，fence 与 SeqCst）。

State::load：读完之后

atomic.rs:435-454：

        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

1. track_load：和 with_mut 的非同步访问冲突就 panic（04 UnsafeCell 与原子的非同步访问）。
2. apply_load_coherence：把已看到的写、发生在之前的写定在被读的写之前（写历史与 coherence）。
3. first_seen.touch：本线程第一次看到这个写，记下当前分量。以后本线程、以及所有「发生在本线程这一步之后」的线程，都会把它当成已看到。
4. sync_load：Acquire 以上才把写的同步点并进本线程时钟（向量时钟与同步点）。

Relaxed load 只做前三步。它不传递 happens-before，但会改变「谁已看到什么」，从而收窄后续 load 的候选。

unsync_load：不建分支

AtomicUsize::unsync_load 是 unsafe fn，loom 的扩展 API（std 没有），into_inner 也是用它实现的（sync/atomic/int.rs:30-49）。运行时实现（atomic.rs:252-270）：

• 不调 branch，不是调度点；不调 synchronize；不建 Load 分支；
• 直接返回 stores[index(cnt - 1)]，即 loom 执行顺序里最后一次写的值；
• 只做 track_unsync_load：和并发的原子写、with_mut 冲突就报错。

它的语义是「我保证此刻没有并发的写，给我最新值」，loom 不去探索它能读到什么，只检查那个保证是否成立。检查的细节见 04 UnsafeCell 与原子的非同步访问。

小结

• 候选只在路径第一次走到这次 load 时计算，之后按 Load 分支的 pos 重放；step 逐个换候选。候选按槽位顺序排列。
• 一个写被排除，前提是有修改顺序上严格更晚的写；理由有三：更晚的写已被看到（coherence）、本线程 yield 前读过它、SeqCst load 且两次都是 SeqCst 写。
• E5 CoRR：44 个交错、六种结果，没有倒序。
• yield 规则让自旋模型能结束，代价是「yield 之后读到旧值」这一类结果不再出现（实验：17 个交错四种结果 → 11 个交错三种结果）。
• SeqCst load 只跳过「被更新的 SeqCst 写压着的 SeqCst 写」，初值不受影响（实验：两次 SeqCst 写之后仍能读到 0，读不到 1）。
• State::load 之后才做 coherence、first_seen 和 acquire；unsync_load 不是调度点，直接读最后一次写，只检查竞争。