|
メモリ一貫性モデルを考慮したモデル検査を高速に実行可能にするプログラム中の全スレッドに対して定義される性質 data race freedom をスレッドのサブセットに対する概念に拡張することで local data race freedom という性質を提唱した。この性質は、メモリ一貫性モデルを考慮したプログラム検証において特徴的なプログラムである Independent Reads Independent Writes (IRIW) や、全てのミューテータが data race free なプログラムであることを仮定した場合、ミューテータたちとコレクタからなる並行コピーガベージコレクションのモデルが満たす性質の一つである。また、local data race freedom を利用したモデル検査の状態数削減手法、memory sharing optimization を提唱した。この最適化を、IRIW と昨年度に開発を開始したモデル検査器 VeriDAG に実装し、本研究課題で継続的に開発している McSPIN の評価のための実験に使用した並行コピーガベージコレクションのモデルを使用して実験をおこない、その有効性を確認した。これらすべてに関する内容を記載した論文を執筆し、The 23rd International SPIN Symposium に採択された。モデル検査器 VeriDAG と実験に使用したモデルすべてを公開した。本研究課題で網羅的に調査した国内外の研究内容と自身の研究成果について、産業技術総合研究所関西センターでメモリ一貫性モデルを考慮したプログラム検証に関するチュートリアル的な依頼講演をおこなった。
|
