分離ロジック

コンピュータサイエンスにおいて、分離論理^[1]は、プログラムについての推論方法であるホーア論理の拡張です。これは、ロッド・バーストールの初期の研究を参考にして、ジョン・C・レイノルズ、ピーター・オハーン、サミン・イシュティアク、ホンソク・ヤンによって開発されました^{[1] [2] [3] [4]}。分離論理のアサーション言語は、束ねられた含意の論理(BI)の特殊なケースです。 ^{[6]オハーン}によるCACMレビュー記事は、2019年初頭までのこの分野の発展を示しています。^[7]

分離ロジックにより、次の点についての推論が容易になります。

• ポインタデータ構造を操作するプログラム（ポインタの存在下での情報の隠蔽を含む）。
• 「所有権の移転」 （意味フレーム公理の回避）；そして
• 同時実行モジュール間の仮想分離（モジュール推論）。

分離論理は、ピーター・オハーンらがローカル推論と呼んでいる発展途上の研究分野をサポートします。ローカル推論では、プログラム コンポーネントの仕様と証明で、コンポーネントが使用するメモリの部分のみに言及し、システムの全体的なグローバル状態には言及しません。アプリケーションには、自動プログラム検証(アルゴリズムが別のアルゴリズムの有効性をチェックする) やソフトウェアの自動並列化などがあります。

分離ロジックアサーションは、ストアとヒープで構成される「状態」を記述します。これは、 CやJavaなどの一般的なプログラミング言語のローカル(またはスタックに割り当てられた) 変数と動的に割り当てられたオブジェクトの状態にほぼ相当します。ストアは、変数を値にマッピングする関数です。ヒープは、メモリアドレスを値にマッピングする部分関数です。2 つのヒープと は、それらのドメインが重複していない場合 (つまり、すべてのメモリアドレス について、との少なくとも 1 つが未定義の場合)、互いに素です( と表記) 。 ${\displaystyle s}$${\displaystyle h}$${\displaystyle h}$${\displaystyle h'}$${\displaystyle h\,\bot \,h'}$${\displaystyle \ell }$${\displaystyle h(\ell )}$${\displaystyle h'(\ell )}$

このロジックにより、形式 の判断を証明できます。ここで、はストア、はヒープ、 は指定されたストアとヒープ上のアサーションです。分離ロジック アサーション ( 、、と表記)には、標準のブール接続子に加えて、、、、およびが含まれます。ここで、 と は式です。 ${\displaystyle s,h\models P}$${\displaystyle s}$${\displaystyle h}$${\displaystyle P}$${\displaystyle P}$${\displaystyle Q}$${\displaystyle R}$${\displaystyle \mathbf {e} \mathbf {m} \mathbf {p} }$${\displaystyle e\mapsto e'}$${\displaystyle P\ast Q}$${\displaystyle P{-\!\!\ast }\,Q}$${\displaystyle e}$${\displaystyle e'}$

• この定数は、ヒープが空である、つまり、すべてのアドレスに対して が未定義であることを示します。${\displaystyle \mathbf {e} \mathbf {m} \mathbf {p} }$${\displaystyle s,h\models \mathbf {e} \mathbf {m} \mathbf {p} }$${\displaystyle h}$
• バイナリ演算子は、アドレスと値を受け取り、ヒープが正確に 1 つの場所で定義され、指定されたアドレスが指定された値にマッピングされることをアサートします。つまり、(ここで、はストアで評価された式の値を示します)の場合はであり、それ以外の場合は未定義です。${\displaystyle \mapsto }$${\displaystyle s,h\models e\mapsto e'}$${\displaystyle h([\![e]\!]_{s})=[\![e']\!]_{s}}$${\displaystyle [\![e]\!]_{s}}$${\displaystyle e}$${\displaystyle s}$${\displaystyle h}$
• 二項演算子(スター演算子または分離接続詞 と発音) は、2 つの引数がそれぞれ成り立つ2 つの別々の部分にヒープを分割できることを主張します。つまり、およびおよびが存在する場合です。${\displaystyle \ast }$${\displaystyle s,h\models P\ast Q}$${\displaystyle h_{1},h_{2}}$${\displaystyle h_{1}\,\bot \,h_{2}}$${\displaystyle h=h_{1}\cup h_{2}}$${\displaystyle s,h_{1}\models P}$${\displaystyle s,h_{2}\models Q}$
• 二項演算子(マジック ワンドまたは分離含意 と発音) は、最初の引数を満たす分離部分でヒープを拡張すると、2 番目の引数を満たすヒープになると主張します。つまり、となるすべてのヒープに対して の場合、 も成り立ちます。${\displaystyle -\!\!\ast }$${\displaystyle s,h\models P-\!\!\ast \,Q}$${\displaystyle h'\,\bot \,h}$${\displaystyle s,h'\models P}$${\displaystyle s,h\cup h'\models Q}$

演算子と演算子は、古典的な連言演算子および含意演算子といくつかの特性を共有しています。これらは、モーダスポネンスに似た推論規則を使用して組み合わせることができます。${\displaystyle \ast }$${\displaystyle -\!\!\ast }$

${\displaystyle {\frac {s,h\models P\ast (P-\!\!\ast \,Q)}{s,h\models Q}}}$

そして、それらは随伴 を形成します。つまり、に対して である場合に限ります。より正確には、随伴演算子はおよびです。 ${\displaystyle s,h\cup h'\models P\ast Q\Rightarrow R}$${\displaystyle s,h\models P\Rightarrow Q-\!\!\ast \,R}$${\displaystyle h\,\bot \,h'}$${\displaystyle \_\ast Q}$${\displaystyle Q-\!\!\ast \,\_}$

分離論理では、ホーア トリプルはホーア ロジックとは少し異なる意味を持ちます。このトリプルは、プログラムが前提条件を満たす初期状態から実行された場合、プログラムはエラーにならず(たとえば、未定義の動作をする)、終了した場合は最終状態が事後条件を満たすと主張します。本質的には、実行中は、前提条件で存在が主張されているメモリ位置、またはそれ自体で割り当てられたメモリ位置にのみアクセスできます。 ${\displaystyle \{P\}\ C\ \{Q\}}$${\displaystyle C}$${\displaystyle P}$${\displaystyle Q}$${\displaystyle C}$${\displaystyle C}$

ホーア論理の標準ルールに加えて、分離論理は次の非常に重要なルールをサポートします。

${\displaystyle {\frac {\{P\}\ C\ \{Q\}}{\{P\ast R\}\ C\ \{Q\ast R\}}}~{\mathsf {mod}}(C)\cap {\mathsf {fv}}(R)=\emptyset }$

これはフレーム規則（フレーム問題にちなんで名付けられました）として知られており、局所的な推論を可能にします。これは、小さな状態（ を満たす）で安全に実行されるプログラムは、より大きな状態（ を満たす）でも実行でき、その実行は状態の追加部分に影響を与えない（したがって事後条件で真のままになる）と述べています。副条件は、 によって変更される変数のいずれも で自由に発生しないこと、つまり の「自由変数」セットに含まれないことを指定することによって、これを強制します。 ${\displaystyle P}$${\displaystyle P\ast R}$${\displaystyle R}$${\displaystyle C}$${\displaystyle R}$${\displaystyle {\mathsf {fv}}}$${\displaystyle R}$

分離論理は、分離結合を使用して簡単に記述できる規則的な共有パターンを示すデータ構造のポインタ操作の簡単な証明につながります。例としては、単方向および二重にリンクされたリストやさまざまなツリーがあります。グラフや DAG など、より一般的な共有を持つ他のデータ構造は、形式的および非形式的証明の両方がより困難です。それでも、分離論理は、一般的な共有を持つプログラムに関する推論にうまく適用されてきました。

POPL'01論文^[3]で、オハーンとイシュティアクは、共有が存在する場合の推論に魔法の杖接続詞をどのように使用できるかを、少なくとも原理的には説明した。例えば、 ${\displaystyle {-\!\!*}}$

${\displaystyle \{(x\mapsto -)\ast ((x\mapsto 42){-\!\!*}P)\}\ [x]=42\ \{P\}}$

位置 にあるヒープを変更するステートメントの最も弱い前提条件が得られます。これは、分離接続詞を使用してきちんとレイアウトされたものだけでなく、任意の事後条件に機能します。このアイデアは、古典的なショール-ウェイトグラフマーキングアルゴリズムで変化についての局所的な推論を提供していたヤンによってさらに発展しました。^[8]最後に、この方向での最新の研究の1つは、HoborとV​​illardによるものです。^[9]彼らは、 だけでなく、重複接続詞またはセピッシュ^[10] とも呼ばれる接続詞も使用します。これは、重複するデータ構造を記述するために使用できます。つまり、 および がサブヒープに対して成り立つとき 、ヒープ が成り立ち、その和集合は ですが、空でない部分が共通している可能性があります。抽象的には、は関連性論理 の融合接続詞のバージョンと見なすことができます。 ${\displaystyle x}$${\displaystyle {-\!\!*}}$${\displaystyle {-\!\!*}}$${\displaystyle \cup \,\!\!\!\!\!*}$${\displaystyle P\cup \!\!\!\!\!*Q}$${\displaystyle h}$${\displaystyle P}$${\displaystyle Q}$${\displaystyle h_{P}}$${\displaystyle h_{Q}}$${\displaystyle h}$${\displaystyle h_{P}\cap h_{Q}}$${\displaystyle P\cup \!\!\!\!\!*Q}$

並行プログラムのための分離論理の一種である並行分離論理（CSL）は、もともとピーター・オハーン^[11]によって提案され、 証明規則を用いている 。

${\displaystyle {\frac {\{P_{1}\}C_{1}\{Q_{1}\}\quad \{P_{2}\}C_{2}\{Q_{2}\}}{\{P_{1}*P_{2}\}C_{1}\parallel C_{2}\{Q_{1}*Q_{2}\}}}}$

これにより、別々のストレージにアクセスするスレッドについて独立した推論が可能になります。O'Hearn の証明規則は、 Tony Hoareの初期の並行性に関する推論へのアプローチを採用したもので、^[12] 分離を保証するためのスコープ制約の使用を分離ロジックでの推論に置き換えました。Hoare のアプローチをヒープに割り当てられたポインターの存在下に適用するように拡張することに加えて、O'Hearn は並行分離ロジックでの推論がプロセス間のヒープ部分の動的な所有権移転を追跡する方法を示しました。論文の例には、ポインター転送バッファーとメモリマネージャーが含まれています。

スーザン・オウィッキとデイヴィッド・グリースによる干渉の自由に関する初期の古典的な研究についてコメントして、オハーンは、証明の構築方法の性質上、彼のシステムは暗黙的に干渉を排除するため、非干渉の明示的なチェックは必要ないと述べています。

並行分離論理のモデルは、オハーンの論文に付随するスティーブン・ブルックスによって初めて提示された。^[13]この論理の健全性は難しい問題であり、実際、ジョン・レイノルズの反例は、この論理の以前の未発表バージョンの不健全性を示していた。レイノルズの例によって提起された問題は、オハーンの論文で簡単に説明されており、ブルックスの論文ではより詳細に説明されている。

当初、CSLはダイクストラが緩く結合したプロセスと呼んだもの^[14]には適しているように見えましたが、干渉が著しい細粒度の並行アルゴリズムには適していないかもしれません。しかし、論理接続子やホーアトリプルの非標準モデルを採用すれば、CSLの基本的なアプローチは当初考えられていたよりもはるかに強力であることが徐々に認識されました。

分離論理の抽象バージョンが提案され、事前条件と事後条件が特定のヒープモデルではなく任意の部分可換モノイド上で解釈される式である Hoare トリプルで機能するようになりました。^[15] その後、可換モノイドを適切に選択することで、並行分離論理の抽象バージョンの証明規則を使用して、干渉する並行プロセスについて推論できることが驚くべきことに判明しました。たとえば、干渉について推論するために最初に提案された依存保証技法をエンコードすることによってです。^[16]この研究では、モデルの要素はリソースではなく、プログラム状態の「ビュー」と見なされ、Hoare トリプルの非標準的な解釈には、事前条件と事後条件の非標準的な読み取りが伴います。最後に、CSL スタイルの原則を使用して、プログラム状態ではなくプログラム履歴についての推論を構成し、細粒度の並行アルゴリズムについて推論するためのモジュール式技法を提供しました。^[17]

CSL のバージョンは、次のセクションで説明するように、多くの対話型および半自動 (または「中間」) 検証ツールに組み込まれています。特に重要な検証作業は、そこで言及されている μC/OS-II カーネルの検証です。しかし、いくつかのステップは踏まれていますが、^[18]現時点では、CSL スタイルの推論は、自動プログラム分析カテゴリの比較的少数のツールに組み込まれています (次のセクションで言及されているものはありません)。

オハーンとブルックスは、並行分離論理の発明により2016年のゲーデル賞を共同受賞した。 ^[19]

プログラムを推論するためのツールは、ユーザー入力を必要としない完全に自動のプログラム分析ツールから、人間が証明プロセスに深く関与する対話型ツールまで多岐にわたります。このようなツールは数多く開発されており、次のリストには各カテゴリの代表的なツールがいくつか含まれています。

• 自動プログラム分析。これらのツールは通常、限定されたクラスのバグ (メモリ安全性エラーなど) を探すか、バグが存在しないことを証明しようとしますが、完全な正しさを証明することはできません。
  • 現在の例としては、 分離論理とバイアブダクションに基づくJava、C、Objective-Cの静的解析ツールであるFacebook Inferがあります。 ^[20] 2015年の時点で、毎月数百のバグがInferによって発見され、Facebookのモバイルアプリに出荷される前に開発者によって修正されていました。 ^[21]
  • その他の例としては、SpaceInvader（最初のSLアナライザーの1つ）、Predator（いくつかの検証コンテストで優勝）、MemCAD（形状と数値プロパティを組み合わせたもの）、SLAyer（Microsoft Research製、デバイスドライバー内のデータ構造に重点を置いたもの）などがあります。
• インタラクティブな証明。証明は、 Coq 証明アシスタントやHOL (証明アシスタント)などのインタラクティブな定理証明器への分離ロジックの埋め込みを使用して行われてきました 。プログラム分析作業と比較すると、これらのツールは人間の労力をより多く必要としますが、機能的な正しさに至るまで、より深い特性を証明します。
  • FSCQファイルシステム^[22]の証明。仕様には、通常の動作だけでなくクラッシュ時の動作も含まれています。この研究は、2015年のオペレーティングシステム原則シンポジウムで最優秀論文賞を受賞しました。
  • Coq 証明アシスタントの分離ロジックに Iris フレームワークを使用して、RustBelt プロジェクトのRust型システムの大部分とその標準ライブラリの一部を検証します。
  • 検証可能なC言語を使用した暗号認証アルゴリズムのOpenSSL実装の検証^[23]
  • 商用OSカーネルの主要モジュールの検証。μC/OS-IIカーネルは、検証された最初の商用プリエンプティブカーネルです。 ^[24]
  • その他の例としては、 Coq証明支援システム用のYnot ^[25]ライブラリ、HOLにおけるSmallfootのHolfoot埋め込み、細粒度並行分離ロジック、Bedrock（低レベルプログラミング用のCoqライブラリ）などがある。
• 中間。多くのツールは、プログラム解析よりもユーザーの介入を必要とします。つまり、ユーザーが関数の事前/事後仕様やループ不変条件などのアサーションを入力することを期待しますが、この入力が与えられた後は、完全にまたはほぼ完全に自動化しようとします。この検証モードは、J King の検証器や Stanford Pascal 検証器などの 1970 年代の古典的な作品にまで遡ります。このスタイルの検証器は、最近、自動アクティブ検証と呼ばれています。これは、プログラマと型チェッカーのやり取りに類似した、アサート チェック ループを介して検証器とやり取りする方法を思い起こさせる用語です。
  • 最初の分離ロジック検証ツールである Smallfoot は、この中間のカテゴリに属していました。ユーザーは、事前/事後仕様、ループ不変条件、およびロックのリソース不変条件を入力する必要がありました。また、シンボリック実行の方法と、フレーム公理を自動的に推論する方法を導入しました。Smallfoot には、並行分離ロジックが含まれていました。
  • SmallfootRG は、並行プログラムの分離ロジックと従来の依存/保証方式の結合を検証するツールです。
  • Heap Hop は、 Singularity (オペレーティング システム)の考え方に従って、メッセージ パッシングの分離ロジックを実装します。
  • VeriFast は、中間カテゴリの高度な最新ツールです。オブジェクト指向パターンから高度な並行アルゴリズム、システム プログラムまで、さまざまな証明を実現しています。
  • Viperは、許可ベース推論のための最先端の自動検証インフラストラクチャです。主にプログラミング言語と2つの検証バックエンドで構成されており、1つはシンボリック実行ベース、もう1つは検証条件生成（VCG）ベースです。^[26] Viperインフラストラクチャに基づいて、さまざまなプログラミング言語用のフロントエンドがいくつか登場しています。Go用のGobra、Python用のNagini、Rust用のPrusti、C、Java、OpenCL、OpenMP用のVerCorsです。これらのフロントエンドは、フロントエンドのプログラミング言語をViperに変換し、Viper検証バックエンドを使用して入力プログラムの正しさを証明します。
  • Mezzo プログラミング言語と非同期液体分離型には、プログラミング言語の型システムにおける CSL に関連するアイデアが含まれています。型システムに分離を含めるというアイデアについては、エイリアス型と干渉の構文制御で以前に例が示されています。

インタラクティブな検証者と中間の検証者との区別は明確ではありません。たとえば、Bedrock は、ほぼ自動の検証と呼ばれる高度な自動化を目指していますが、Verifast では、インタラクティブな検証者で使用される戦術 (小さなプログラム) に似た注釈が必要になることがあります。

場所とデータのソートでパラメータ化された、量指定子のない多重ソートされた分離ロジックのフラグメントの充足可能性問題は、PSPACE完全であることが示されます。^[27] DPLL(T)ベースのSMTソルバーでこのフラグメントを解くアルゴリズムは、 cvc5に統合されています。^{[28]この結果を拡張すると、解釈されないメモリ場所を持つ分離ロジックの}Bernays-Schönfinkelクラスの類似体の充足可能性もPSPACE完全であることが示されますが、解釈されるメモリ場所（整数など）や量指定子のさらなる交替では問題は決定不能です。^[29]