偏序约简

动作独立关系 ​

设 $T$ 是动作集合。按动作独立与交换公理库动作独立与交换Action independence · Commuting actions · 动作交换性两个转移动作在共同使能时不会互相禁用且交换执行顺序不改变结果的语义关系。的状态语义，关系 $I\subseteq T\times T$ 对称且无反射；对每个 $(a,b)\in I$ 和每个可达状态 $s$，若 $a,b$ 在 $s$ 都使能，则执行任一动作后另一仍使能，并且

$$a(b(s))=b(a(s))$$

两条组合路径都已由使能性条件保证有定义。未落入 $I$ 的动作对视为依赖；这种保守判定可能少做约简，却不会因错误交换而漏掉行为。

若两个线程只写不同局部变量，动作可能独立；若都访问同一锁、一个写另一个读同一变量，或一个动作抛异常改变控制流，就可能依赖。

独立动作的相邻次序可交换，许多全序 interleaving 因而代表同一个偏序执行。happens-before公理库Happens-before 关系Happens-before · Causal order由进程内顺序与消息传递生成的事件因果严格偏序。保留因果与同步边，而不是强迫无关事件排序。

两线程交错 ​

线程 P 执行局部赋值 $p_1,p_2$，线程 Q 执行局部赋值 $q_1,q_2$。保留线程内次序时共有六种交错，例如

$$p_1{p}_2{q}_1{q}_2,p_1{q}_1{p}_2{q}_2,q_1{q}_2{p}_1{p}_2.$$

若所有跨线程动作独立，这些路径经相邻交换相互可达，最终全局状态相同。探索一个代表便足以检查不观察中间排序的安全性质。

若 $p_2$ 与 $q_1$ 都写共享 x，交换会改变最终值，二者必须保留不同次序。按“属于不同线程”直接判独立会漏竞态反例。

ample set 选择 ​

在状态 $s$，完整使能集为 $enabled(s)$。POR 选择子集 $ample(s)$ 探索。若 $ample(s)=enabled(s)$，没有约简；选真子集时要满足依赖闭包、不可见性和 cycle proviso 等条件。

核心依赖条件直观上要求：任何未选动作在未来第一次与所选动作发生依赖之前，不能越过它改变结果。否则推迟未选动作可能丢掉必要排序。

对保持 stutter-invariant 性质，若选集不完整，其中动作通常需对被检查原子命题不可见。一个动作虽与其他动作交换，却直接改变 bad 标记，跳过其时机可能改变性质。

cycle proviso ​

若每个状态都只选择某个持续可用动作，搜索可能沿环永远忽略另一个动作，造成 artificial starvation。cycle proviso 要求 DFS 环上不能永久推迟未探索的使能动作。

例如状态 $s$ 有自环 $a$ 与通往错误的动作 $b$。若每次选 $ample(s)=\{a\}$，约简图只见安全自环，漏掉 $b$。$a,b$ 即使局部交换，循环条件仍必须强制某处探索 $b$。

保存 safety/deadlock 的条件与保存 liveness/fairness 的条件不完全相同。把用于无环可达性的简化 ample 规则直接用于 Büchi 接受环，会丢失公平反例。

动态与静态依赖 ​

静态分析可按变量读写集合保守判断依赖：若可能冲突就视为 dependent。过保守只减少约简，误判独立则破坏 soundness。

动态 POR 利用当前执行的具体地址、锁和分支，发现更多实际独立性，并通过 backtracking sets 补探索必要替代顺序。算法状态不仅含程序状态，还含已观察依赖和回溯点。

对象身份、别名和弱内存语义会使依赖判断更难。顺序一致下可交换的两次读写，在特定内存模型上可能通过可见重排影响观察，不能无证明复用关系。

约简保证边界 ​

POR 减少路径或状态探索，不改变单步执行成本。高度同步程序中依赖密集，约简可能很小；组件局部性强时收益可接近阶乘级。

选择条件必须相对于待验证性质声明。若性质观察动作顺序、计数每次调度或含 next，普通 stutter-preserving POR 不一定适用。

睡眠集合与重复前缀 ​

sleep-set 方法在 DFS 节点记录一组当前可跳过的动作：它们已在某个等价前缀中探索，并与此后交换过的动作独立。执行一个动作后，依赖于它的睡眠项必须移除，仍独立的项才可继承。

若把 sleep set 只按程序状态缓存，不考虑到达路径，可能在新前缀中错误跳过尚未探索的次序；若从不继承，则仍正确但几乎没有约简。该辅助集合是搜索历史，不属于程序语义状态，却参与算法正确性不变量。

源代码级依赖还需处理动态线程创建：新线程动作与既有动作的关系在创建前不存在，不能用静态固定矩阵覆盖全部执行。

参考资料

• Patrice Godefroid, Partial-Order Methods for the Verification of Concurrent Systems, LNCS 1032, Springer, 1996；Chapter 3（尤其 §§3.1–3.4）定义动作独立、trace 与独立性检测，Chapters 4–5 分别给出 persistent sets 与 sleep sets。
• Doron Peled, “Combining Partial Order Reductions with On-the-Fly Model-Checking,” CAV, LNCS 818, 1994, pp. 377–390；定位 ample-set 依赖条件、不可见性要求与 cycle proviso。
• Antti Valmari, “A Stubborn Attack on State Explosion,” CAV 1990, LNCS 531, Springer, 1991, pp. 156–165；给出 stubborn-set 的原始选择条件及死锁保持目标。
• Cormac Flanagan and Patrice Godefroid, “Dynamic Partial-Order Reduction for Model Checking Software,” POPL, 2005, pp. 110–121，§§2–3；用执行中观察到的依赖关系和 backtracking points 构造 DPOR。