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

摘要

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