动作独立与交换

形式陈述 ​

本页先采用偏序约简中最常见的确定性动作粒度：每个动作标签已经细化为状态上的确定性偏变换。在标号转移系统公理库标号转移系统Labeled transition system · Labelled transition system · LTS在状态转移上标记动作，明确路径、可达性、使能动作以及终止与死锁的行为模型。的状态 $s$ 上执行动作 $a$ 后到达唯一状态 $a(s)$；若 $a$ 在 $s$ 不可执行，则 $a(s)$ 未定义。动作集合 $T$ 上的独立关系

$$I\subseteq T\times T$$

通常要求对称且反自反。对任意 $(a,b)\in I$ 和任意可达状态 $s$，只要 $a,b$ 在 $s$ 同时使能，就应满足两项条件：

1. 使能保持：执行 $a$ 后 $b$ 仍使能，执行 $b$ 后 $a$ 仍使能；
2. 交换性：两种次序都到达同一状态，亦即 $b(a(s))=a(b(s))$。

第一项不能由第二项省略。若某一次序中第二个动作根本无法执行，就不存在两条完整路径可供比较；仅仅发现另一条路径偶然到达相同终态，不足以判定独立。未进入 $I$ 的动作对构成依赖关系 $D=(T\times T)\setminus I$。把不确定的动作保守地列为依赖只会减少约简，把真实依赖误判为独立却会合并本应分别检查的行为。

这里的“独立”描述转移之间的语义干扰，与概率论中随机事件满足 $P(A\cap B)=P(A)P(B)$ 的概率独立性公理库独立性Statistical independence若干 σ-代数的任意有限事件选择都按概率乘积分解的性质。无关。前者问执行次序能否安全交换，后者问联合分布能否分解；名称相同不意味着可以互作前置或证明工具。

直觉 ​

两个动作独立，意味着它们各自处理不同的那部分世界：先做哪一个都不会挡住另一个，也不会留下不同结果。可以把它想成两个人分别在文档的不同段落改字。交换提交顺序后，最终文档相同，任何一人的修改也不会使另一人的修改失去适用位置。

“最后结果碰巧一样”比独立弱得多。两个事务都先检查余额再更新，某组输入上可能恰好写回同一个数，但一次读到的中间值已经可能改变另一次决策；这种动作不能因为一个样例同终态就视为可交换。独立性必须覆盖规定范围内的所有可达共同使能状态，而不是从单条运行归纳。

例子与反例 ​

线程 P 写自己的局部变量 p，线程 Q 写自己的局部变量 q。若这些位置不别名，两个赋值彼此不改变使能条件，先 P 后 Q 与先 Q 后 P 都得到同一对值，因此可以列入 $I$。两个只读动作访问同一不可变对象时通常也可交换，尽管它们触及相同地址。

若 $a$ 写 x 而 $b$ 读 x，执行顺序可能改变 $b$ 的返回值；若二者都争用同一把锁，先取得锁的动作会暂时禁用另一个；若一个动作关闭文件而另一个读取文件，关闭会直接改变读取是否可执行。这三类分别破坏结果交换、使能保持或两者，因此都属于依赖。

异常和控制流同样属于状态。动作 $a$ 修改除数，动作 $b$ 随后可能从正常返回变成抛出异常；即使两个分支最后都被外层处理成同一个错误码，中间可观察事件已经不同。判断独立时必须使用性质实际观察的状态和标签，不能只比较被过度投影的终值。

静态关系与动态关系 ​

最简单的静态分析用读写集合判定：两个动作若访问集合不冲突，就视为独立；只要可能别名或涉及未知调用，就保守判为依赖。这种关系一次计算后可用于全部状态，容易验证，但数组下标、对象身份和分支条件不够精确时会丢掉大量可交换机会。

动态独立性可以引用一次具体执行中的地址、锁和分支。例如两条同为 write(a[i]) 的语句，在本次运行中下标不同便可能交换；换一组输入后下标相同又会依赖。此时关系属于事件实例而非粗粒度动作标签，缓存或迁移结论时必须连同产生判断的状态条件保存。

若原始 LTS 允许同一状态与标签有多个后继，就不能用单值记号 $a(s)$ 偷换模型。此时可以把具体转移实例细化成动作，重新获得偏变换语义；也可以直接要求任意 $a$-后继与 $b$-后继都能补成标签交换的菱形，并明确采用强交换还是只要求存在匹配后继。两种版本给出的独立关系未必相同，约简证明必须沿用实际声明的版本。

弱内存还会改变动作语义。在顺序一致模型中互不干扰的源代码读写，经编译器或硬件重排后可能通过可见性影响另一线程。要在弱内存验证中宣称独立，需要对模型允许的传播、屏障和原子顺序证明交换性，不能直接复用源代码级的不同变量判据。

推论与应用 ​

独立动作可以反复作相邻交换，由此把多个全序交错归入同一等价类。Mazurkiewicz trace公理库Mazurkiewicz traceMazurkiewicz trace · Trace monoid · Partially commutative word以独立动作的相邻交换对执行词取商，使一个 trace 表示同一因果偏序的全部交错。把这件事抽象为词的商结构；偏序约简公理库偏序约简Partial-order reduction · POR · Ample-set reduction利用独立并发动作的可交换性只探索等价交错代表，并以 proviso 保存死锁与时序性质。则在搜索中只保留足够的代表交错，避免为无关动作的排列重复探索同一行为。

局部交换并不独自保证任意性质都被保存。若规格直接观察动作先后、使用 next 运算符，或要求无限执行中的公平性，即使终态一致，也可能区分两个排列。约简算法因此还要结合动作可见性、cycle proviso 与待验证性质说明保存范围；动作独立关系只提供可交换的语义基础，不包办完整约简证明。

参考资料

• Antoni Mazurkiewicz, “Trace Theory,” in Petri Nets: Applications and Relationships to Other Models of Concurrency, Springer, 1987, pp. 278–324。
• Patrice Godefroid, Partial-Order Methods for the Verification of Concurrent Systems, Springer, 1996, Chapters 2–3。
• Cormac Flanagan and Patrice Godefroid, “Dynamic Partial-Order Reduction for Model Checking Software,” POPL, 2005, pp. 110–121。