Owicki–Gries 方法

方法把困难分为“自己走路是否正确”和“别人从身边经过时路标会不会倒”两部分。局部纲要仍使用熟悉的顺序 Hoare 推理；全局检查则把调度器可能插入的每个外来动作当成一次断言稳定性测试。这样无需枚举完整交错树，却仍逐项覆盖交错造成的风险。

代价是证明纲要并不真正模块化。新增一个线程，会给其他每份纲要增加一批非干扰义务；改变某个控制点断言，也可能迫使全局重查。辅助变量可以记录逻辑进度，让不可见的控制事实进入不变式，但它们必须是保守的 ghost：擦除后原程序行为不变，不能偷偷替程序作调度决定。

经典辅助变量规则通常要求 ghost 赋值不影响真实变量的计算或控制，并能从增广执行中擦除而得到原执行。ghost 可以与一个真实原子动作同步更新，用于记录该动作已发生；若单独增加可被调度观察的 ghost 步，还要说明这些停顿不会改变待证历史与终止性质。

初态为 $x=0,d_1=d_2=0$，其中 $d_1,d_2$ 是取值 $0$ 或 $1$ 的 ghost 标志。线程 $i$ 恰好一次原子执行

< x := x + 1; d_i := 1 >

并且动作前有 $d_i=0$。取共享断言

动作 1 把 $x$ 和 $d_1$ 同时增加一，因此

动作 2 的计算对称。二者都保持 $I$，也保持另一个尚未执行线程的 guard 信息；两个出口标志均为 $1$ 时，$I$ 给出 $x=2$。这里不是靠“递增可交换”一句话，而是用 ghost 进度把最终计数与已完成动作一一对应。

若尖括号内两条赋值实际可被抢占，执行 x:=x+1 后、设置 $d_i$ 前会暂时出现 $x\ne d_1+d_2$。此时必须增加中间控制断言并把暂存进度纳入不变式，或由真实锁证明这两步原子；继续沿用大原子块会证明另一个程序。辅助标志也不得参与真实分支，否则擦除它们可能改变可见轨迹。

非干扰检查还包括另一线程动作对 $d_i=0$ 这类控制断言的影响。在本例中线程 2 保持 $d_1$、线程 1 保持 $d_2$，所以相应义务成立；若两个线程都能重置同一个完成标志，仅证明共享等式 $I$ 保持并不足以推出每个线程“恰好执行一次”。

方法仍不证明死锁自由、公平或终止。即使所有断言在每一步都保持，调度器也可以永远不运行某个线程；需要总正确性或时序推理另行处理。

Owicki–Gries 方法适合线程数固定、原子动作明确的共享变量算法。互斥协议、短并行循环和带 ghost program counter 的细粒度算法都可用它把安全性质还原成顺序验证条件。工具可以自动枚举跨线程 action/assertion 对，求解器失败时给出具体干扰状态。

当组件要在不同环境中复用时，依赖—保证推理公理库依赖—保证推理Rely-guarantee reasoning · Rely-guarantee method以环境可做的 rely 关系和组件承诺的 guarantee 关系概括干扰，并通过交叉包含组合线程规格。用关系规格替代全局两两检查；当干扰主要来自堆别名时，并发分离逻辑用资源所有权使许多交叉义务在语义上不可能发生。这些后续方法没有取消原子性和稳定性责任，而是把它们放进更局部的接口。