| 研究課題/領域番号 |
16K21335
|
|---|
| 研究機関 | 千葉工業大学 |
|---|
研究代表者 |
安部 達也 千葉工業大学, 人工知能・ソフトウェア技術研究センター, 上席研究員 (50547388)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2019-03-31
|
| キーワード | メモリ一貫性モデル / プログラム検証 / 定理証明 / モデル検査 / プログラム論理 / 数理論理学 |
|---|
| 研究実績の概要 |
メモリ一貫性モデルを考慮することで行える、状態の統合による状態爆発の回避に関する論文を執筆・投稿し、国際会議 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 から採用されることに決定した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究計画に記載したもののうち、non-multiple-copy-atomicity を扱うことができるプログラム論理の構築・論文投稿・採択と、本研究課題において提案するものの XcalableMP 仕様書への反映を完了しているため、おおむね順調に進展していると言える。
|
| 今後の研究の推進方策 |
構築したプログラム論理で使用しているデータ構造を基にモデル検査器をブラッシュアップし、さらなる実用化を目指す。
|
| 次年度使用額が生じた理由 |
当初、予定していた旅費の本科研費から支出を学校費による支出に変更し、また、計算機の学校費による購入を本科研費に変更したため、次年度使用額にわずかな差が増分として現れた。
|
| 次年度使用額の使用計画 |
本年度は研究成果の発表を控えており旅費を多く使用するため、それに充てる予定である。
|
