2016 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 |
メモリ一貫性モデルを考慮することで行える、状態の統合による状態爆発の回避に関する論文を執筆・投稿し、国際会議 The 2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications に採択された。また、Xu 博士（澳門大学）の提案した（メモリ一貫性モデルを考慮していない）並行プログラム論理を拡張することでメモリ一貫性モデルを考慮した新しい並行プログラム論理を構築した。このプログラム論理は（申請者の知る限り）既存の全ての並行プログラム論理が扱うことができない (non-)multiple-copy-atomicity についてパラメタライズされており、既存のプログラム論理で扱うことが容易でないことが知られている並行プログラム Independent Reads Independent Writes の検証を行うことに成功した。このプログラム論理に関する論文を投稿し、Journal of Information Processing と国際会議 The 14th Asian Symposium on Programming Languages and Systems にそれぞれ採択された。また、共同研究を行っている鵜川博士・松元氏（高知工科大学）とメモリ一貫性モデルを考慮する SPIN ライブラリの開発に関する論文を投稿し、FOSE'16 に採択された。また、国産並列プログラミング言語 XcalableMP の仕様について、申請者が執筆した Appendix E (pages 147--152) が 2017 年 1 月 12 日に行われた XcalableMP の仕様策定の規格部会で承認され、Version 1.3 から採用されることに決定した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究計画に記載したもののうち、non-multiple-copy-atomicity を扱うことができるプログラム論理の構築・論文投稿・採択と、本研究課題において提案するものの XcalableMP 仕様書への反映を完了しているため、おおむね順調に進展していると言える。
|
| Strategy for Future Research Activity |
構築したプログラム論理で使用しているデータ構造を基にモデル検査器をブラッシュアップし、さらなる実用化を目指す。
|
| Causes of Carryover |
当初、予定していた旅費の本科研費から支出を学校費による支出に変更し、また、計算機の学校費による購入を本科研費に変更したため、次年度使用額にわずかな差が増分として現れた。
|
| Expenditure Plan for Carryover Budget |
本年度は研究成果の発表を控えており旅費を多く使用するため、それに充てる予定である。
|
