Distributive Laws for Parallel Composition in Rely-Guarantee Concurrency

技术摘要：并行组合中的分配律（用于依赖/保证并发推理）

问题陈述
依赖/保证（rely/guarantee）方法是一种通过将干扰假设（依赖/rely）和承诺（保证/guarantee）分解为组合属性，来对共享内存并发程序进行正确性推理的成熟方法。虽然分配律在数学和 Hoare 逻辑的程序代数操作中是基础性的，但将其应用于依赖/保证框架下的并发程序却非常复杂。具体而言，需要一个严谨的代数理论来确定在何时以及如何将保证和依赖条件分配到并行组合（$c_1 \parallel c_2$）上。以往的工作已经建立了关于顺序组合和迭代的分配律，但将这些扩展到并行组合时面临挑战。值得注意的是，虽然保证条件可以分配到并行组合上，但依赖条件通常不行，这是由于干扰假设的作用域不同（全局环境与特定线程交互之间的差异）。本文旨在填补开发统一代数框架的空白，以推导涉及依赖和保证命令的并行组合的精确分配律。

方法论
作者开发了一种基于**并发细化代数（Concurrent Refinement Algebra, CRA）的理论，该理论使用增强了测试（tests）和原子命令（atomic commands）的弱量子（weak quantales）和弱双量子（weak biquantales）**进行构建。该方法分为三个阶段进行：

1. 抽象代数基础： 该理论首先在一个高度抽象的“同步原子代数”中开发。命令被建模为具有顺序组合（$;$）、并行组合（$\parallel$）和弱合取（$\sqcap$）运算的完备分配格（complete distributive lattice）中的元素。该框架区分了原子命令（不可分割的转换）和伪原子命令（可能中止的命令，表示为 $a \lor b; \top$）。
2. 推导通用分配律： 作者研究了原子命令的迭代 $a^\omega$ 分配到并行组合上的条件。他们证明了等式 $a^\omega \sqcap (c_1 \parallel c_2) = (a^\omega \sqcap c_1) \parallel (a^\omega \sqcap c_2)$ 成立的充分必要条件是该原子命令对于并行组合是幂等的（即 $a = a \parallel a$）。该证明利用了：
   • 有限近似： 分析长度最高为有限值 $i$ 的命令。
   • 极限闭包： 证明原子命令的无限迭代是极限闭合的（等于其有限近似的下确界）。
   • 超紧性（Super-compactness）： 假设命令格是“超代数的”（super-algebraic），允许任意命令分解为对超紧（确定性、非中止）命令的选择。
3. 应用于依赖/保证： 这些抽象结果被实例化在一个 Aczel 代数中，其中命令通过程序转换（$\pi$）和环境转换（$\epsilon$）来定义。
   • 保证命令（$\text{guar}_\pi g$）被定义为 $(\pi g \lor \epsilon \text{univ})$ 的无限迭代。
   • 依赖命令（$\text{rely } r$）被定义为 $(\pi \text{univ} \lor \epsilon r \lor \epsilon \bar{r}; \top)$ 的无限迭代。
   • 作者通过分析这些特定命令形式的 $a = a \parallel a$ 条件来确定其有效性。

核心贡献与结果

• 原子迭代的通用分配律： 本文确立了对于原子命令 $a$，分配律 $a^\omega \sqcap (c_1 \parallel c_2) = (a^\omega \sqcap c_1) \parallel (a^\omega \sqcap c_2)$ 成立的充要条件是 $a = a \parallel a$。
• 保证分配的有效性： 通过证明保证的基础命令 $\pi g \lor \epsilon \text{univ}$ 满足幂等性条件（因为 $g \subseteq \text{univ}$），作者证明了等式：
  $$\text{guar}_\pi g \sqcap (c_1 \parallel c_2) = (\text{guar}_\pi g \sqcap c_1) \parallel (\text{guar}_\pi g \sqcap c_2)$$
  这证实了保证条件可以分配到并行组合上。
• 纯依赖分配的无效性： 作者证明了依赖的基础命令 $\pi \text{univ} \lor \epsilon r \lor \epsilon \bar{r}; \top$ 并不满足幂等性条件（除非 $r$ 是全集）。因此，依赖在并行组合上的通用分配律并不成立：
  $$\text{rely } r \sqcap (c_1 \parallel c_2) \neq (\text{rely } r \sqcap c_1) \parallel (\text{rely } r \land c_2)$$
  这归因于：左侧的依赖假设来自整个环境的干扰，而右侧的依赖仅考虑来自另一对线程的干扰。
• 复合分配（演化不变性）： 本文推导了一个针对结合了依赖和保证的复合命令的更强等式，即“演化不变性”（evolve invariant）命令（$\text{evolve } r \equiv \text{rely } r \sqcap \text{guar}_\pi r$）。如果 $g \subseteq r$，则以下等式成立：
  $$\text{rely } r \sqcap \text{guar}_\pi g \sqcap (c_1 \parallel c_2) = (\text{rely } r \sqcap \text{guar}_\pi g \sqcap c_1) \parallel (\text{rely } r \sqcap \text{guar}_\pi g \sqcap c_2)$$
  这是有效的，因为保证条件确保了在并行组合中满足依赖条件。
• 伪原子命令： 该理论被扩展到了处理伪原子命令（可能中止的命令），表明在涉及中止组件的特定条件下，类似的分配性质仍然成立。

意义与主张
本文声称提供了第一个专门为依赖/保证并发量身定制的并行组合分配律的代数推导。通过在 Isabelle/HOL 中将理论形式化，作者确保了所呈现的引理和证明的正确性。

其意义在于能够实现并发程序的逐步代数开发。将保证条件分配到并行组合上的能力，使开发者能够通过将复杂并发系统分解为具有局部保证的组件，从而简化验证过程。本文明确指出，虽然最一般的定律是细化关系（单向的），但通过限制命令的形式（例如使用保证或特定的依赖/保证组合），可以获得更强的等式定律。这项工作架起了抽象代数结构（量子）与实际并发推理（依赖/保证）之间的桥梁，为操作并发规范提供了严谨的基础。作者并非声称解决了所有并发验证问题，而是为依赖/保证推理这一特定领域提供了必不可少的代数工具。