2016 Fiscal Year Annual Research Report
A Program Verification Theory of Memory Consistency Models on PGAS languages and its Implementation
| Project/Area Number |
25871113
|
|---|
| Research Institution | Chiba Institute of Technology |
|---|
Principal Investigator |
安部 達也 千葉工業大学, 人工知能・ソフトウェア技術研究センター, 上席研究員 (50547388)
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Keywords | メモリ一貫性モデル / プログラム検証 / モデル検査 / プログラム論理 |
|---|
| Outline of Annual Research Achievements |
本研究課題で提案したメモリ一貫性モデルを考慮したモデル検査理論に関して執筆した論文が International Journal on Software Tools for Technology Transfer に採択された。また、メモリ一貫性モデルを考慮することで行うことができるようになる最適化の一つ「状態の統合による状態爆発の回避」に関する論文を執筆・投稿し、国際会議 The 2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications に採択された。また、前年度に執筆を完了していたメモリ一貫性モデルを考慮したプログラム検証においてその正しさを保証するためのプログラム論理に関する論文を投稿し Journal of Information Processing に採択された。また、これも前年度から引き続いて行っていた、国産並列プログラミング言語 XcalableMP の仕様書へ本研究課題で行った形式化されたメモリ一貫性モデルによる仕様記述の採用を目指す活動であるが、申請者が執筆した Appendix E が 2017 年 1 月 12 日に行われた XcalableMP の仕様策定の規格部会で承認され、Version 1.3 から採用される予定である。
|
