Scalable Deductive Verification of Data-Level Parallel Programs

技術的概要：データレベル並列プログラムのスケーラブルな演繹的検証

問題定義
データレベル並列プログラム（CUDA、OpenCL、または SYCL を使用する GPU カーネルなど）の演繹的検証は、重大なスケーラビリティの課題に直面しています。これらのプログラムは通常、大規模な配列や行列を操作するため、ネストされた量化子に富む形式的な契約（コントラクト）が生じます。特定された主なボトルネックは以下の通りです：

1. 量化子のインスタンス化: SMT ソルバーは、配列インデックス内に算術式を含むネストされた量化子（例：A[i * stride + offset]）に苦慮します。標準的な E-マッチング（トリガーに基づくインスタンス化）は、トリガーが単純なパターンであることを要求します。トリガー内の算術演算は、しばしばソルバーが適切なインスタンス化を見つけることを妨げ、検証の失敗や過剰な時間消費をもたらします。
2. エイリアス推論: 複数の配列や行列を利用するプログラムは、これらの構造が重複するかどうか（エイリアシング）について推論する必要があります。分離論において、潜在的に重複する配列に対する非重複権限を検証すると、証明義務の数が二次関数的に増加し、検証時間が劇的に増大します。

手法
著者らは、権限ベースの分離論と Viper 中間検証言語に基づいた演繹的プログラム検証器VerCors内で実装された、3 つの統合された手法を提案します。

1. トリガー生成のための量化子書き換え:
   本論文は、ネストされたまたは複雑な量化子を含む式を、単一の量化子と算術を含まないトリガーを持つ等価な形式に書き換える手続きを導入します。

   • メカニズム: この手法は、$f(x_1, \dots, x_k) = \sum a_i x_i + b$ の形式の線形算術インデックスパターンを識別します。線形インデックスから元の量化変数への全単射写像（逆関数 $f^{-1}$）を定義します。
   • 変換: 元の量化子 $\forall x_1, \dots, x_k; \dots; R(A[f(x_1, \dots, x_k)], \dots)$ は、$\forall x; Y(x); R(A[x], f^{-1}(x))$ に書き換えられます。これにより、$A[x]$ が SMT ソルバーに対する有効なトリガーとして機能することが可能になります。
   • 正当性: この手続きの正当性は、境界と係数に関する特定の条件下で書き換えられた量化子が元の量化子と論理的に等価であることを保証するために、Lean 定理証明器（約 2500 行のコード）を用いて形式的に証明されています。

2. 一意かつ不変な型修飾子:
   エイリアシングと権限のオーバーヘッドに対処するため、著者らは 2 つの型修飾子を導入します。

   • 不変（Immutable）: ポインタが指すデータが実行中に変更されないことを示します。これにより、検証器はデータを可変ヒープブロックではなく数学的な列としてモデル化でき、権限の追跡の必要性を排除し、ヒープスナップショットの複雑さを低減します。
   • 一意（Unique）: ポインタに一意の番号を割り当てます。異なる一意番号を持つポインタは、エイリアスしないことが保証されます。これにより、検証器は非重複配列を Viper バックエンドの異なるフィールドにエンコードでき、エイリアシングをチェックするために必要なスナップショット比較の二次関数的な爆発を防ぎます。
   • 統合: これらの修飾子は既存のライブラリと互換性があり、柔軟な型チェックを可能にします。これにより、非一意の配列を期待する関数も、一意性の制約が守られれば一意の配列を受け入れることができます。

3. カーネル本体の抽出:
   著者らは、モノリシックな GPU カーネルを検証することは、SMT ソルバーに提示される情報の膨大さにより、しばしば遅くなることを観察しました。彼らは、カーネル本体を独自の契約を持つ別々の関数へ移動させる自動化された抽出戦略を提案します。このモジュール化により、ソルバーのコンテキストサイズが削減され、パフォーマンスが向上します。

主要な貢献

• 形式的書き換え手続き: 算術インデックスを持つネストされた量化子を、E-マッチングに適した単一量化子形式に平坦化する、数学的に証明された手法。これは VerCors に実装されています。
• 型ベースのエイリアス削減: メモリ配置と可変性を検証器に明示的に指示する unique および immutable 修飾子の導入。これにより、エイリアシングチェックの探索空間が大幅に削減されます。
• 包括的な評価: 大規模な実験的評価。対象は以下の通りです。
  • CLBlast ライブラリ: 基本線形代数サブルーチン（BLAS）を実装する OpenCL カーネルのスイート。
  • 電波望遠鏡パイプライン: Padre アルゴリズムおよび Halide DSL から生成された他の最適化された並列 CPU プログラムを含むケーススタディ。
• アーティファクトの入手可能性: すべての実験データ、Lean による証明、および使用された特定の VerCors バージョンは、付随するアーティファクトで提供されています。

結果
実験は、スケーラビリティと成功率の大幅な改善を実証しています。

• CLBlast カーネル: 組み合わせた手法（書き換え、一意/不変型、抽出）を適用した結果、平均検証時間が9 倍短縮されました。特定の外れ値（例：xger カーネル）では、検証が150 倍高速化されました。重要なのは、手法の組み合わせにより、以前は検証不可能であったり、非常に脆弱（多くの実行で失敗する）であったカーネル（xger や xher2 など）の検証が可能になったことです。
• 電波望遠鏡パイプライン: これらの手法により、以前の研究では得られなかった perform_iteration アルゴリズム（Padre）の検証が可能になりました。成功したケースの検証時間は、特定のアルゴリズムと構成に応じて 1.2 倍から 3.4 倍まで短縮されました。
• 書き換えへの依存: 著者らは、量化子書き換え手続きがなければ、報告された実験のいずれも全く検証できなかったと指摘しており、その基礎的な役割を強調しています。

重要性
本論文は、これらの手法がデータ並列プログラムの演繹的検証における根本的なボトルネックに対処すると主張しています。複雑な配列アクセスに対する適切なトリガーの生成を自動化し、型修飾子によるエイリアス推論のオーバーヘッドを削減することで、著者らは以前は非現実的であった複雑な実世界の GPU および並列 CPU カーネルの検証を可能にします。この研究は、理論的な分離論と、高性能計算コードの実用的かつスケーラブルな検証との間のギャップを埋め、特に電波望遠鏡データ処理に使用される Padre アルゴリズムにおける成功を実証しています。著者らは、手動での書き換えも可能ではあるものの、GPU カーネルの構造化された自動化された検証には、これらのパターンの自動検出と適用が不可欠であると強調しています。