|
前年度までの研究で、wait-notifyゲーム(渡辺氏との共同研究)の提案等によりゲーム意味論の並列実行の形式化や公平性への対応を達成してきた。研究当初から、これらをそのまま並列プログラムの検証に適用するには、並列性に起因する状態数の爆発を抑える効果的な手法が必要であることは予想されており、研究計画では正規表現で言うところのshuffle表現により状態数爆発を抑えることを予定していたが、その効果は限定的であろうとの見込みが判明していた。
本年度の研究では、この局面を打開するための技術的手段として組合せ幾何的モデルの援用を検討し、これがかなり有望であるとの確信を得ることができた。組合せ幾何的モデルは分散コンピューティングの理論で近年研究が活発に行われている手法で、並列プロセス間のコミュニケーションによる組合せ的非決定性を組合せ幾何における単体的複体（点・線・面などの図形の組合せ）の形で抽象化して表現する。このような抽象化によって状態爆発の緩和を行う手法の研究を行った。具体的には、並列プログラムの仕様を組合せ幾何的モデルで与えたとき、この仕様から導出される単体的複体上である一定の部分複体の変形を発見することで仕様を満たすプログラムを導出できることが原理的に可能であることを見出した。問題はそのような複体変形を効率良く発見することができるかどうかだが、並列プロセスの数を制限する等の一定の条件のもとで、いくつかの組合せ論的アルゴリズムを組み合わせて適用することにより現実的な時間で解が導き出せることを確認している。まだ途上の成果であるが、これらの内容については国内の研究集会で口頭・ポスター発表を行っている。
|
