| 研究課題/領域番号 |
25871113
|
|---|
| 研究種目 |
若手研究(B)
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
高性能計算
ソフトウェア
|
|---|
| 研究機関 | 千葉工業大学 (2015-2016)
独立行政法人理化学研究所 (2013-2014) |
|---|
研究代表者 |
安部 達也 千葉工業大学, 人工知能・ソフトウェア技術研究センター, 上席研究員 (50547388)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2017-03-31
|
| 研究課題ステータス |
完了 (2016年度)
|
| 配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2015年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
2014年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2013年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
|
|---|
| キーワード | メモリ一貫性モデル / プログラム検証 / モデル検査 / プログラム論理 / PGAS言語 / 形式的体系 |
|---|
| 研究成果の概要 |
PGAS言語で採用されているメモリ一貫性モデルを調査し、それらを統一的に扱うプログラム検証理論の一つを提案し、ユーザ定義可能なメモリ一貫性モデルまでも考慮することができるモデル検査を行うための実装McSPINを開発・公開した。いくつかの最適化を提案し、それに関する論文を雑誌・国際会議に投稿し、採択された。プログラム論理の構築にも成功し、これを記載した論文を雑誌に投稿し、採択された。また、検証理論で使用する記述言語で、実際のPGAS言語であるところのXcalableMPのメモリ一貫性モデルを記述した。これはXcalableMPの仕様策定の規格部会で採用が承認され1.3版から収録される予定である。
|
