2017 Fiscal Year Research-status Report
メモリ一貫性モデルを考慮したプログラム検証の統一理論の構築とその検査器の実装
| Project/Area Number |
16K21335
|
|---|
| Research Institution | Chiba Institute of Technology |
|---|
Principal Investigator |
安部 達也 千葉工業大学, 人工知能・ソフトウェア技術研究センター, 上席研究員 (50547388)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | メモリ一貫性モデル / プログラム検証 / モデル検査 / ガベージコレクション |
|---|
| Outline of Annual Research Achievements |
メモリ一貫性モデルを考慮したモデル検査における状態爆発問題に対し、リオーダリングされる命令の制御という解決手法の提案を行い、それを開発しているモデル検査器 McSPIN に実装し、評価を行った。それらに関して執筆した論文は、国際会議 9th Working Conference on Verified Software: Theories, Tools, and Experiments に採択された。Garbage Collection の代表的な教科書である Jones et al.「The Garbage Collection Handbook」に載っている並行 GC を McSPIN で検査し、知られていないバグ 2 つを発見し、それに関する論文が国際会議 The 32nd OOPSLA に採択された。平成28年度に構築したプログラム論理においてもプログラムの表現として利用されている directed acyclic graph を検査するモデル検査器 VeriDAG を開発し、これに関する論文が The 13th Haifa Verification Conference に採択された。メモリ一貫性モデルを考慮したモデル検査器 SPIN 用のライブラリに関する、共同研究をしている松元稿如氏・鵜川始陽博士との共著論文が Journal of Information Processing に採択された。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究計画に記載したもののうち、既存の GC の検査を行い、知られていなかったバグの発見を完了しているため、おおむね順調に進展していると言える。
|
| Strategy for Future Research Activity |
研究計画に記載したものの残りである、さらにより大きな並列分散アルゴリズムへの適用のための状態数の削減、特に、考慮・検査すべきミューテータ数の削減による方法に関する論文の執筆を行う。
|
Research Products
(5 results)
