A unified theory of program verision with memory consistency models and its implementations
| Project/Area Number |
16K21335
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Software
High performance computing
|
|---|
| Research Institution | Chiba Institute of Technology |
|---|
Principal Investigator |
ABE Tatsuya 千葉工業大学, 人工知能・ソフトウェア技術研究センター, 上席研究員 (50547388)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Project Status |
Completed (Fiscal Year 2018)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2018: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2017: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2016: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
|
|---|
| Keywords | プログラム検証 / メモリ一貫性モデル / モデル検査 / ガベージコレクション / プログラム論理 / Non-multi-copy atomicity / IRIW / 定理証明 / 数理論理学 |
|---|
| Outline of Final Research Achievements |
I did joint researches with Tomoharu Ugawa, Toshiyuki Maeda, and Kosuke Matsumoto. We proposed an optimization of model checking with memory consistency models (MCMs) that reduces the number of states by integrating multiple states and controlling reordering of instructions according to input MCMs. We constructed a program logic with MCMs that Independent Reads Independent Writes with non-multi-copy atomicity (non-MCA). We developed a SPIN library that supports MCMs. We designed an MCM for a directive-based parallel programing language XcalableMP. We demonstrated model checking of concurrent copy garbage collecton algorithms. We proposed local data race freedom (LDRF), a property of a program. We also proposed an optimization of model checking with MCMs that reduces the number of states of programs that enjoy LDRF with non-MCA MCMs.
We wrote some papers about these results. All of them were published. We also released tools and programs that we developed in this study.
|
| Academic Significance and Societal Importance of the Research Achievements |
プログラムを世に出す前にその安全性を検証する手法を研究・開発しました。本研究で開発した手法により、既存手法に対して検査時間の短縮と扱えるプログラムの範囲の拡張が実現されました。また、並列計算環境が普及した現代において広く使われているアルゴリズムである並行コピーガベージコレクションの検査を実演することで私たちの手法の有効性を示しました。研究したことは論文というかたちで出版されていることによりその内容を公知のものとし、また、開発したツールとプログラムをすべて公開したことでこれらを広く使用可能にしました。
|
Report
(4 results)
Research Products
(15 results)
