| 研究課題/領域番号 |
25871113
|
|---|
| 研究種目 |
若手研究(B)
|
| 研究機関 | 独立行政法人理化学研究所 |
|---|
研究代表者 |
安部 達也 独立行政法人理化学研究所, 計算科学研究機構, 研究員 (50547388)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | メモリ一貫性モデル / プログラム検証 / 形式的体系 / モデル検査 |
|---|
| 研究概要 |
複数の計算ノード上に存在する複数のメモリに対する統一的なアクセス方法を提供する、いわゆる Partitioned Global Address Space (PGAS) 言語である Unified Parallel C (UPC) と Coarray Fortran のメモリ一貫性モデルの調査を行った。さらに、コンピュータアーキテクチャである Itanium のメモリ一貫性モデルの調査も行った。その上で、少なくともこれら三つのメモリ一貫性モデルを記述可能にする汎用的なモデル（ベースモデル）とそのモデルの上でこれら三つのメモリ一貫性モデルを記述するための形式言語の定義を与えた。この定義の下では、この形式言語で記述されたメモリ一貫性モデルはベースモデル上におけるプログラムの実行トレースのうち、どの実行トレースを許容可能とするかという規則である。これらの定義を与えたことにより曖昧性や多義性を含みがちな自然言語によって記述されるメモリ一貫性モデルを形式的に扱えるようにした。
メモリ一貫性モデルを形式的に扱うことができる利点の一つとして、形式化されたメモリ一貫性モデルを入力にとるモデル検査器の試作を行った。このモデル検査器で UPC Language Specifications V1.2 の Appendix B に載っているサンプルプログラムと Itanium の仕様書（A Formal Specification of Intel Itanium Processor Family Memory Ordering）の Appendix A に載っているサンプルプログラムに対し検査を行い、検査器の正しさ・有用性・汎用性を確認した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
既存のメモリ一貫性モデルの調査が順調に進んでおり、機能的に大きな区切りとなるところでそこまででわかったところまででそれらメモリ一貫性モデルの形式化とその形式化されたメモリ一貫性モデルを入力とするモデル検査器の実装が行えている。また、これらの結果をまとめた論文が国際会議・ワークショップに受理されている。
|
| 今後の研究の推進方策 |
研究計画通りに進めることができているので、今後も研究計画通りに進める。特に（研究計画書にもある通り）理化学研究所・筑波大学が中心になって開発している PGAS 言語である XcalableMP の対応に注力する。
|
| 次年度の研究費の使用計画 |
研究が計画より早まり次年度に執筆・投稿予定であった論文を執筆・投稿できたため、次年度使用額を繰り越して論文を投稿したが、不受理となったためその国際会議へ出席するための旅費・参加費が浮いたため。
2014年5月に開催される国際会議・ワークショップに論文が受理されたため、その旅費・参加費に充てる。
|
