2013 Fiscal Year Research-status Report
ゲーム意味論による共有メモリ型並列プログラムの定式化と検証
| Project/Area Number |
24500014
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
西村 進 京都大学, 理学(系)研究科(研究院), 准教授 (10283681)
|
|---|
| Keywords | 並列プログラム / ゲーム意味論 / プログラム検証 |
|---|
| Research Abstract |
共有メモリ型並列プログラムのゲーム意味論による定式化を行うことにより、並列プログラムに内在する計算構造を明らかにした。
並列計算は、並列して動作する複数の逐次計算スレッドが非決定的に選択されるため、本質的に非決定的な性質を持つ。非決定性を扱うゲーム意味論としてはHarmerとMcCuskerによる提案があるが、これを含む従来のゲーム意味論では複数の逐次的計算を混ぜ合わせてゲームを構成することは困難であった。この問題を解決する一つの方法として、渡辺敬介氏との共同研究（２０１２年)においてwait-notifyゲームを提案した。しかしながら、上記共同研究における提案では、関数などの既存の計算要素との関係が明らかでなかったため、ごく限られた形の並列プログラムしか扱うことができなかった。
当該年度の研究においては、ゲーム意味論が構成する圏において、wait-notifyゲームが可換強モナドの構造を誘導することを示し、これによって（一定の緩やかな制限のもとで）関数型言語に書き換え可能変数を加えたAlgol言語の並列拡張したものをゲームのKleisli圏における射として定式化できることを示すことができた。また、この定式化に基づき、ゲーム意味論における標準的な証明手法を改良することによってゲーム意味論の重要な定理であるfull abstractionが成立することを示した。またこの証明は、共有変数のアクセス競合を回避するためのアトミックなメモリ操作命令が本質的に必要であることが示唆するものであり、大変興味深い。この成果は、国際学会Computer Science Logic 2013 (CSL 2013)に採択され、研究発表を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
ゲーム意味論を用いた共有メモリ型並列プログラムの意味の定式化については、当該年度の研究によりおおよそ達成できたかと思われたが、以下に述べるような理由で、これをこのまま並列プログラムの検証に適用するには力不足と考えられる。通常、並列プログラムのアルゴリズム等は公平性(fairness)、すなわち全ての実行待ちのスレッドはいつか必ず実行する機会が与えられるとの仮定のもとで設計されていることが多いが、上記のwait-notifyゲームにおいては公平性は考慮されていない。このため、公平性に依存した多くの並列プログラムに適切な意味を与えることができない。
研究開始当初は想定していなかったこの問題を解決し理論的基礎をかためるため、もう少し研究を進める必要がある。
|
| Strategy for Future Research Activity |
（１）公平性を考慮に入れた並列プログラムのゲーム意味論の確立： 「現在までの達成度」で述べた公平性の問題はwait-notifyゲームに限らず、より一般のゲーム意味論に共通する問題である。なぜなら、一般的なゲーム意味論は計算が無限ステップ行われるときのプログラムの挙動(liveness)についての仕様を何も定めないからである。今後の研究においては、ゲーム意味論がlivenessについての仕様を含むように拡張し、これによって公平な並列プログラム実行に関するゲーム意味論を確立する。この具体的な方法については、おおよそ見通しが付いている。
（２）並列プログラムの検証手法の開発： 上記の理論的基礎となる部分が完成次第、次の研究のステージとして、与えられた並列プログラムが意図した通りの動作をするかどうかをゲーム意味論の枠組みの中で判定する系統的方法の研究を行う。
ゲーム意味論で証明済みのfull abstractionによって、並列プログラムの等価性を対応するゲームの等価性のそれに還元できるが、これをそのまま並列プログラムの等価性の検証に適用することはできない。なぜなら、ゲームの等価性の判定が一般には決定不可能であるからである。この問題に対して、以下のように対処して解決を図る。
(a) 定式化したゲーム構造のさらなる解析を行い、等価性の判定を行うのに必要な条件必を明らかにする。(b) 条件に基づいて等価性の判定を行うアルゴリズムを考案する。逐次プログラミング言語についてGhicaとMcCuskerが行ったように、適切な言語サブセットを設定することによって、正規言語の等価性問題へと帰着することを計画している。(c) 上記言語サブセットについて、プログラムの等価性判定を正規言語の等価性に自動的に還元して判定するツールのプロトタイプを作成し、その実効性を調査する。
|
| Expenditure Plans for the Next FY Research Funding |
「現在までの達成度」で述べた公平性の問題に対応するための理論的基礎の完成を優先させ、並列プログラムの検証手法の開発は次年度に先送りとした。これに伴って、検証手法のプロトタイプ開発に必要なPC等の新規購入も先送りとした。
効率的な並列プログラムの検証手法の開発のためには、相当量の文献調査等が必要になるので、大学院生等に文献調査、資料整理を手伝ってもらうことで研究を加速する。そのために、研究資料として専門書等を購入するとともに、謝金の支払いを予定している。
また、得られた研究成果について、海外で開催される国際会議や、内外の研究集会などで参加・発表するため前年より旅費をより多く使用する計画である。プログラムの等価性判定をおこなうプロトタイプの作成に当たっては、十分な性能を持つPCを新規に購入する計画である。
|
Research Products
(1 results)
