2022 Fiscal Year Research-status Report
正しさと効率の形式的証明を備えたスケルトン並列プログラミング環境に関する研究
| Project/Area Number |
19K11903
|
|---|
| Research Institution | Kyushu Institute of Technology |
|---|
Principal Investigator |
江本 健斗 九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
|
|---|
| Project Period (FY) |
2019-04-01 – 2024-03-31
|
| Keywords | 並列プログラミング / グラフ計算 |
|---|
| Outline of Annual Research Achievements |
今年度は、大きくふたつの観点で研究を進めた。
ひとつ目の観点として、まず、BSP モデルに基づく並列スケルトンの組み合わせにコンパイル可能な大規模グラフ計算記述言語について、その記述性向上のための拡張を行った。この言語は、頂点集合変数を用いた並列性を意識しない大域的視点でのグラフ計算記述を可能とする言語として設計されたものであり、今回、辺集合変数の導入と通信削減等のコンパイル時最適化の導入を行った。これにより、辺集合を用いて記述されるマッチングアルゴリズムなどの並列プログラムを、並列性を意識せずに自然に記述できるようになった。また、命令の順序入れ替えによるスーパーステップ数の削減や自明な冗長通信の削除等の最適化を導入し、コンパイル後の並列プログラムの実行性能の向上を行った。この成果については国内ワークショップでの発表を行った。
もうひとつの観点として、昨年度の研究により明らかになった「並列プログラムの証明の手間がかかりすぎる」という問題点に対し、その証明の手間を軽減するための手法の開発を開始した。整数算術などの特定分野については自動証明タクティックが存在するものの、「並列プログラムの（計算量）証明」については新たな手法の開発が必要となる。基本的なアプローチとして深層学習による部分的証明の自動生成を考え、深層学習に基づく証明全体の自動生成に関する既存研究の調査してその学習モデルの拡張に着手した。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
昨年度の段階で研究の大きな目標である「並列スケルトンを用いた並列プログラムに対する計算量証明を伴う形での記述を行える環境の構築」の基本技術はおよそ実現されたものの、そこで明らかになった実用に向けての課題である「証明支援技術の開発」が望ましい状況にある。また、それらを有効に活用するための、既存の形式化の改変も必要になる可能性がある。よって、上記の判断としている。
|
| Strategy for Future Research Activity |
研究の大きな目標である「並列スケルトンを用いた並列プログラムに対する計算量証明を伴う形での記述を行える環境の構築」の実用性向上に向け、その課題である「証明支援技術の開発」を継続して行う。具体的には、深層学習に基づく部分証明の自動生成による証明支援機構の開発、並列スケルトン（高階関数）に特化した自動証明タクティックの開発を進める。
|
| Causes of Carryover |
研究の遅れによる。
用途は研究成果発表のための旅費等とする。
|
Research Products
(1 results)
