抢占上限与剪枝

主线位置：主线 1 的两个旋钮。上一章的 DPOR 决定「哪些位置值得换一个线程试试」；本章的两个机制在此之上再收紧：抢占上限限制一条路径上「强行打断一个还能跑的线程」的次数，explore / stop_exploring / skip_branch 让模型自己声明哪一段不必换序。

flowchart LR
  dpor["DPOR：backtrack(point, T)"] --> b{"该 Schedule 的 preemptions == 上限？"}
  b -->|是| drop["不登记"]
  b -->|否| mark["T 标 Pending"]
  mark --> extra["有上限时：沿 prev 往前找上一个换过线程的 Schedule，再登记一次"]
  dpor --> ex{"该 Schedule.exploring？"}
  ex -->|否：stop_exploring / skip_branch 之后建的| back["往前找 exploring 的 Schedule"]

怎么数抢占

抢占（preemption）指：当前线程还能跑，却换成了别的线程。线程自己阻塞、结束或 yield_now 后换人，不算抢占。

Schedule 里有三个字段为此服务（path.rs:37-54）：preemptions（到达这个分支之前已经发生的抢占数）、initial_active（这个分支新建时的默认线程，如果它就是上一个分支的活动线程）、prev（上一个 Schedule 的下标）。新建分支时（path.rs:297-318）：

let mut initial_active = active;

if let Some(prev) = prev {
    if initial_active != prev.get(&self.branches).active_thread_index() {
        initial_active = None;
    }
}

let preemptions = prev
    .map(|prev| prev.get(&self.branches).preemptions())
    .unwrap_or(0);

Schedule::preemptions()：

fn preemptions(&self) -> u8 {
    if self.initial_active.is_some() && self.initial_active != self.active_thread_index() {
        return self.preemptions + 1;
    }

    self.preemptions
}

合起来：一个分支的默认线程如果就是「上一个分支在跑的那个线程」（initial_active 有值），而这一轮这里被换成了别的线程（因为某个 Pending 被 step 改成了 Active），这就是一次抢占，记到下一个分支的 preemptions 上。默认线程本来就和上一个不同（上一个线程阻塞或结束了），initial_active 是 None，在这里换谁都不算抢占。

在 一次 model 的一生 的路径表里可以直接看到：第 2 轮位置 2 默认是 0 号线程、实际跑了 1 号，从位置 3 起 preemptions 是 1；第 4 轮又在位置 6 把 1 号换回 0 号，位置 8 起是 2。6 个交错里，抢占数为 0、1、1、2、2、2。

上限在哪里起作用

Builder.preemption_bound（LOOM_MAX_PREEMPTIONS）进入 Path 时转成 u8（model 与 Builder）。它只在一个地方拦截，Schedule::backtrack 的开头：

if let Some(bound) = preemption_bound {
    assert!(
        self.preemptions <= bound,
        "[loom internal bug] actual = {}, bound = {}",
        self.preemptions,
        bound
    );

    if self.preemptions == bound {
        return;
    }
}

到达这个分支时已经用满了上限，就不在这里登记任何 Pending。因为只有 Pending 能让 step 换线程，用满上限的路径后面再也不会出现新的抢占。上限 0 时第一个分支的 preemptions 就是 0 = 上限，DPOR 的所有回溯都被拒绝，整个模型只跑 1 轮：每个线程一口气跑到阻塞或结束。

有上限时多补一个回溯点

Path::backtrack 在正常登记之后，只在设了上限时多做一步：

let mut curr = if let Some(curr) = schedule.prev {
    curr
} else {
    return;
};

if self.preemption_bound.is_some() {
    loop {
        // Preemption bounded DPOR requires conservatively adding
        // another backtrack point to cover cases missed by the bounds.
        if let Some(prev) = curr.get(&self.branches).prev {
            let active_a = curr.get(&self.branches).active_thread_index();
            let active_b = prev.get(&self.branches).active_thread_index();

            if active_a != active_b && curr.get_mut(&mut self.branches).exploring {
                curr.get_mut(&mut self.branches)
                    .backtrack(thread_id, self.preemption_bound);
                return;
            }

            curr = prev;
        } else {
            if curr.get(&mut self.branches).exploring {
                // This is the very first schedule
                curr.get_mut(&mut self.branches)
                    .backtrack(thread_id, self.preemption_bound);
            }
            return;
        }
    }
}

从刚登记的那个分支的前一个 Schedule 起，沿 prev 链往前，找到最近一个「活动线程和它的前一个分支不同」的分支（即一次线程切换发生的地方），在那里为同一个线程再登记一次；一直找到第一个分支也没有，就登记在第一个分支上。这一步同样经过 Schedule::backtrack，同样受上限约束。它是 2019 年加入抢占上限时（b9d5a95「Add thread preemption bounding (#28)」）就有的逻辑。

上限越大，被拒绝的回溯越少，交错数越多；上限 None 时既不拒绝，也不补这个额外的点。

实验 E2：上限与交错数、耗时

断言：上限 0 时恒为 1 个交错；上限每加 1，交错数乘上一个随模型变大的因子；耗时与交错数大致成正比。

方法（exp-loom/runtime/tests/bound.rs）：T 个线程（2–4）共享一个 AtomicUsize 和一把 Mutex<usize>（都放在 loom Arc 里），每个线程做 O 次「fetch_add(1, AcqRel) + 加锁加一」；主线程 join 全部后断言计数。Builder.max_branches = 10_000，preemption_bound 取 0、1、2、3、4、None。交错数用闭包开头的 std 原子计数，--release。

交错数（确定，与负载无关）：

（「—」：没有跑，规模超出本页需要。）

耗时（release，3 轮）：

2026-11-03 00:21–00:25，开始时负载 1 分钟 2.07、5 分钟 2.87，三轮之后 2.71、2.93（exp-loom/runtime/timing.sh，与其他实验共用 exp-loom/.timing.lock）。单位秒，三轮依次列出：

（3 × 1 不设上限那一次跑了约 2.5 分钟，结束时负载 1 分钟 2.55、5 分钟 2.86。）

• 上限 0 恒为 1 个交错，这一列就是反向验证：上限确实在拦截回溯，计数方法也确实数的是轮数。
• 上限从 2 到 3，交错数在 2 × 2 上乘 3.4，在 3 × 1 上乘 7.6，在 4 × 1 上乘 16；线程越多，每多允许一次抢占带来的增量越大。
• 3 × 1 不设上限是 1 393 998 个交错，是上限 3 的 249 倍、上限 4 的 47 倍。
• 耗时基本和交错数成正比，每秒约 7 000–9 000 个交错（这个模型、这台机器上；4 线程的模型每轮更长，约 7 200 个 / 秒）。

crossbeam 卷的最小 EBR 是第二个实例：两线程模型在上限 2 时 188 个交错、上限 3 时 457 个；三线程模型 3 727 → 29 237，乘了约 7.8。

再看一个能失败的模型。一次 model 的一生 的消息传递模型（exp-loom/runtime/tests/mp_bound.rs），把 flag 的写和读都换成 Relaxed 后，loom 在第 3 个交错报「Causality violation: Concurrent read and write accesses.」：

这个错误需要「1 号线程先跑到 store 之后、0 号线程再读」，也就是一次抢占；上限 0 时这条路径被拒绝，错误代码也会通过。上限是用交错数换「能走到多深的交错」。

设多少

crate 文档的建议是 2 或 3（lib.rs:278-292）：「In practice, setting the thread pre-emption bound to 2 or 3 is enough to catch most bugs while significantly reducing the number of possible executions.」这是上游的经验之谈，文档没有给出数据。本卷照这个建议，只从成本一侧给出依据：

• 上表里上限 3 的交错数，最大的模型（4 × 1）是 13 万个、约 18.5 秒；上限 2 都在 1 万以内，最多约 1.2 秒。3 × 1 不设上限要 154 秒，是上限 3 的约 250 倍。
• 再加 1，交错数乘几倍到十几倍。线程多、操作多的模型，上限 3 就可能从秒级变成分钟级。
• 真实项目的做法：crossbeam-epoch 的 CI 用 LOOM_MAX_PREEMPTIONS=2，脚本注释说「With MAX_PREEMPTIONS=2 the loom tests (currently) take around 11m. If we were to run with =3, they would take several times that」（crossbeam 卷：怎么验证并发代码）。

先用 2 跑通，再在能接受的时间内试 3；模型怎么写才能小，见 写一个好模型。

explore、stop_exploring 与 skip_branch

0.7.0 加入的三个函数（8075e03「Enable user pruning of exploration branches (#323)」），让模型自己告诉 loom「这一段不用换序」。实现都在 Path 上（rt/mod.rs:199-222 转发到 path.rs:139-156）：

pub(crate) fn explore_state(&mut self) {
    if !self.skipping {
        assert!(!self.exploring, "not in critical state");
        self.exploring = true;
    }
}

pub(crate) fn critical(&mut self) {
    if !self.skipping {
        assert!(self.exploring, "not in exploring state");
        self.exploring = false;
    }
}

pub(crate) fn skip_branch(&mut self) {
    self.exploring = false;
    self.skipping = true;
}

Path.exploring 是一个开关，新建的每个分支都把当时的值抄进自己的 exploring 字段。exploring == false 的分支：

• step 回溯时直接跳过，不换选项（Path）；
• DPOR 的 backtrack 不在它上面登记，往前找最近一个 exploring 的 Schedule。

三个函数的区别：

实验 E17：剪枝的效果

方法（exp-loom/runtime/tests/explore.rs）：3 个线程，各对同一个 AtomicUsize（放在 loom Arc 里）做两次 fetch_add(1, Relaxed)，主线程 join 后断言等于 6。不设上限。三种写法：不调任何函数；在 spawn 三个线程之前 stop_exploring()、之后 explore()；spawn 之后调 skip_branch()。

结果（交错数确定）：

• 包住 spawn 毫无作用：spawn 不是调度点（协程调度器），被包住的那段里只有为每个线程 clone Arc 的分支，而那时被 clone 的 Arc 只和 Inspect 相关（DPOR），这段本来就几乎没有可换的序。交错来自三个线程的 fetch_add，它们都发生在 explore() 之后。
• skip_branch 之后只剩 617 个：主线程调用之后，这一轮新建的所有分支都不探索，剩下的交错只来自调用之前已经建好的分支，即主线程 clone Arc、spawn 的过程中已 spawn 的线程插进来跑的那些位置。

skip_branch 的用途是在模型里识别出「这条路径已经没意思了」（比如某个早期选择已经决定了结果），主动放弃它之后的探索。它省下的是探索量；放在哪、放了以后哪些顺序不再被试，要由写模型的人负责。

小结

• 抢占 = 默认线程（上一个分支的活动线程）还能跑却换了人；计数记在下一个 Schedule.preemptions 上，按 u8 存。
• 上限只在 Schedule::backtrack 拦截：到达分支时抢占数已等于上限，就不登记 Pending；上限 0 恒为 1 个交错。
• 设了上限时，Path::backtrack 沿 prev 链在上一个线程切换点再补登记一次（#28 起就有）。
• E2：上限每加 1，交错数乘几倍到十几倍；3 线程各 1 次操作，上限 3 是 5 594、不设是 1 393 998。文档建议 2 或 3，本卷只从交错数和耗时给出依据。
• stop_exploring / explore / skip_branch 把之后新建的分支标成不探索；包住 spawn 没有作用（E17：116 319 → 116 319），spawn 之后 skip_branch 降到 617。