| 研究課題/領域番号 |
19K11903
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 九州工業大学 |
|---|
研究代表者 |
江本 健斗 九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2024-03-31
|
| 研究課題ステータス |
完了 (2023年度)
|
| 配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2022年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2021年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2020年度: 2,340千円 (直接経費: 1,800千円、間接経費: 540千円)
2019年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
|
|---|
| キーワード | 並列プログラミング / 並列スケルトン / 定理証明支援系 / Coq / 形式証明 / 深層学習 / グラフ計算 / BSP モデル / 計算量証明 / 持続型例外処理 / BSPモデル / recursion scheme / coq |
|---|
| 研究開始時の研究の概要 |
本研究は、定理証明支援系を用いた、並列プログラムの開発・最適化・証明を一貫して行える並列プログラミング環境の構築を目指す。特に、並列プログラムの正しさに加えて、その実行効率（並列計算量）の証明を支援する環境の構築に注力する。そのために、本研究は、（１－１）並列スケルトンの定理証明支援系上での形式化、（１－２）最適化のためのプログラム変換規則の形式化、（１－３）以上に付随する数学的概念の形式化、（２）定理証明支援系Coq における自動・半自動証明の為のタクティックライブラリやプラグイン開発、（３）並列実行モデルの定理証明支援系での形式化に関する研究を実施する。
|
| 研究成果の概要 |
本研究では、定理証明支援系での形式証明を経た正しい（並列）プログラムの構築に対し、その支援技術の開発や具体的なモデル・言語機構の形式化を行った。形式化については、計算量を含めた低層並列計算モデル、並列計算のための負荷分散等を実現できる言語機能、並列プログラムの構成パーツ等の定式化の基礎となる recursion schemes の定理証明支援系での形式化を行った。支援技術については、これらの証明を簡単化するためのライブラリやシステムの構築を行った。これらの取り組みで得られた成果は、国際会議や国内雑誌、国内大会・研究会等で発表した。
|
| 研究成果の学術的意義や社会的意義 |
昨今、複数のコンピュータや複数のCPU・コアを用いて計算を加速する並列計算は、AI・物理シミュレーション・ビッグデータ処理の実現において必須の技術となっている。しかし、並列計算を実現する並列プログラムの開発は難しく、特に正しく効率の良い並列プログラムが得られていることを保証することは困難である。この問題に対し、本研究は、定理証明支援系による正しさと効率の形式的保証をもった並列プログラムの系統的な開発環境を構築しようとするものであり、得られた研究成果はこの問題の解決に貢献する。
|
