干扰自由 | Codeboy's Blog

形式陈述

给定状态谓词 $P$ 与环境一步关系 $R$ ，称 $P$ 对 $R$ 稳定，若

\operatorname{stable}(P,R) \quad\Longleftrightarrow\quad \forall s,s'.\;P(s)\land R(s,s')\Rightarrow P(s').

在 Owicki–Gries 风格的并发证明中，每个线程都有带控制点断言的顺序证明纲要。设 $Q$ 是线程 $i$ 某个控制点的断言， $a$ 是另一线程 $j$ 的一个原子动作， $\operatorname{pre}(a)$ 是执行 $a$ 前该线程纲要保证的断言。干扰自由要求对每个 $i\ne j$ 、每个这样的 $Q$ 与 $a$ 都证明

\{Q\land\operatorname{pre}(a)\}\ a\ \{Q\}.

这里的 Hoare 三元组不是只检查动作自己的后置，而是在动作实际可能启用的状态中检查另一线程事实是否幸存。若 $a$ 有多个原子分支，每个分支都要覆盖；若一条高级语句可在中间被抢占，就必须拆成多个动作和控制点，不能把整段代码塞进一个大括号逃避交错。

$\operatorname{pre}(a)$ 应来自动作所在控制边的完整证明状态，包括 guard、程序计数器和已建立的 ghost 事实。把它弱化成 $\mathsf{true}$ 仍然可靠却可能让义务难以证明；把它任意加强则可能排除动作真实可执行的状态，造成不可靠的“无干扰”结论。

直觉

顺序证明默认“我刚建立的事实在下一行之前不会被别人改掉”。共享内存把这个默认撕开：本线程停在两个指令之间时，其他线程可以任意走许多步。干扰自由逐一审查这些外来步，确认它们不会推翻当前控制点依赖的断言。

它比“两个线程不写同一变量”更精确。变量不相交当然足以消除许多干扰，但两个动作也可以共同修改计数器并仍然保持“计数器非负”；反过来，一个线程只改变量 $x$ ，也可能破坏另一线程关于 $x+y$ 的关系。真正的判据是断言在转移关系下是否闭合，而不是变量名是否重合。

例子与边界

令断言

P(x,y)\equiv x\le y.

环境动作 $a_y$ 为 y := y + 1。从 $x\le y$ 可推出 $x\le y+1$ ，所以

\{x\le y\}\ a_y\ \{x\le y\}

有效。动作 $a_x$ 为 x := x + 1 时则不稳定：状态 $(x,y)=(4,4)$ 满足前置，执行后得到 $(5,4)$ ，直接否定 $P$ 。若 $a_x$ 只有在 guard $x<y$ 下启用，那么整数离散性给出 $x+1\le y$ ，相应义务

\{x\le y\land x<y\}\ a_x\ \{x\le y\}

恢复有效。这个例子也说明动作的控制前断言不是装饰条件，它可以精确排除伪干扰。

边界在原子粒度。若 if x<y then x:=x+1 的测试和写入是两个可交错步骤，另一线程可能在二者之间减小 $y$ ；把它当成单个动作得到的证明便不适用于实现。干扰自由只是一项安全条件：它不会说明锁最终可得、线程不会饿死或并行程序一定终止。环境动作集合若漏掉中断、回调或异常清理，同样会产生不完整结论。

断言也必须覆盖所有会被后续局部证明使用的控制点，而不只是线程入口与出口。某个外来动作可能保持最终目标，却破坏本线程下一条赋值所需的中间前置；等本线程继续执行时错误才显现。proof outline 的细粒度正是为了在这个暂停位置捕获干扰。

推论与应用

干扰自由把若干顺序 proof outline 连接成并发安全证明，是 Owicki–Gries 方法的全局检查阶段。依赖—保证推理把外来动作概括为 rely 关系，再以另一组件的 guarantee 兑现；并发分离逻辑则用所有权排除大批根本无法访问本地资源的动作。三者处理的是同一类稳定性问题，却采用不同的模块边界。

实际验证器可以把每个 action/assertion 对编码成验证条件。数量可能随线程和控制点成平方增长，因此减少原子动作、寻找共享归纳不变式或使用更组合化的规格会影响可扩展性。不过合并动作必须尊重真实抢占边界；为了少几个公式而虚构原子块，会改变被证明的程序。

稳定性具有逐步归纳用途：若 $P$ 对环境的每个一步关系都稳定，那么任意有限串环境步骤后仍有 $P$ 。无限执行中的安全结论也由所有有限前缀得到；“环境最终停止干扰”则是额外活性假设，不能从逐步稳定性推出。

参考资料

Susan Owicki and David Gries, “An Axiomatic Proof Technique for Parallel Programs I,” Acta Informatica 6, 1976, pp. 319–340。
Susan Owicki and David Gries, “Verifying Properties of Parallel Programs: An Axiomatic Approach,” Communications of the ACM 19(5), 1976, pp. 279–285。
Krzysztof R. Apt, Frank S. de Boer, and Ernst-Rüdiger Olderog, Verification of Sequential and Concurrent Programs, 3rd ed., Springer, 2009, Chs. 8–10。

形式陈述 ​

反向链接

形式陈述