ヒープ中の同期ロックの整合性に関するモデル検査

スポンサーリンク

概要

論文の詳細を見る
カーネル・モジュール等に対して,排他ロック等の呼び出し整合性の検査を行うため,抽象実行に基づくモデル検査器が提案されている.しかし,カーネルではロック等はヒープ中に置かれることが多いのでヒープを扱うことができる検査器が必要である.一方,ヒープに関する性質を記述・検査するのに用いられる Separation Logic のサブセットに対して決定手続きが提案されている.そこで我々は開発中のモデル検査器のソルバにヒープに関する決定手続きを組み込み,ヒープ中にあるロックの整合性検査を試みた.ヒープの決定手続きは,ヒープの制約を等式の制約として生成するので,ソルバに対してフロントエンドとして組込み込むことができる.また,述語セットのリファインメントを行わずに実用的な速度で検査を行うため,関数の入口で行う述語セットの選択を導入している.また,ヒープに関するモデル検査行う場合の一般的な課題について述べる.
2010-06-16

著者

関連論文

もっと見る

スポンサーリンク