正しさと効率の形式的証明を備えたスケルトン並列プログラミング環境に関する研究
| Project/Area Number |
19K11903
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Kyushu Institute of Technology |
|---|
Principal Investigator |
江本 健斗 九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
|
|---|
| Project Period (FY) |
2019-04-01 – 2024-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2022: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2021: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2020: ¥2,340,000 (Direct Cost: ¥1,800,000、Indirect Cost: ¥540,000)
Fiscal Year 2019: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
|
|---|
| Keywords | 並列プログラミング / グラフ計算 / BSP モデル / 並列スケルトン / 定理証明支援系 / 計算量証明 / 持続型例外処理 / BSPモデル / recursion scheme / coq |
|---|
| Outline of Research at the Start |
本研究は、定理証明支援系を用いた、並列プログラムの開発・最適化・証明を一貫して行える並列プログラミング環境の構築を目指す。特に、並列プログラムの正しさに加えて、その実行効率（並列計算量）の証明を支援する環境の構築に注力する。そのために、本研究は、（１－１）並列スケルトンの定理証明支援系上での形式化、（１－２）最適化のためのプログラム変換規則の形式化、（１－３）以上に付随する数学的概念の形式化、（２）定理証明支援系Coq における自動・半自動証明の為のタクティックライブラリやプラグイン開発、（３）並列実行モデルの定理証明支援系での形式化に関する研究を実施する。
|
| 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 |
研究の大きな目標である「並列スケルトンを用いた並列プログラムに対する計算量証明を伴う形での記述を行える環境の構築」の実用性向上に向け、その課題である「証明支援技術の開発」を継続して行う。具体的には、深層学習に基づく部分証明の自動生成による証明支援機構の開発、並列スケルトン（高階関数）に特化した自動証明タクティックの開発を進める。
|
Report
(4 results)
Research Products
(8 results)
