2013 Fiscal Year Research-status Report
PGAS言語のメモリ一貫性に関するプログラム検証理論とその実装
| Project/Area Number |
25871113
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Research Institution | Institute of Physical and Chemical Research |
|---|
Principal Investigator |
安部 達也 独立行政法人理化学研究所, 計算科学研究機構, 研究員 (50547388)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | メモリ一貫性モデル / プログラム検証 / 形式的体系 / モデル検査 |
|---|
| Research Abstract |
複数の計算ノード上に存在する複数のメモリに対する統一的なアクセス方法を提供する、いわゆる 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 に載っているサンプルプログラムに対し検査を行い、検査器の正しさ・有用性・汎用性を確認した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
既存のメモリ一貫性モデルの調査が順調に進んでおり、機能的に大きな区切りとなるところでそこまででわかったところまででそれらメモリ一貫性モデルの形式化とその形式化されたメモリ一貫性モデルを入力とするモデル検査器の実装が行えている。また、これらの結果をまとめた論文が国際会議・ワークショップに受理されている。
|
| Strategy for Future Research Activity |
研究計画通りに進めることができているので、今後も研究計画通りに進める。特に（研究計画書にもある通り）理化学研究所・筑波大学が中心になって開発している PGAS 言語である XcalableMP の対応に注力する。
|
| Expenditure Plans for the Next FY Research Funding |
研究が計画より早まり次年度に執筆・投稿予定であった論文を執筆・投稿できたため、次年度使用額を繰り越して論文を投稿したが、不受理となったためその国際会議へ出席するための旅費・参加費が浮いたため。
2014年5月に開催される国際会議・ワークショップに論文が受理されたため、その旅費・参加費に充てる。
|
