2014 Fiscal Year Annual Research Report
非正則なデータ構造上の非数値計算問題に対するスケルトン並列プログラミングの応用
| Project/Area Number |
24700025
|
|---|
| Research Institution | Kyushu Institute of Technology |
|---|
Principal Investigator |
江本 健斗 九州工業大学, 大学院情報工学研究院, 助教 (00587470)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | スケルトン並列プログラミング / 機械証明 / グラフ計算 |
|---|
| Outline of Annual Research Achievements |
本年度は、グラフに代表される非正則なデータ構造上の容易な並列プログラミングのための、愚直な計算仕様記述からの効率的プログラム生成手法の構築のため、以下の2点についての成果を得た：（１）列上の計算問題に関する計算仕様からの効率的プログラムの自動導出を行う自動最適化ライブラリの機械証明付きの定式化とプロトタイプ実装、（２）既存の効率化手法とプログラム変換による効率的プログラム導出との同時適用による大規模な非正則データ構造のための条件付き最適解探索アルゴリズムの構築及び実装。
（１）については、グラフ上の計算では計算仕様と効率的な実装との間のギャップが大きく、その等価性の証明を手で行うこと及びその導出の実装を正しく行うことが困難であるという問題の解決のため、Coq による機械証明をその両者（等価性及び実装の正しさ）に適用するための土台の定式化を試みたものである。この定式化には、スケルトンによるプログラムの構造化が重要な役割を果たしている。この成果により、非正則なデータ構造上の容易な並列プログラミング環境を正しく提供するための基盤が示された。
（２）については、様々な最適化問題が帰着されうるグラフ上の最短路問題に対し、既存のグラフ前処理による高速化手法とプログラム変換による愚直な記述からの効率的なプログラム導出手法とを組み合わせた、大規模な非正則データ構造のための容易な条件付き最適解探索アルゴリズムの構築と実装を行った。本成果では、これらふたつの手法を完全に組み合わせることは出来ないことを指摘し、前処理による高速化手法を前提にしつつプログラム変換側の適用範囲を狭めることで、両者を同時に利用できる枠組みを示した。この枠組は、大規模な非正則データ構造上の最適化問題に対して愚直な記述から効率的な並列プログラムを与えるプログラミング環境の基盤のひとつとなる。
|
