ISP 形式検証ツール

ISP ("In-situ Partial Order") は、ユタ大学のコンピューティング学部で開発されたMPIプログラムの形式検証ツールです。SPINなどのモデル チェッカーと同様に、ISP はシステムの完全な状態空間を検証して一連の安全性プロパティを確認します。ただし、モデル チェッカーとは異なり、ISP はコード レベルの検証を実行します。つまり、ツールは、検証モデルを構築せずに実際のプログラム コードを再生することで、並行プログラムの関連するすべてのインターリーブを検証します。このアイデアは、Godefroid の VeriSoft ツール^[1]をはじめ、多くのツールで開拓されました。このジャンルの他の最近のツールには、Java Pathfinder、Microsoft の CHESS ツール、MODIST などがあります。関連するインターリーブは、 POE ^{[2]と呼ばれるカスタマイズされた}動的部分順序削減アルゴリズム を使用して計算されます。^[3]

ISP は、最大 14,000 行の MPI/C コードのデッドロックとアサーション違反の検証に成功しています。現在、60 を超えるMPI 2.1関数をサポートしており、 MPICH2、OpenMPI、Microsoft MPIライブラリでテストされています。

ISP は、 LinuxおよびMac OS X用、Windowsで実行するためのVisual Studioプラグイン、およびEclipseプラグインとしてダウンロードできます。

Anh Vo、Sarvani Vakkalanka、Michael DeLisi、Ganesh Gopalakrishnan、Robert M. Kirby、Rajeev Thakur、実践的な MPI プログラムの正式検証、 PPoPP 2009

Sarvani Vakkalanka、Michael DeLisi、Ganesh Gopalakrishnan、および Robert M. Kirby、「MPI、並列、および分散システム用の動的検証ツールを構築するためのスケジュールの考慮事項- テストとデバッグ (PADTAD-VI)」、 Wayback Machineに 2008 年 9 月 30 日にアーカイブ、シアトル、ワシントン州、2008 年 7 月。

Sarvani Vakkalanka、Michael DeLisi、Ganesh Gopalakrishnan、Robert M. Kirby、Rajeev Thakur、William Gropp、「MPI プログラム用の効率的な動的形式検証方法の実装」、並列仮想マシンおよびメッセージ パッシング インターフェイスの最近の進歩 (EuroPVM/MPI 2008)、ダブリン、アイルランド、2008 年、LNCS 5205、pp. 248–256。

Sarvani Vakkalanka、Subodh Sharma、Ganesh Gopalakrishnan、および Robert M. Kirby、「ISP: MPI プログラムのモデル検査ツール、並列プログラミングの原則と実践 (PPoPP 2008)」、Wayback Machineに 2009-02-08 にアーカイブ、ソルトレイクシティ、2008 年 2 月、285 ～ 286 ページ。

Salman Pervez、Robert Palmer、Ganesh Gopalakrishnan、Robert M. Kirby、Rajeev Thakur、William Gropp、「MPI プログラムの正確性を検証するための実用的なモデル検査方法」、並列仮想マシンとメッセージ パッシング インターフェイスの最近の進歩 (PDF) 2008 年 4 月 18 日にWayback Machineにアーカイブ(EuroPVM/MPI)、パリ、344—353、LNCS 4757、フランス、2007 年 9 月 30 日 - 10 月 3 日

並列数値プログラムを検証するためのシンボリック実行とモデル検査の組み合わせ、umass.edu PDF SF Siegel、A Mironova、GS Avrunin、LA Clarke - ACM Transactions on Software Engineering and Methodology - portal.acm.org

非ブロッキング操作を使用した MPI プログラムの停止特性の検証

- psu.edu PDF 

SF シーゲル、GS アヴルニン - コンピュータサイエンスの講義ノート、2007 - シュプリンガー

MPIWiz: MPI アプリケーションのサブグループ再現可能な再生 R Xue、X Liu、M Wu、Z Guo、W Chen、W Zheng、Z Zhang、Geoffrey M. Voelker 清華大学、Microsoft Research Asia、南カリフォルニア大学サンディエゴ校 - cs.ucsd.edu

フローグラフベースの並列アプリケーションの動的テスト

- epfl.ch [1] 2016年6月10日にWayback Machineにアーカイブ 

B Schaeli、RD Hersch - 並列および分散プログラミングに関する第 6 回ワークショップの議事録、2008 - portal.acm.org

MPI アプリケーションのビジュアル デバッグ

- epfl.ch PDF 

B Schaeli、A Al-Shabibi、RD Hersch - 第 15 回ヨーロッパ PVM/MPI ユーザー グループ会議議事録 …、2008 - Springer

• ISPリリース