tla+ 不能直接验证 c++ 代码，需手动将并发逻辑抽象为状态变量、动作和不变式；建模对象是算法逻辑而非实现细节，常见断连点包括内存序忽略、未定义行为未建模和时间维度丢失。
TLA+ 不能直接验证 C++ 代码
TLA+ 不是静态分析器，也不是能读取 .cpp 文件的工具。它不解析 C++ 语法，不运行你的 std::atomic 或 std::mutex，更不会插桩或生成测试用例。你写的 C++ 并发逻辑，必须先手动抽象成一组状态变量、动作和不变式——这个过程叫「建模」，不是「接入」。
常见错误现象：TLA+ spec type-checks but never finds the race I saw in CI，原因往往是模型漏掉了某个调度路径，或把非确定性操作（比如线程启动顺序）写成了确定性赋值。
- 建模对象是「算法逻辑」，不是「C++ 实现细节」：比如用
pc[i] ∈ {"idle", "waiting", "critical"}表示线程 i 的控制流位置，而不是跟踪std::thread::id或栈帧 - 所有共享状态必须显式声明为 TLA+ 变量（
vars），且初始值需覆盖所有可能起点（比如counter = 0不能默认，要写进Init） - 非阻塞算法中，
compare_exchange_weak的失败分支必须建模为单独的Next动作分支，否则 TLC 会跳过重试路径
用 TLC 检查 C++ 并发算法的典型建模模式
以 Peterson 算法或 Bakery 算法为例，关键不是“怎么写 C++”，而是“怎么让 TLA+ 覆盖最坏调度”。TLC 的穷举本质决定了：只要模型里允许某个交错（interleaving），它就一定会尝试。
使用场景：验证无锁队列的线性化点、自旋锁的死锁自由、多生产者单消费者的 ABA 抵抗能力。
-
Next必须包含所有可能的原子动作，包括「线程休眠」「CAS 失败」「load-acquire 返回旧值」——这些都得写成显式条件分支 - 用
ENABLED配合UNCHANGED控制动作是否可执行，避免 TLC 因无效动作爆炸（比如不让线程在critical = TRUE时再次进入临界区） - 性能影响：若用
CHOOSE模拟非确定性选择（如哪个线程先执行），TLC 会枚举所有选择；改用∃+ 辅助变量更可控
TLA+ 和 C++ 实现之间最容易断连的三个地方
模型通过了，C++ 还出 bug，八成卡在这三处。不是 TLA+ 不行，是映射没对齐。
- 内存序被忽略：
memory_order_relaxed在模型里对应「无同步约束」，但很多人建模时默认所有读写都带acquire/release，导致模型比实际更严格 - 未定义行为未建模：比如
int* p = nullptr; *p = 42;在 C++ 是 UB，但在 TLA+ 里如果没禁止p = NULL后的写操作，TLC 就不会报错 - 时间维度丢失：C++ 中两个原子操作的「实际间隔」可能影响硬件重排，但 TLA+ 只关心状态跃迁顺序。若算法依赖「某操作在 100ns 内完成」，TLA+ 根本无法表达
从 TLA+ 模型到 C++ 实现的校验建议
别指望一次建模就覆盖全部。重点是让每次修改 C++ 时，都能快速回答：这个改动是否破坏了模型里的某个不变式？
- 把模型里的每个
Inv（不变式）转成 C++ 断言注释，比如// INV: counter ≥ 0 ∧ counter ≤ max_allowed，写在相关函数顶部 - 用
assert或 sanitizer 捕获模型中已排除的非法状态（如pc[i] = "critical" ∧ pc[j] = "critical"），这类断言在 release 模式可关，但开发阶段必须开 - TLC 报错的反例（
counter = -1）要人工翻译成最小复现 C++ 片段，验证它是否真能触发——如果不能，说明模型过度简化了调度假设
真正难的从来不是写 Spec == Init ∧ [Next]_vars，而是决定哪些细节该放进 vars，哪些该当作环境噪声扔掉。这个权衡点，没有工具能帮你划。
C++免费学习笔记（深入）：立即使用
在学习笔记中，你将探索 C++ 的入门与实战技巧！
