checkpoint、日志与位置

主线位置：主线 1 的调试面。checkpoint 存的是 Path（每个分支选了什么），重放就是主线 1 里「已走过的前缀按记录选」那一步；日志是 Execution::schedule 和各原语里的 tracing 事件；位置信息来自每个对外操作上的 #[track_caller]。

flowchart TB
  start["check：i = 1"] --> load{"有 checkpoint 文件？"}
  load -->|有| ld["载入 Path，从那条路径开始"]
  load -->|没有| loop
  ld --> loop["第 i 轮"]
  loop --> chk{"i % interval == 0 ？"}
  chk -->|是| st["写文件（本轮即将走的路径）；检查 max_permutations / max_duration"]
  chk -->|否| run
  st --> run["跑闭包；失败则 panic 穿出，文件停在最近一次写入"]
  run --> step{"step：还有未走的分支？"}
  step -->|有| inc["i += 1"] --> loop
  step -->|没有| done["Completed in N iterations；文件留在磁盘上"]

文档的三步法

lib.rs:192-249 推荐的调试流程：

1. 设 LOOM_CHECKPOINT_FILE=my_test.json 跑一次失败的测试，「生成 checkpoint」。
2. 再加 LOOM_CHECKPOINT_INTERVAL=1 跑，「检查下一个交错确实触发错误」，测试应在第一个交错失败。
3. 再加 LOOM_LOG=trace、LOOM_LOCATION=1，只看失败那一轮的完整日志。

下面对照代码看每一步实际发生什么，再给出一个能用的流程。

checkpoint 只在整 interval 轮写

model.rs:164-189：

let start = Instant::now();
loop {
    if i % self.checkpoint_interval == 0 {
        info!(parent: None, "");
        info!(
            parent: None,
            " ================== Iteration {} ==================", i
        );
        info!(parent: None, "");

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

三个事实：

• 文件只在第 interval、2 × interval … 轮开始前写，内容是「这一轮即将走的路径」。LOOM_CHECKPOINT_INTERVAL 默认 20 000。
• 失败就是 panic 穿出 check，没有「失败时写一次」的逻辑。文件里留下的是失败之前最近一次整点的路径。
• 启动时文件存在就载入（152-157 行），从那条路径开始，而不是从头开始。max_permutations / max_duration 也只在这些整点检查（model 与 Builder）。

实验 E3（exp-loom/survey/tests/checkpoint2.rs）用两个会失败的模型：

40 000 + 14 302 − 1 = 54 301：第二次运行从第 40 000 轮的路径接着走，走到同一个失败。

对照文档的三步法：

• 第 1 步只有在失败发生在第 20 000 个交错之后才会留下文件；早失败时什么都没有，第 2 步就是从头跑。
• 第 2 步不会「第一个交错就失败」，而是从最近的整点续跑，在第 (N − 整点 + 1) 个交错失败；它的作用是以每轮写一次的代价，把失败那一轮的路径精确存下来。
• 第 3 步（同一个文件、INTERVAL=1）才会在第 1 个交错失败。

能用的流程

1. 失败来得早（几万个交错以内）：直接 LOOM_CHECKPOINT_FILE=f.json LOOM_CHECKPOINT_INTERVAL=1 跑一次，失败时文件就是那一轮的路径。
2. 失败来得晚：先只设 LOOM_CHECKPOINT_FILE 跑一次，得到一个离失败不到 20 000 轮的起点；再加 LOOM_CHECKPOINT_INTERVAL=1 跑一次，从起点续跑到失败，文件变成精确路径。
3. 最后加 LOOM_LOG=trace LOOM_LOCATION=1，仍用这个文件和 INTERVAL=1，第 1 个交错就失败，日志只有这一轮。
4. 修完以后删掉文件（见下一节）。

INTERVAL=1 的代价是每轮序列化一次 Path 并写盘。E3 的晚失败模型（54 301 轮）：默认间隔 6.04–6.09 s，INTERVAL=1 8.48–8.52 s，慢约 40%（3 轮，exp-loom/speed/timing.sh，开始时负载 2.55 / 2.86，过程中 1 分钟负载升到约 3.5，量级）。用默认间隔留下的文件续跑到失败只要 1.58–1.59 s。

残留的文件决定下一次从哪开始

文件在测试通过后也不会被删。实测（exp-loom/usage/tests/stale.rs，2 个线程各两次 fetch_add）：

第三次运行从「最后一轮」的路径开始，step 之后已经没有未走的分支，于是报告完成。测试显示通过，实际只跑了一轮。修完 bug 后忘了删文件、或者把 LOOM_CHECKPOINT_FILE 写进了 CI 的环境变量，都会这样。如果代码改了、旧路径对不上新代码的分支，则会在重放时报「Reached unexpected exploration state. Is the model fully deterministic?」。

没开 checkpoint feature

序列化 Path 要用 serde，所以放在 checkpoint feature 后面。没开时两个函数都是 panic（model.rs:267-278）：

#[cfg(not(feature = "checkpoint"))]
mod checkpoint {
    use std::path::Path;

    pub(crate) fn load_execution_path(_fs_path: &Path) -> crate::rt::Path {
        panic!("not compiled with `checkpoint` feature")
    }

    pub(crate) fn store_execution_path(_path: &crate::rt::Path, _fs_path: &Path) {
        panic!("not compiled with `checkpoint` feature")
    }
}

但它们只在上面那两个位置被调用：文件存在时载入，整点时写入。E3 反向（exp-loom/no-checkpoint，loom =0.7.2 不开任何 feature，一个 4 个交错的小模型）：

所以「设了环境变量却忘了开 feature」在小模型上是静默的。tokio 的 Cargo.toml 给 loom dev-dependency 开了 checkpoint 和 futures 两个 feature。

LOOM_LOG：tracing 过滤串

model() 在每次调用时装一个 tracing-subscriber 的 fmt subscriber（model.rs:231-244）：

let subscriber = fmt::Subscriber::builder()
    .with_env_filter(EnvFilter::from_env("LOOM_LOG"))
    .with_test_writer()
    .without_time()
    .finish();

LOOM_LOG 的值就是 EnvFilter 的指令串（写法见 tracing 卷 EnvFilter），可以写 info、trace，也可以写 loom::rt::atomic=trace 只看原子。直接调 Builder::check 不会装这个 subscriber（model 与 Builder）。

实测（exp-loom/usage/tests/logs.rs，Release / Acquire 消息传递，6 个交错）：

• info：每次线程切换一行 ~~~~~~~~ THREAD n ~~~~~~~~（来自 execution.rs:252），6 轮共 18 行，最后一行 INFO loom::model: Completed in 6 iterations。每行带 span 前缀 iter{3}:thread{id=1}:，两个 span 是 0.5.5 加的（#266、#267），告诉你这是第几轮、哪个线程。
• trace：每个对象创建、每个 branch、每次引用计数变化各一行，同一个模型共 313 行。例如：

TRACE iter{1}: loom::rt::arc: Arc::new state=Ref<loom::rt::arc::State>(1) location=
TRACE iter{1}: loom::rt::object: Object::branch_action obj=Ref<loom::rt::arc::State>(1) action=RefInc
TRACE iter{1}:thread{id=0}: loom::rt: branch switch=false
TRACE iter{1}:thread{id=0}: loom::rt::arc: Arc::ref_inc state=Ref<loom::rt::arc::State>(1) ref_cnt=2 location=

location= 为空，是因为没开 LOOM_LOCATION。对一个跑满上万轮的模型开 trace 会产生海量输出，这就是三步法先用 checkpoint 把范围缩到一轮的原因。输出里带 ANSI 颜色码，重定向到文件时也一样。

什么时候看得到

with_test_writer() 把日志写进 libtest 的输出捕获：

失败的测试本来就会附上捕获的输出，所以调试失败时不加 --nocapture 也能看到全部日志；只有想看通过的模型走了哪些轮时才需要加。

LOOM_LOCATION

Builder::new 里是 env::var("LOOM_LOCATION").is_ok()（model.rs:90）：只看变量是否存在，LOOM_LOCATION=0 也会打开（实测：同一个自锁模型，设成 0 时死锁报告里带上了文件位置）。

打开后，每个对外操作经 #[track_caller] 传下来的调用位置会被记录。两种常见输出（exp-loom/survey/tests/misc.rs）：

Causality violation: Concurrent write accesses to `UnsafeCell`.
      created: tests/misc.rs:15:24
    write one: thread #0 @ tests/misc.rs:18:9
    write two: thread #1 @ tests/misc.rs:17:41

deadlock; threads = [(Id(0), Blocked(Location(Some(Location { file: "tests/misc.rs", line: 220, column: 18 }))))]

不开时第一种只有第一行，第二种是 Blocked(Location(None))。格式与来源见 UnsafeCell 与原子的非同步访问 与 死锁、分支上限与位置信息。位置记录只在报错时有用，平时可以不开。

小结

• checkpoint 文件只在第 interval 的整数倍轮开始前写，内容是这一轮的路径；失败时不额外写。默认间隔 20 000 下，早失败不留文件（E3），晚失败的文件让重跑从最近整点续跑（第 54 301 轮失败的模型，重跑在第 14 302 轮失败）。
• INTERVAL=1 每轮写一次，失败时文件就是失败那一轮，重放第 1 轮即失败。能用的流程：早失败直接 INTERVAL=1；晚失败先默认间隔跑出起点、再 INTERVAL=1 续跑；最后加日志重放；修完删文件。
• 残留文件让下一次从中途开始：通过的模型留下的文件使重跑只跑 1 轮就「通过」。
• 没开 checkpoint feature：文件不存在且不到整点时静默通过；整点或文件存在时 panic「not compiled with checkpoint feature」。
• LOOM_LOG 是 EnvFilter 串，只在 model() 里生效；info 每次切换一行加「Completed in N iterations」，trace 每个操作一行；失败的测试不加 --nocapture 也会附上日志。
• LOOM_LOCATION 只看是否存在，设成 0 也打开；报错里带上创建与访问位置。