GPGPUのための並行分離論理のCoqによる健全性証明

GPGPU 向けの並行分離論理 (GPUCSL) を設計し,定理証明支援器 Coq を用いた健全性の証明を与える. Blom らは GPGPU カーネルの自動検証のために CSL を設計したが,その推論規則は frame 規則がないなど,標準的な CSL と異なる.本研究で設計した GPUCSL は,標準的な CSL の素直な拡張であるため, CSL に関する他の研究成果を取り込みやすくなっている.健全性の証明には, fork-join モデルの並行プログラム向け CSL の健全性についての Vafeiadis の証明法を応用した.この証明を通して, (1) スレッド ID 独立性をバリア相違 (barrier divergence) がないことの十分条件とした Blom らの議論の不備と (2) Blom らの証明の単純な拡張では frame 規則のある CSL の健全性を示せないことを明らかにした.GPUCSL は CUDA 言語のサブセットをモデル化したものだが,バリア同期を用いた単純なカーネルが仕様を満たすことを検証するのに十分な表現力を持つ.このことを予備実験を通して示した.

Members

健全性の証明

Coqスクリプト(for 8.4pl4)

論文