2014 Fiscal Year Research-status Report
ゲーム意味論による共有メモリ型並列プログラムの定式化と検証
| Project/Area Number |
24500014
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
西村 進 京都大学, 理学(系)研究科(研究院), 准教授 (10283681)
|
|---|
| Project Period (FY) |
2012-04-01 – 2016-03-31
|
| Keywords | 並列プログラム / ゲーム意味論 / プログラム検証 |
|---|
| Outline of Annual Research Achievements |
共有メモリ型並列プログラムのゲーム意味論に関する研究、特に当該年度では公平性を考慮した場合のゲーム意味論についての研究を行った。
もともとゲーム意味論は逐次的プログラムのために提案されたものであったが、wait-notifyゲーム(渡辺氏との共同研究)やその数学的構造の解明など、昨年度までの研究成果によりこれを並列プログラムにも可能であることをすでに示してきた。
しかしながら、これまでの結果をもってしても公平性(fairness)を考慮した並列実行に対して適切な意味を与えることができなかった。なぜなら、ゲーム意味論は公平性のように無限長のゲーム列を考慮する必要がある活性(liveness)を記述することを考慮していないからである。また、並列実行による非決定的実行と公平性との組合せは、通常のプログラムでは非有界非決定性(unbounded nondeterminism)を誘導するため、意図しないプログラムの発散を導出してしまうという問題があった。
これらの問題を解決するため、以前提案したwait-notifyゲームの枠組みを詳細化し、並列プログラムの公平実行のためのゲーム意味論を構築した。この詳細化されたwait-notifyゲームでは、非決定的選択も計算資源の一種であるとみなし、これら計算資源へのアクセスを表すゲーム手をゲーム列中に明示的に挿入することにした。これにより、すべての並列実行のゲーム列における可能な非決定的選択肢の数が、先行する非決定性資源へのアクセス回数によって定まる上限で抑えられることを示した。これをWN有界ゲーム戦略とよび、このようなWN有界ゲーム戦略によるゲーム意味論がfull abstractであることを示した。この結果について、日本ソフトウェア科学会第３１回大会において講演発表を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
共有メモリ型並列プログラムのゲーム意味論の理論的基礎については、当該年度までの研究により、wait-notifyゲームによる並列実行の形式化および公平性への対応が達成できた。
しかしながら、その実用性の観点から見た場合、この理論を並列プログラムの検証に適用するにはその実行効率の面で問題がある。すなわち、効率的な並列プログラム検証を実現するには、並列性に起因する状態数（ゲーム意味論においては可能なゲーム列の数）の爆発を抑える効果的な手法が必要であると考えられる。研究開始当初は、並列プロセスのインターリーブ実行を正規表現で言うところのshuffleで表現することにより状態数爆発を抑えられるものと予想していたが、その効果は限定的であろうといのが現在の見込みであり、この局面を打開するための技術的手段の開発が課題となっている。
|
| Strategy for Future Research Activity |
「現在までの達成度」で述べたように並列プログラムの効率的な検証のためには、並列性に起因する状態数の爆発を抑えるための手法の開発が喫緊の課題である。次年度の研究では、並列性から誘導される組合せ爆発の問題を、組合せ幾何的なモデルを併用することで解決することを試みる。組合せ幾何による並列性の定式化は、分散コンピューティングの理論で近年研究が活発に行われている手法で、並列プロセス間のコミュニケーションによる組合せ的非決定性を、組合せ幾何における単体的複体（点・線・面などの図形の組合せ）の形で抽象化して表現する。理論分散コンピューティングの分野では、特定のクラスの分散計算タスクの実現不可能性を示すのに有効な手法としてよく研究されている。この抽象化の手法を並列プログラムの検証に応用し、並列計算によって誘導される組合せ的爆発を単体的複体として抽象化することによって状態爆発の問題を解決することを試みる。
単体的複体に関する組合せ幾何は計算幾何学とも相性が良い分野であり、既存の幾何計算アルゴリズムが適用できると期待される。このようなアルゴリズムを援用した並列プログラムの検証システムのプロトタイプを開発する予定である。
|
| Causes of Carryover |
「現在までの達成度」で述べた、並列性に起因する状態数の爆発を抑える手法について当該年度中に実現が間に合わず、そのために予定していた成果発表や並列プログラムの検証のプロトタイプ作成を先送りしたため若干の繰越が生じた。
|
| Expenditure Plan for Carryover Budget |
研究最終年度にあたって、その研究成果の発表や検証システム作成のために繰越分を有効活用していく。
|
Research Products
(1 results)
