同步原语的模型

02 运行时 讲了 loom 怎么调度、怎么回溯，03 内存模型 讲了原子变量的写历史与 happens-before。这一部分讲剩下的对外类型：锁、条件变量、线程、静态变量、引用计数、channel、future。它们的形状几乎一样：

flowchart LR
  subgraph pub["对外类型（src/sync、src/thread.rs ...）"]
    m["loom::sync::Mutex<T>"]
    a["loom::sync::Arc<T>"]
    ch["mpsc::Sender / Receiver"]
  end
  subgraph rt["rt 运行时对象（只有状态，没有数据）"]
    rm["rt::Mutex：持有者、Synchronize"]
    ra["rt::Arc：ref_cnt、三类上次访问"]
    rc["rt::Channel：消息数、每条消息一个 Synchronize"]
  end
  subgraph std["真正存数据的 std 容器"]
    sm["std::sync::Mutex<T>"]
    sa["std::sync::Arc<T>"]
    sc["std::sync::mpsc"]
  end
  m --> rm
  m --> sm
  a --> ra
  a --> sa
  ch --> rc
  ch --> sc

• rt 对象放在 Execution 的对象仓库里（Execution 与对象仓库），只记录调度和内存模型需要的状态：谁持有锁、计数是多少、上一次相关访问在路径的哪个位置、一个或多个 Synchronize（向量时钟与同步点）。
• 数据放在 std 的同名容器里。loom 用 rt 对象决定「这一步谁能走」，走到了再去拿 std 容器；所以 std 容器那边永远不会真的竞争，它的 lock()、try_read() 在 loom 里只起「把数据借出来」的作用。
• 每个对外操作先调一次 branch_*（调度点），再改 rt 状态、做 acquire / release 同步。阻塞的写法是把当前线程标成 Blocked，由 Execution::schedule 去挑别的线程；释放方把等在同一对象上的线程改回可运行。

四章：

1. Mutex 与 RwLock：branch_acquire 与「加锁成功后把其他想拿锁的线程标成阻塞」；解锁不是调度点；不毒化；RwLock 的读者集合、没有写者优先、同线程嵌套读的内部错误（E14 与反向验证）。
2. Condvar、Notify 与 park：Condvar 没有虚假唤醒，if 写法也通过（E9）；wait_timeout 不超时；loom 独有的 Notify 每个对象最多伪唤醒一次，同样的 if 写法换成 Notify 第 5 个交错就被抓到（E9 反向）；rt::park 消费预存的 unpark。
3. 线程、线程局部与 lazy_static：spawn 没有 Send 约束；join 恒为 Ok，子线程 panic 直接让模型失败（E15，std 对照）；最多 5 个线程（E12）；thread_local! 每线程一份；lazy_static! 每轮重新初始化，一轮里可能初始化两次（E13 与反向验证），没人 join 的线程碰它会报错。
4. Arc、mpsc 与 future：Arc 的三种动作与依赖关系；mpsc 每条消息一个同步点；发送方全部 drop 后 recv 被报成死锁、接收方 drop 后 send 被报成消息泄漏；recv_timeout 与 Barrier 是调用即 panic 的桩；block_on 与 AtomicWaker 抓丢唤醒（E18）。

和 std 的语义差别一览

每一项都标出方向：假阳性是 loom 报错而代码在真实环境里没问题；假阴性是代码有问题而 loom 通过。汇总见 07 能力边界。

本部分的实验

所有实验都用 RUSTFLAGS="--cfg loom" cargo test --release --offline、单独的 target 目录；会 abort 的场景每个单独一个 #[test]，逐个 --exact 运行。交错数是确定的，与机器负载无关。