| 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 |
Emoto Kento 九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
|
|---|
| Project Period (FY) |
2019-04-01 – 2024-03-31
|
| Project Status |
Completed (Fiscal Year 2023)
|
| 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 | 並列プログラミング / 並列スケルトン / 定理証明支援系 / Coq / 形式証明 / 深層学習 / グラフ計算 / BSP モデル / 計算量証明 / 持続型例外処理 / BSPモデル / recursion scheme / coq |
|---|
| Outline of Research at the Start |
本研究は、定理証明支援系を用いた、並列プログラムの開発・最適化・証明を一貫して行える並列プログラミング環境の構築を目指す。特に、並列プログラムの正しさに加えて、その実行効率（並列計算量）の証明を支援する環境の構築に注力する。そのために、本研究は、（１－１）並列スケルトンの定理証明支援系上での形式化、（１－２）最適化のためのプログラム変換規則の形式化、（１－３）以上に付随する数学的概念の形式化、（２）定理証明支援系Coq における自動・半自動証明の為のタクティックライブラリやプラグイン開発、（３）並列実行モデルの定理証明支援系での形式化に関する研究を実施する。
|
| Outline of Final Research Achievements |
In this research, we developed formalization of parallel models and language systems on Coq and support tools for such formal proofs, to realize programming environments for certified correct/efficient parallel programs. This includes formalization of (1) the BSP model with formal proofs on user programs' computational costs, (2) new language systems useful for load-balancing in parallel programs, (3) recursion schemes that are the basis of parallel skeletons with powerful optimizations, as well as development of support tools such as libraries and semi-automatic techniques to reduce the burden of formal proofs. These results have been published in international conferences, domestic journals, and research workshops.
|
| Academic Significance and Societal Importance of the Research Achievements |
昨今、複数のコンピュータや複数のCPU・コアを用いて計算を加速する並列計算は、AI・物理シミュレーション・ビッグデータ処理の実現において必須の技術となっている。しかし、並列計算を実現する並列プログラムの開発は難しく、特に正しく効率の良い並列プログラムが得られていることを保証することは困難である。この問題に対し、本研究は、定理証明支援系による正しさと効率の形式的保証をもった並列プログラムの系統的な開発環境を構築しようとするものであり、得られた研究成果はこの問題の解決に貢献する。
|
