Distributive Laws for Parallel Composition in Rely-Guarantee Concurrency

技術要約：Rely-Guarantee 並行性における並行合成のための分配法則

問題提起
Rely/Guarantee アプローチは、共有メモリ並行プログラムの正当性を、干渉仮定（rely）とコミットメント（guarantee）を組成的な特性へと分解することで推論するための確立された手法である。分配法則は、数学やホーア論理におけるプログラムの代数的操作において基本的であるが、Rely/Guarantee フレームワーク内での並行プログラムへの適用は複雑である。具体的には、Guarantee 条件と Rely 条件を並行合成（$c_1 \parallel c_2$）に対していつ、どのように分配できるかを決定するための厳密な代数理論が必要とされている。先行研究では、逐次合成および反復に関する分配法則が確立されているが、これらを並行合成（$c_1 \parallel c_2$）へと拡張することには課題がある。特に、Guarantee 条件は並行合成に対して分配可能であるが、Rely 条件は一般に分配できない。これは、干渉仮定のスコープ（グローバルな環境 vs 特定のスレッド間の相互作用）の違いによるものである。本論文は、Rely および Guarantee コマンドを含む並行合成のための精密な分配法則を導出するための、統一された代数的フレームワークの開発という空白を埋めるものである。

手法
著者らは、**弱クオンタール（weak quantales）および弱バイクオンタール（weak biquantales）**にテストと原子コマンドを付加した構造を持つ、**並行リファインメント代数（Concurrent Refinement Algebra: CRA）**に基づく理論を開発している。この手法は以下の3つの段階で進行する：

1. 抽象代数基盤： 理論はまず、高度に抽象的な「同期原子代数」において展開される。コマンドは、逐次合成（$;$）、並行合成（$\parallel$）、および弱論理積（$\sqcap$）の演算を持つ完全分配束の要素としてモデル化される。このフレームワークは、原子コマンド（不可分な遷移）と疑似原子コマンド（中断する可能性があるコマンド、 $a \lor b; \top$ で表される）を区別する。
2. 一般的な分配法則の導出： 著者らは、原子コマンドの反復 $a^\omega$ が並行合成に対してどのように分配されるかについての条件を調査する。彼らは、原子コマンドが並行合成に関して冪等である（$a = a \parallel a$）ことと、等式 $a^\omega \sqcap (c_1 \parallel c_2) = (a^\omega \sqcap c_1) \parallel (a^\omega \sqcap c_2)$ が成立することは同値であることを証明する。この証明には以下を用いる：
   • 有限近似： 有限の長さ $i$ までのコマンドの解析。
   • 極限閉包： 原子コマンドの無限反復が極限閉（有限近似のインフィマムに等しい）であることを証明すること。
   • 超コンパクト性： コマンドの格子が「超代数的（super-algebraic）」であると仮定し、任意のコマンドを超コンパクト（決定論的で中断しない）なコマンドの選択へと分解することを可能にする。
3. Rely/Guarantee への適用： 抽象的な結果は、プログラム遷移（$\pi$）と環境遷移（$\epsilon$）を通じてコマンドが定義される**アツェル代数（Aczel algebra）**においてインスタンス化される。
   • Guarantee コマンド（$\text{guar}_\pi g$）は、$(\pi g \lor \epsilon \text{univ})$ の無限反復として定義される。
   • Rely コマンド（$\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$ であることを確立した。
• Guarantee 分配の妥当性： 基底コマンド $\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)$$
  これにより、Guarantee 条件が並行合成に対して分配可能であることが確認された。
• 純粋な Rely 分配の不成立： 著者らは、Rely の基底コマンド $\pi \text{univ} \lor \epsilon r \lor \epsilon \bar{r}; \top$ が（$r$ がユニバーサルでない限り）冪等条件を満たさないことを示している。その結果、並行合成に対する Rely の一般的な分配法則は成立しない：
  $$\text{rely } r \sqcap (c_1 \parallel c_2) \neq (\text{rely } r \sqpacking c_1) \parallel (\text{rely } r \sqcap c_2)$$
  これは、左側の Rely が環境全体からの干渉を仮定しているのに対し、右側の Rely はペア内の「もう一方のスレッド」からの干渉のみを考慮していることに起因する。
• 複合分配（Evolve Invariant）： 著者らは、Rely と Guarantee が組み合わされた複合コマンド、具体的には「エボルブ・インバリアント（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)$$
  これは、Guarantee 条件が並行合成全体にわたって Rely 条件が満たされることを保証するためである。
• 疑似原子コマンド： 理論は、中断する可能性があるコマンド（疑似原子コマンド）を扱うように拡張されており、中断成分に関する特定の条件の下で同様の分配特性が保持されることが示されている。

意義と主張
本論文は、Rely/Guarantee 並行性に特化した並行合成のための分配法則の最初の代数的導出を提供することを主張している。Isabelle/HOL において理論を形式化することにより、著者らは提示された補題と証明の正当性を保証している。

その意義は、並行プログラムの段階的な代数的開発を可能にすることにある。Guarantee 条件を並行合成に対して分配できる能力により、開発者は複雑な並行システムをローカルな Guarantee を持つコンポーネントへと分解して推論できるようになり、検証を簡素化できる。本論文は、最も一般的な法則はリファインメント（一方向的）であるが、コマンドの形式（例：Guarantee や特定の Rely/Guarantee の組み合わせ）を制限することで、より強い等式法則が得られることを明記している。本研究は、抽象的な代数構造（クオンタール）と実用的な並行推論（Rely/Guarantee）の間の溝を埋め、並行な仕様を操作するための厳密な基礎を提供するものである。著者らは、すべての並行検証問題を解決すると主張しているのではなく、Rely/Guarantee 推論という特定の領域のための不可欠な代数的ツールを提供しているのである。