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

• Item type: Trans(1)
• 公開日: 2010-06-16
• タイトル: ヒープ中の同期ロックの整合性に関するモデル検査
• タイトル / 言語: en
• タイトル: Model Checking Consistency of Usage of Synchronization Locks in Heap
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 発表概要
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 東京大学大学院情報理工学系研究科
• 著者所属: 東京大学大学院情報理工学系研究科
• 著者所属: 東京大学大学院情報理工学系研究科
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Technology, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Technology, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Technology, The University of Tokyo
• 著者名: 松田, 元彦; 前田, 俊行; 米澤, 明憲
• 著者名(英): Motohiko, Matsuda; Toshiyuki, Maeda; Akinori, Yonezawa
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: カーネル・モジュール等に対して，排他ロック等の呼び出し整合性の検査を行うため，抽象実行に基づくモデル検査器が提案されている．しかし，カーネルではロック等はヒープ中に置かれることが多いのでヒープを扱うことができる検査器が必要である．一方，ヒープに関する性質を記述・検査するのに用いられる Separation Logic のサブセットに対して決定手続きが提案されている．そこで我々は開発中のモデル検査器のソルバにヒープに関する決定手続きを組み込み，ヒープ中にあるロックの整合性検査を試みた．ヒープの決定手続きは，ヒープの制約を等式の制約として生成するので，ソルバに対してフロントエンドとして組込み込むことができる．また，述語セットのリファインメントを行わずに実用的な速度で検査を行うため，関数の入口で行う述語セットの選択を導入している．また，ヒープに関するモデル検査行う場合の一般的な課題について述べる．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Several model checkers have been proposed for checking consistent usage of kernel routines such as synchronization locks in kernel modules. Such model checkers fail to check locks when they are allocated in heaps. It is because they are typically based on abstract interpretation using integer constraint solvers and cannot handle descriptions of heaps. Recently, some decision procedures are proposed for subsets of Separation Logic, which is popularly used in describing properties of heaps. We present an extension to a model checker, which integrates a decision procedure to an integer constraint solver, where the extension generates heap constraints as a set of integer constraints, and can be integrated to many solvers. And also, the checker implements predicate selection at function call entries, which attains practical speed without using predicate refinement. The paper includes some discussion on general issues of heap related model checking.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 3, 号 3, p. 20-20, 発行日 2010-06-16
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会