| 研究課題/領域番号 |
15K15974
|
|---|
| 研究機関 | 九州工業大学 |
|---|
研究代表者 |
江本 健斗 九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2019-03-31
|
| キーワード | 定理証明支援系 / 並列プログラミング / 計算量 |
|---|
| 研究実績の概要 |
計算機に支持を与えるプログラムは，正しい結果を計算することだけでなく，それを高速に行うことも期待される．特に，昨今の大規模なデータを対象とした計算を行う並列計算においては，その並列プログラムの正しさと効率の保証が重要である．今年度の本研究は，既存の逐次プログラムに対する定理証明支援を用いた計算量保証の枠組みを，並列計算に対応するよう拡張した．具体的には次のふたつを行った：まず，２つの計算を並列に行うという記法（プリミティブ）を追加し，並列プログラムを記述可能とした．次に，その記述に対する計算量証明機構の追加を行った．この並列プログラムへの対応の中心は，並列計算時の計算量（ないし計算時間）の見積もりのための対数系として min-plus の代数系を用いたことである．これは，逐次プログラムに対する計算量証明が plus による代数系を用いて計算時間の経過を見積もっているところに，分配性を持つ min 演算を付け加えることで並列分岐に対する計算量の見積もりを可能にしたととらえることが出来る．この拡張により，簡単な再帰関数による計算，具体的にはフィボナッチ数計算やマージソート等に対し，その並列計算量の証明が容易に行えることが確認された．ただし，現状のこの拡張はまだ計算機の持つ並列性への対応レベルが低く，無限の並列性を持つ計算機を仮定した上での並列計算量の証明となっている．今後，代数系をより情報量の多い代数系に置き換えることで，有限リソース下での並列計算量証明へと拡張することを考えている．以上の並列計算量証明機構自体の進展のほか，その応用を確認するための枠組みとして大規模グラフ並列計算用関数型プログラミング言語のモデリングを進め，さらにグラフ計算アルゴリズム記述を容易にする領域特化言語をその言語上に設計した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
既存の枠組みを分配性を持つ代数系を用いて拡張することにより，幾つかの例に対して並列計算時の計算量証明が正しく動くことが示された．
|
| 今後の研究の推進方策 |
今後は有限リソース時の証明手法の確立と実問題への応用が取り組むべき課題となる．前者については，まずは並列分岐時にリソースを分割するなどの愚直なスケジューリングを対象とする．これにより，既存のデータ並列スケルトン程度までを統一的に扱えることを期待する．それを踏まえ，後者の一例として，既存のデータ並列スケルトンを組み合わせたプログラムを対象に計算量の証明を試みる．これ以降の方針としては，より高度なスケジューリングに対する証明機構の構築が考えられる．上記の愚直な分割スケジューリングは，不均等な仕事の割当時などにリソースの再配置などは考えていない．しかし，実用上は状況に応じたスケジューリングが重要となる．最適なスケジューリングで達成される計算量の証明は一般に実行状態を網羅的に扱う必要が出るため難しいが，「何らかの手法で事前に与えられたプログラムから実行時のスケジューリングがわかっている」との仮定は問題の切り分けとして妥当であると考えられる．この仮定のもと，並列計算量証明機構をスケジューリングに対してポータブル化することが課題となる．
|
| 次年度使用額が生じた理由 |
研究打合せ等の出張を別研究と合わせて行い出張費を節約したことによる．
|
| 次年度使用額の使用計画 |
研究会参加の旅費等に充てる
|
