Towards parallel programming environment with certified correctness and complexity

• Project/Area Number: 15K15974
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Software
• Research Institution: Kyushu Institute of Technology
• Principal Investigator: Emoto Kento 九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
• Project Period (FY): 2015-04-01 – 2019-03-31
• Project Status: Completed (Fiscal Year 2018)
• Budget Amount: ¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000); Fiscal Year 2018: ¥390,000 (Direct Cost: ¥300,000、Indirect Cost: ¥90,000); Fiscal Year 2017: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000); Fiscal Year 2016: ¥2,730,000 (Direct Cost: ¥2,100,000、Indirect Cost: ¥630,000); Fiscal Year 2015: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
• Keywords: 定理証明支援系 / 並列プログラミング / 計算量 / 不等式 / 並列 / 並列スケルトン / グラフ / 機械証明

Outline of Final Research Achievements

Programs have to be correct and efficient. We have obtained the following two results for parallel programming with certified correctness and complexity: (1)
a consise notation in a proof assistant Coq for writing local complexity naively within the program code, to carry out a formal proof of its parallel complexity; and (2) a method for easy and natural manipulation of inequalities in formal proofs. These results have made it easier to build parallel programs with certified correctness and complexity.

Academic Significance and Societal Importance of the Research Achievements

身の回りにあふれるコンピュータが安全かつ効率的に仕事をしているのは、その仕事の指示をしているプログラムが「正しく・速く」動くように作られているからである。しかし、どのような専門家であっても、人である以上、見落としなく「正しさ」と「速さ」を保証したプログラムを作ることはできない。そのため、人ではなく、見落としをしないコンピューター自身にその「正しさ」と「速さ」を保証させることが理想である。残念なことに、コンピュータにその保証をさせるにも煩雑な手順が必要であり、コストが掛かってしまう。本研究は、その手順を簡単化する手法を開発し、そのコストを下げることでより安全かつ効率的な社会の実現に貢献する。

Research Products

• [Journal Article] A DSL for graph parallel programming with vertex subsets (2019)
  • Author(s): Kento Emoto, Fumihisa Sadahira
  • Journal Title: The Journal of Supercomputing Volume: 75 Issue: 7 Pages: 1-18
  • DOI: 10.1007/s11227-019-02821-w
  • Peer Reviewed / Open Access
• [Journal Article] 定理証明支援系Coqにおける不等式変形記法 (2018)
  • Author(s): 村田 康佑 , 江本 健斗
  • Journal Title: 情報処理学会論文誌プログラミング（PRO） Volume: 11(4) Pages: 1-12
  • NAID: 170000149918
  • Peer Reviewed
• [Presentation] Coqを用いた高度なプログラム運算定理の検証に向けて (2019)
  • Author(s): 村田 康佑 , 江本 健斗
  • Organizer: 第21回プログラミングおよびプログラミング言語ワークショップ PPL2019
• [Presentation] Coqにおける検証されたプログラム運算の拡張 (2018)
  • Author(s): 村田 康佑 , 江本 健斗
  • Organizer: 日本ソフトウェア科学会 第35回大会
• [Presentation] Coqにおける可読性の高い形式的証明に向けて (2018)
  • Author(s): 村田 康佑, 江本 健斗
  • Organizer: 第20回プログラミングおよびプログラミング言語ワークショップ (PPL 2018)
• [Presentation] 頂点部分集合変数を備えた大規模グラフ計算用領域特化言語 (2017)
  • Author(s): 定平 典久, 江本 健斗
  • Organizer: 第19回プログラミングおよびプログラミング言語ワークショップ PPL 2017
  • Place of Presentation: 笛吹市
  • Year and Date: 2017-03-08
• [Presentation] 中島 拓, 江本 健斗 (2017)
  • Author(s): Spark GraphXへのFregelコンパイラ
  • Organizer: 第19回プログラミングおよびプログラミング言語ワークショップ PPL 2017
  • Place of Presentation: 笛吹市
  • Year and Date: 2017-03-08
• [Presentation] 並列プログラム計算量の系統的機械証明手法の開発 (2017)
  • Author(s): 白水 駿, 江本 健斗
  • Organizer: 日本ソフトウェア科学会第34回大会
• [Presentation] Think like a vertex, behave like a function! a functional DSL for vertex-centric big graph processing (2016)
  • Author(s): Kento Emoto, Kiminori Matsuzaki, Zhenjiang Hu, Akimasa Morihata, Hideya Iwasaki
  • Organizer: 21st ACM SIGPLAN International Conference on Functional Programming, ICFP2016,
  • Place of Presentation: Nara, Japan
  • Year and Date: 2016-09-19
  • Int'l Joint Research
• [Presentation] 大規模グラフ並列処理のための関数型領域特化言語 Fregel とその評価 (2016)
  • Author(s): 江本 健斗, 松崎 公紀, 胡 振江, 森畑 明昌, 岩崎 英哉
  • Organizer: 日本ソフトウェア科学会第33回大会
  • Place of Presentation: 仙台市
  • Year and Date: 2016-09-07
• [Presentation] 大規模グラフ並列処理のための関数型領域特化言語 (2016)
  • Author(s): 江本 健斗，松崎 公紀，胡 振江，森畑 明昌，岩崎 英哉
  • Organizer: 第18回プログラミングおよびプログラミング言語ワークショップ（PPL2016）
  • Place of Presentation: 岡山県玉野市
  • Year and Date: 2016-03-07
• [Presentation] A Functional DSL for Large Scale Graph Processing (2016)
  • Author(s): Kento Emoto, Kiminori Matsuzaki, Zhenjiang Hu, Akimasa Morihata, Hideya Iwasaki
  • Organizer: Thirteenth International Symposium on Functional and Logic Programming (FLOPS 2016)
  • Place of Presentation: Kochi, Japan
  • Year and Date: 2016-03-04
  • Int'l Joint Research