Recursive Mutexes in Separation Logic

技術要約：分離論理における再帰的ミューテックス

問題提起
メカニズム化された並行分離論理は、VST、BRiCk、RustBeltといったツールを用いてC++やRustのような言語の現実世界のプログラムを検証できる段階まで進歩していますが、標準的な並行ライブラリの形式検証には依然としてギャップが存在します。具体的には、再帰的ミューテックス（C++やJavaで一般的）には、確立された分離論理の仕様が欠けています。標準的なミューテックスとは異なり、再帰的ミューテックスは、単一のスレッドが同じロックを複数回取得することを許可します。この機能により、ロックを保持している関数が、同じロックを取得しようとする別の関数を安全に呼び出すことができる（例：図1におけるtransferからupdate_aの呼び出し）といった、慣用的なコードパターンが可能になります。標準的なミューテックスの仕様は、このような透明性とカプセル化をサポートできず、開発者に非ロッキングの代替関数を作成させたり、複雑なケース分析を行わせたりすることを余儀なくさせることがよくあります。

手法
著者らは、呼び出しスレッドの現在の所有状態に関わらず、ロックの取得と解放を一様に扱う、再帰的ミューテックスのための新しい分離論理仕様を提案しています。この手法は、主に2つのコンポーネントを導入しています。

1. 分数ハンドルとスレッド固有の述語:

   • 不変条件 $P$ を持つ再帰的ミューテックス $\gamma$ は、分数ハンドル $\ell \mapsto_q \text{rmutex}(\gamma, P)$ と関連付けられます。
   • 決定的なのは、ミューテックスと相互作用するすべてのスレッド $t$ が、独自の述語 $\text{holds}(\gamma, t, n, P)$ を保持することです。ここで、$n$ はスレッド $t$ がミューテックスを取得した回数を表します。
   • 相互排除は、2つのスレッドがミューテックスを保持している場合、少なくとも一方がゼロのカウントを持つ（$n_1 = 0 \lor n_2 = 0$）というルールによって強制されます。
   • スレッドがリソースを「二重計上」することを防ぐため、論理は、あるスレッドが2つの $\text{holds}$ 述語を同時に保持できないことを強制します。したがって、$\text{holds}(\gamma, t, n_1, P) * \text{holds}(\gamma, t, n_2, P) \vdash \text{False}$ となります。

2. 状態遷移と借用:

   • ロック/アンロック: ロックの取得はスレッドのカウント $n$ をインクリメントし（$n \to n+1$）、解放はデクリメントします（$n \to n-1$）。
   • 借用ルール: スレッドは、そのカウント $n > 0$ である場合に限り、保護された不変条件 $P$ にアクセスできます。このルールは、$\text{holds}(\gamma, t, n, P)$ （$n>0$）を、実際の型リソース $P$ と、カウントを追跡するが $P$ へのアクセス権を与えないリテーナー $\text{held}(\gamma, t, n)$ と交換することを許可します。
   • 量化された引数の処理: ロックの不変条件に存在量化された変数（例：$\exists v. x \mapsto v$）が含まれる場合の問題に対処するため、著者らは $\text{holds}$ 述語に渡される引数のタプル $a$ を導入しています。これにより、スレッドが $P$ を借りる際に、不変条件の状態に戻る際に情報を再量化して失うのではなく、リソースに関する特定の知識（例：変数の特定の値）を保持できることが保証されます。

主な貢献

• 統一された仕様: 本論文は、クライアントが「初回」の取得と「再帰的」な取得を区別することなく、自身のカウント $n$ がゼロより大きいかどうかをチェックするだけで、ミューテックスを保持しているかどうかを判断できる仕様を提供します。
• 慣用的な推論: これらの仕様は、関数が同じロックを取得する別の関数を呼び出すコードパターンにおいて、特別な「ノーロック」版の関数を必要とせずに、標準的なC++の使用法を模倣した証明を可能にします。
• C++並行性の形式検証: 本研究は、BRiCkフレームワークを用いてC++の並行ライブラリ（具体的には std::recursive_mutex）を検証することによる、これらの仕様の適用を実証しています。

結果
著者らは、transfer 関数が同じ再帰的ミューテックスを保持しながら update_a と update_b を呼び出す図1の例を検証するために、これらの仕様を適用することに成功しました。この検証により、以下が確認されました。

• transfer 関数は、両者が同じミューテックスを取得しているにもかかわらず、update_a を安全に再利用できること。
• 操作全体を通じて不変条件（balance_a と balance_b の合計）が保持されること。
• 論理が、スレッドが最初にロックを保持していたか否かにかかわらず不変条件の状態を正しく扱い、コールスタックを通じて特定の変数（$a$ や $b$ など）の特定の値が保持されること。

意義
本論文は、これらの仕様が、通常のミューテックスを使用する場合よりも再帰的ミューテックスの推論を「より透明かつ高度にカプセル化」できると主張しています。ロックの取得（$n$ のインクリメント）と不変条件の借用（$n>0$ の時の $P$ へのアクセス）を分離することで、このアプローチは主流の言語に見られる一般的なソフトウェアエンジニアリングパターンをサポートします。この研究は、C++標準ライブラリ全体の検証というより広い目標に向けた一歩として提示されており、現実世界の並行プログラミングに実用的な推論原理を明らかにすることを目指しています。著者らは、現在の仕様が std::atomic や std::vector といった他の標準ライブラリのコンポーネントもカバーしていると述べています。