並行プログラムのPartialStoreOrderingでの実行をモデル検査するためのReleaseメモリバリア

情報処理学会

書誌事項

タイトル別名
  • Promela Model of Acquire Fence for Model Checking of Concurrent Programs against Partial Store Ordering

抄録

我々は，並行プログラムの弱いメモリ一貫性モデルでの振舞いをモデル検査するためのモデル集（以下，モデル検査ライブラリ）であるMMLibを開発している．SPINモデル検査器で検査するために，Promelaで記述されたモデルに対して，共有変数のリードとライトを，MMLibが提供するマクロの呼出しに置き換えるだけで，TSOやPSOに従った振舞いを検査できるようになる．これまでMMLibにはacquire-releaseフェンスが存在しなかったため，それを用いたプログラムを検査できなかった．本研究では，このうちPSOのreleaseフェンスのモデルを実装した．releaseフェンスの使用に誤りがあることが分かっている並行GCをMMLibを使って検査し，誤りが検出されることを確認した．

収録刊行物

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ