model 与 Builder

主线位置：主线 1 的入口。loom::model(f) 装一个日志订阅者，Builder::new() 读环境变量，check 建好 Execution 和 Scheduler，然后进入「跑一轮、查泄漏、step 到下一条路径」的循环。本页讲这个循环本身，以及它的几个开关在什么时候生效。

flowchart TB
  m["model(f)：装 tracing 订阅者（EnvFilter 读 LOOM_LOG）"] --> b["Builder::new()：读 8 个环境变量"]
  b --> c["check(f)：Execution::new + Scheduler::new；有 checkpoint 文件就载入 Path"]
  c --> q{"i % checkpoint_interval == 0 ?"}
  q -->|是| ck["写 checkpoint；查 max_permutations / max_duration，超了就 return"]
  q -->|否| run
  ck --> run["scheduler.run：把 f 包成 0 号线程跑完一轮"]
  run --> leak["check_for_leaks"]
  leak --> step{"execution.step()"}
  step -->|"Some(next)：还有没走的分支"| q
  step -->|None| done["Completed in N iterations"]

整个文件 model.rs 278 行，一半是字段文档。

10 个字段与 8 个环境变量

model.rs:14-72 定义 Builder，model.rs:74-128 的 Builder::new 逐个读环境变量：

几点从代码直接能看出来的：

• 解析失败直接 panic。 每个数值变量都是 v.parse().expect("invalid value for ...")。实测 LOOM_MAX_PREEMPTIONS=two，Builder::new() 本身就 panic：

  Copy

  invalid value for `LOOM_MAX_PREEMPTIONS`: ParseIntError { kind: InvalidDigit }
  

  变量名写错（例如 LOOM_MAX_PREEMPTION）则不会有任何提示，等于没设。

• preemption_bound 实际按 u8 存。 字段是 Option<usize>，传进 Execution::new 时 bound.try_into().expect("preemption_bound too big")（execution.rs:58-59），因为 Path 里的抢占计数是 u8。实测 preemption_bound = Some(300) 在 check 一开始就 panic「preemption_bound too big: TryFromIntError(PosOverflow)」。上限有多大意义见 抢占上限与剪枝。

• #[non_exhaustive]（model.rs:16）。外部 crate 不能用结构体字面量构造 Builder，只能 Builder::new()（或 Default，它就是 new()）之后逐个改字段。这意味着环境变量总会被读一遍：代码里把字段改掉会覆盖环境变量，没改的字段仍然受环境影响。本卷实验里固定上限的写法是：

  Copy

  let mut b = loom::model::Builder::new();
  b.preemption_bound = Some(2);
  b.check(|| { /* 模型 */ });
  

• max_threads 的文档和默认值对不上。 字段文档说「must be less than [MAX_THREADS]」，而默认值 DEFAULT_MAX_THREADS = 5 正好等于 MAX_THREADS = 5（model.rs:11 对 rt/mod.rs:61-62）。以代码为准：这个数是「包括主线程在内的线程总数」，设成 5 没问题。设成大于 5 不会被拒绝，但向量时钟和 Schedule 里的线程数组都是 MAX_THREADS 长的定长数组：实测 max_threads = 6 再 spawn 5 个线程，在 new_thread 给第 6 个线程的时钟加一处（execution.rs:88）panic「index out of bounds: the len is 5 but the index is 5」。其余实测见下文 E12。

check 的主循环

model.rs:136-219，省略了日志：

pub fn check<F>(&self, f: F)
where
    F: Fn() + Sync + Send + 'static,
{
    let mut i = 1;

    let mut execution = Execution::new(
        self.max_threads,
        self.max_branches,
        self.preemption_bound,
        !self.expect_explicit_explore,
    );
    let mut scheduler = Scheduler::new(self.max_threads);

    if let Some(ref path) = self.checkpoint_file {
        if path.exists() {
            execution.path = checkpoint::load_execution_path(path);
            execution.path.set_max_branches(self.max_branches);
        }
    }

    execution.log = self.log;
    execution.location = self.location;

    let f = Arc::new(f);

    let start = Instant::now();
    loop {
        if i % self.checkpoint_interval == 0 {
            // info!(" ================== Iteration {} ==================", i) …
            if let Some(ref path) = self.checkpoint_file {
                checkpoint::store_execution_path(&execution.path, path);
            }
            if let Some(max_permutations) = self.max_permutations {
                if i >= max_permutations {
                    return;
                }
            }
            if let Some(max_duration) = self.max_duration {
                if start.elapsed() >= max_duration {
                    return;
                }
            }
        }

        let f = f.clone();

        scheduler.run(&mut execution, move || {
            f();

            let lazy_statics = rt::execution(|execution| execution.lazy_statics.drop());

            // drop outside of execution
            drop(lazy_statics);

            rt::thread_done();
        });

        execution.check_for_leaks();

        i += 1;

        if let Some(next) = execution.step() {
            execution = next;
        } else {
            // info!("Completed in {} iterations", i - 1);
            return;
        }
    }
}

逐段看：

1. 闭包是 Fn，不是 FnOnce。 同一个闭包要被调用成千上万次，所以只能借用捕获的东西；每轮在闭包里面新建所有 loom 对象。Sync + Send + 'static 是因为它被包进 std::sync::Arc，再 move 进 0 号线程的协程。
2. Execution 与 Scheduler 只建一次。 每轮结束后 execution.step() 返回一个复用了全部容器的新 Execution（Execution 与对象仓库）；Scheduler 只存一个 max_threads，每轮的协程在 run 里重新创建（协程调度器）。
3. 一轮的尾巴：闭包返回后，先 drop 这一轮的 lazy_static! 值（在执行上下文之外 drop，因为它们的析构函数可能又碰 loom 对象），再 rt::thread_done() 把 0 号线程标成结束。0 号线程的结束和子线程走同一条路（rt/mod.rs:177-197），所以主线程不 join 的子线程也会被调度跑完。
4. 每轮查一次泄漏：check_for_leaks 遍历对象仓库，Arc 计数不为零、alloc 没释放、channel 里还有消息都 panic（04 检测器）。
5. step 返回 None 就结束：路径上再也找不到没走过的选项，打印「Completed in N iterations」。step 怎么找下一条路径见 Path：路径与深度优先。

两个上限只在整间隔处检查

max_permutations 和 max_duration 都放在 if i % self.checkpoint_interval == 0 里面（model.rs:166-189）。默认间隔 20 000，所以：

• 设 LOOM_MAX_PERMUTATIONS=10，第一次检查发生在 i = 20 000。模型不到 2 万个交错就会全部跑完，上限等于没设。
• 设 LOOM_MAX_DURATION=60，第一次看表也在第 2 万轮；之后每 2 万轮看一次。一轮慢的模型，2 万轮可能远超 60 秒。
• 检查发生在这一轮开始之前，条件是 i >= max_permutations。间隔为 100、上限为 10 时，第一次检查在 i = 100，此时已经跑完 99 轮。

文档没有写这个粒度（字段注释只说「Maximum number of permutations to explore」）。

实验 E4：上限什么时候生效

断言：max_permutations 只在 i 是 checkpoint_interval 的整数倍时生效；间隔默认 20 000 时，小模型设了等于没设。

方法（exp-loom/runtime/tests/builder.rs）：3 个线程各对同一个 AtomicUsize 做两次 fetch_add(1, Relaxed)，原子放在 Box::leak 出来的 &'static 里（不经过 loom Arc，少一些分支），preemption_bound = Some(3)。四组：不设上限；max_permutations = 10；再把 checkpoint_interval 改成 100；另起一组 max_duration = 0 秒、间隔 1 000。交错数用模型闭包开头的一个 std 原子计数。

结果（交错数是确定的，与负载无关）：

反向验证：第三行。同样的上限，把间隔调小到 100，就停在第 99 轮，说明上限本身是生效的，跑满完全是检查粒度造成的。max_duration = 0 那一行则说明时间上限同样受间隔约束：0 秒的上限，在第 1 000 轮之前根本不会被看一眼，而模型 720 轮就结束了。

所以要用这两个上限截断一个大模型，必须同时把 LOOM_CHECKPOINT_INTERVAL 调到比上限小；代价是 Iteration N 的横幅和（设了文件时）checkpoint 的写入也会跟着变频繁。checkpoint 的写入时机和它对调试的影响见 checkpoint、日志与位置。

model 只比 check 多一个订阅者

model.rs:228-244：

pub fn model<F>(f: F)
where
    F: Fn() + Sync + Send + 'static,
{
    let subscriber = fmt::Subscriber::builder()
        .with_env_filter(EnvFilter::from_env("LOOM_LOG"))
        .with_test_writer()
        .without_time()
        .finish();

    subscriber::with_default(subscriber, || {
        Builder::new().check(f);
    });
}

model 和 Builder::new().check(f) 的唯一区别，是在一个 tracing_subscriber::fmt 订阅者的作用域里跑。于是：

• LOOM_LOG 的值是一个 EnvFilter 过滤串（info、trace、loom::rt::atomic=trace 都行）；Builder.log 字段只看变量存不存在，存进 execution.log 之后在 0.7.2 里没有任何地方读它。真正决定打不打印的是这个订阅者。
• with_test_writer() 把输出交给测试框架的捕获机制，不加 --nocapture 看不到。
• 直接调 Builder::check 时 LOOM_LOG 不起作用，除非调用方自己装了订阅者。

实测（exp-loom/runtime/tests/builder.rs 的 log_check，LOOM_LOG=info，--nocapture）：同一个「spawn 一个空线程再 join」的模型，loom::model 打出三行

 INFO iter{1}:thread{id=1}: loom::rt::execution: ~~~~~~~~ THREAD 1 ~~~~~~~~
 INFO iter{1}:thread{id=0}: loom::rt::execution: ~~~~~~~~ THREAD 0 ~~~~~~~~
 INFO loom::model: Completed in 1 iterations

紧接着的 Builder::new().check(...) 一行也没有。用 Builder 定制上限、又想看日志的模型，要自己用 tracing_subscriber 包一层，写法照抄上面的 model 即可。

tracing-subscriber（带 env-filter feature）因此是 loom 的必选依赖（Cargo.toml:40-41），每次调用 model 都新建一个订阅者。日志的内容和读法在 checkpoint、日志与位置。

线程数上限

max_threads 在两处起作用：thread::Set::new 用它做 Vec::with_capacity，Set::new_thread 在 spawn 时检查 assert!(self.threads.len() < self.max())（rt/thread.rs:214-226，max() 就是这个 Vec 的容量）。所以 max_threads 是含主线程的总数，默认主线程之外最多 4 个。

实验 E12：线程数上限

方法（exp-loom/runtime/tests/builder.rs 的 e12_threads）：模型里 spawn n 个空线程再逐个 join；默认 Builder 与 max_threads = 3 各跑一组。

结果：

报错不提「线程太多」，也不提上限是几，只有一行断言原文。它来自 rt/thread.rs:215，而不是 Scheduler::run 里那句 assert!(threads.len() < self.max_threads)（scheduler.rs:99）：thread::spawn 先调 execution.new_thread() 登记线程，那里的断言先触发。

小结

• Builder 10 个字段，8 个有环境变量；数值变量解析失败直接 panic，LOOM_LOCATION / LOOM_LOG 只看存在与否；preemption_bound 超过 u8 也 panic。
• #[non_exhaustive]，只能 Builder::new() 后改字段，环境变量总会被读。
• 主循环：每轮 run → 查泄漏 → step；闭包是 Fn，每轮在里面重建所有 loom 对象。
• max_permutations / max_duration 只在 i % checkpoint_interval == 0 时检查（E4：上限 10 在默认间隔下跑满 720 个交错，间隔 100 时停在第 99 个）。
• model = 装 EnvFilter 订阅者 + Builder::new().check；直接用 check 时 LOOM_LOG 无效，日志要 --nocapture。
• max_threads 含主线程，默认 5；超了是「assertion failed: self.threads.len() < self.max()」（E12）。