| 研究課題/領域番号 |
15K15974
|
|---|
| 研究機関 | 九州工業大学 |
|---|
研究代表者 |
江本 健斗 九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2019-03-31
|
| キーワード | 並列スケルトン / グラフ / 機械証明 |
|---|
| 研究実績の概要 |
目的の計算に対し、正しく効率的な並列プログラムを容易に作成する為の環境構築が望まれている。本研究は、そのような環境の構築を、基本並列計算パタン（スケルトン）と最適化のためのプログラム変換技術に定理証明支援系による機械的証明を組み合わせて実現しようとするものである。
本年度は、主に、実用的な計算対象であるグラフに対してその上の基本並列計算パタンであるスケルトンの定式化を行い、また、定理証明支援系における計算効率（計算量）の証明手法に関する調査を行った。任意の計算を対象としての計算量の証明は一般に難しい。対象とするデータ構造のサイズを捉え得る事のできる計算パタンを用意する必要がある。そこで、並列計算が強く望まれる実用的なデータ構造であるグラフを対象に、その並列計算の核となる計算パタンの定義を行い、また、それらで構成されたプログラムを既存の実行環境で実行可能な構成に変換するプログラム変換規則を構築した。その上で、幾つかの実用的な計算例について、簡便な記述が可能であること及びその記述からプログラム変換を経て既存の実行環境で実行可能なプログラムが得られることを確認した。上記の変換及び今後開発されるであろう各種最適化変換の変換前後の並列プログラムの計算量に関する性質を機械的に証明可能とする技術の構築を目指し、計算量の機械証明に関する既存技術の調査を行った。逐次プログラムに対する結果は実用的な証明手法を含めいくつか研究があるものの並列プログラムに関する結果は未だ得られていない状況であることが判明したが、一方で、最新の既存手法が使用しているモナドと呼ばれる代数構造に拡張を入れることで並列プログラムへの対応が比較的素直に行えるであろうとの着想を得た。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
プログラムの正しさ及び計算量の証明のためのグラフ上の基本計算パタンの定式化が行われ、また、基本計算パタンで記述されたプログラムに対する変換規則の構築も行われた。そして、これらの定式化で記述されたプログラムから既存の並列計算機環境で並列実行可能なプログラムが生成されることも示され、定式化が実用的な問題に対して使えるものであることが示された。また、これらの機械証明の実現のために既存技術の調査を行い、並列プログラムへの拡張に対する着想を得た。以上を持って概ね順調に進展していると判断する。
|
| 今後の研究の推進方策 |
今後の研究の第一の目標は、逐次プログラムだけを対象とする既存の計算量機械証明手法を並列プログラムへ拡張することである。そのために、本年度の調査で得た着想をまずは単純な列上の基本並列計算パタンに対する並列計算量の証明を通して具体化する。その後、本年度定式化したグラフ上の基本並列計算パタン等へ具体化された技術を適用する。また、基本並列計算パタンに関する各種の変換規則に関し、それが変換前後で計算量を保存・改善することの証明を試みる。そして、既存の証明付き自動最適化ライブラリを計算量改善保証付きの自動最適化ライブラリとすることを最終的な目標とする。
|
| 次年度使用額が生じた理由 |
計画時からの時間経過等による誤差である。無理に消費せず、次年度の予算と合わせて効果的に使うこととした。
|
| 次年度使用額の使用計画 |
当初計画の物品購入費に充当するものとする。
|
