Research on Skeletal Parallel Programming Environment with Formal Proofs of Correctness and Efficiency

2023 Fiscal Year Final Research Report

• 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
• Keywords: 並列プログラミング / 並列スケルトン / 定理証明支援系 / 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.

Free Research Field

計算機科学

Academic Significance and Societal Importance of the Research Achievements

昨今、複数のコンピュータや複数のCPU・コアを用いて計算を加速する並列計算は、AI・物理シミュレーション・ビッグデータ処理の実現において必須の技術となっている。しかし、並列計算を実現する並列プログラムの開発は難しく、特に正しく効率の良い並列プログラムが得られていることを保証することは困難である。この問題に対し、本研究は、定理証明支援系による正しさと効率の形式的保証をもった並列プログラムの系統的な開発環境を構築しようとするものであり、得られた研究成果はこの問題の解決に貢献する。