2012 Fiscal Year Research-status Report
ゲーム意味論による共有メモリ型並列プログラムの定式化と検証
| Project/Area Number |
24500014
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
西村 進 京都大学, 理学(系)研究科(研究院), 准教授 (10283681)
|
|---|
| Project Period (FY) |
2012-04-01 – 2016-03-31
|
| Keywords | 並列プログラム / ゲーム意味論 / プログラム検証 |
|---|
| Research Abstract |
当該年度では、本研究の理論的な基礎、すなわちゲーム意味論を用いた共有メモリ型並列プログラムの意味の定式化についての研究を行い、次のような成果を得た。
(1) ゲーム意味論による定式化に際しては、並列プログラムが非決定的な実行パスのどれを辿っても正しく動くことを保証できるような定式化を行う必要があるが、これを、HarmerとMcCuskerによる非決定的Algol言語のためのゲーム意味論を、wait-notifyゲームという並列計算のモデル化に適した形に拡張することによって達成した。この成果については、情報処理学会プログラミング研究会論文誌に採録・出版された。(渡辺敬介氏との共同研究)
(2) しかしながら、上記共同研究で提案したwait-notifyゲームは、関数などの既存の計算構造との関係が明らかでなかったため、非常に制限された形の並列プログラムしか扱うことができなかった。そこで、wait-notifyゲームに内在する計算構造を既存の計算構造の中にどのような形で統合することができるか検討した結果、wait-notifyゲームの構造がモナドの構造を持つことを明らかとし、これによって（ごくゆるやかな制限のもとで）並列プログラムをKleisli圏における射として定式化できることを示すことができた。また、この定式化に基づき、ゲーム意味論の重要な定理であるfull abstractionが並列プログラムについても成立することを示すことに成功した。また、この結果によって、並列実行における競合を避けるためのある種のアトミックなメモリ操作命令が本質的に必要である（このようなメモリ操作がなければ実現できない並列プログラムが存在する）ことが明らかとなった。この成果は、現在国際学会に投稿中である。
|
| 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 |
研究の理論的基礎となる部分がおおよそ完成したので、次の研究のステージ、すなわち与えられた並列プログラムが意図した通りの動作をするかどうかを、ゲーム意味論の枠組みの中で判定する系統的方法の研究を開始する。
これまでに成し遂げた定式化によって、並列プログラムの等価性の議論が対応するゲームの等価性のそれに還元できることが示されるが、これをそのまま並列プログラムの等価性の検証に適用することはできない。なぜなら、ゲームの等価性の判定が一般には決定不可能であるからである。この問題に対処するため、次年度は次のような研究を行う。
(1) 定式化したゲームの構造のさらなる解析を行い、等価性の判定を行うにはどのような条件が必要かを明らかにする。
(2) 上記の条件に基づいて、並列プログラミング言語のサブセットに関して等価性の判定を試みる。逐次プログラミング言語についてGhicaとMcCuskerが行ったように、適切な言語サブセットを設定することによって、正規言語の等価性問題へと帰着することを計画している。
(3) 上記言語サブセットについて、プログラムの等価性判定を正規言語の等価性に自動的に還元して判定するツールのプロトタイプを作成し、その実効性について検証を試みる。
|
| Expenditure Plans for the Next FY Research Funding |
海外で開催される国際会議や、国内での研究集会などに参加・発表するため旅費を使用する。研究資料として関連する専門書等も購入する。
また、プログラムの等価性判定をおこなうツールの作成に当たっては、現在所属機関で使用しているPC等では性能が不足する場合は、性能が十分なものを新たに購入する。
|
