| 研究課題/領域番号 |
19K11903
|
|---|
| 研究機関 | 九州工業大学 |
|---|
研究代表者 |
江本 健斗 九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2024-03-31
|
| キーワード | 並列プログラミング / グラフ計算 |
|---|
| 研究実績の概要 |
今年度は、大きくふたつの観点で研究を進めた。
ひとつ目の観点として、まず、BSP モデルに基づく並列スケルトンの組み合わせにコンパイル可能な大規模グラフ計算記述言語について、その記述性向上のための拡張を行った。この言語は、頂点集合変数を用いた並列性を意識しない大域的視点でのグラフ計算記述を可能とする言語として設計されたものであり、今回、辺集合変数の導入と通信削減等のコンパイル時最適化の導入を行った。これにより、辺集合を用いて記述されるマッチングアルゴリズムなどの並列プログラムを、並列性を意識せずに自然に記述できるようになった。また、命令の順序入れ替えによるスーパーステップ数の削減や自明な冗長通信の削除等の最適化を導入し、コンパイル後の並列プログラムの実行性能の向上を行った。この成果については国内ワークショップでの発表を行った。
もうひとつの観点として、昨年度の研究により明らかになった「並列プログラムの証明の手間がかかりすぎる」という問題点に対し、その証明の手間を軽減するための手法の開発を開始した。整数算術などの特定分野については自動証明タクティックが存在するものの、「並列プログラムの（計算量）証明」については新たな手法の開発が必要となる。基本的なアプローチとして深層学習による部分的証明の自動生成を考え、深層学習に基づく証明全体の自動生成に関する既存研究の調査してその学習モデルの拡張に着手した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
昨年度の段階で研究の大きな目標である「並列スケルトンを用いた並列プログラムに対する計算量証明を伴う形での記述を行える環境の構築」の基本技術はおよそ実現されたものの、そこで明らかになった実用に向けての課題である「証明支援技術の開発」が望ましい状況にある。また、それらを有効に活用するための、既存の形式化の改変も必要になる可能性がある。よって、上記の判断としている。
|
| 今後の研究の推進方策 |
研究の大きな目標である「並列スケルトンを用いた並列プログラムに対する計算量証明を伴う形での記述を行える環境の構築」の実用性向上に向け、その課題である「証明支援技術の開発」を継続して行う。具体的には、深層学習に基づく部分証明の自動生成による証明支援機構の開発、並列スケルトン（高階関数）に特化した自動証明タクティックの開発を進める。
|
| 次年度使用額が生じた理由 |
研究の遅れによる。
用途は研究成果発表のための旅費等とする。
|
