PhaseGuard

展开

在 Hopper / Blackwell 上，TMA 写 smem、tcgen05 直读 smem 直写 tmem 这样的异步操作，存在一类 race：冲突双方可以都不是线程指令，compute-sanitizer racecheck 对此没有观测点；而且它万倍慢化会系统性关掉竞争窗口——删掉一条协议必需的同步边，12 runs × 4 shapes 全 PASS。

PhaseGuard 的做法是把执行主体 × 地址区域 × phase/计数状态 × 完成谓词代数抽成 phase-automaton，从源码静态提取，然后有界穷举判定。输出模型是 model-level SAFE / exact J_K REFUSED / source-level INCONCLUSIVE。

已冻结面：CUTLASS SM90/SM100（12 个准入源文件、16 个 collective implementation、20 条 protocol-bearing pipeline、9 个具体 operation、2 个 protocol class）+ FlashAttention-3。野外分布做过验证：CUTLASS/FA 历史 8 个真实修复全落在这个分类格子里，tmem 生命周期占 3 个。

这条线和 ProofWeaver 是同一枚硬币的两面：PhaseGuard 是底座（静态提取协议），ProofWeaver 是它的 agent 应用面（给不可信 agent 的产出做 fail-closed 判定）。

方法

phase-automaton 的有界穷举：状态空间按 (subject × address region × phase/counter state × completion predicate) 切分；从 source-level 静态提取后，把所有可能调度折叠为有限状态机，遍历判定 race 是否可达。Idiom 之外 fail closed 是显式语义而不是工程倾向。