| 研究課題/領域番号 |
19K11903
|
|---|
| 研究機関 | 九州工業大学 |
|---|
研究代表者 |
江本 健斗 九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2023-03-31
|
| キーワード | 定理証明支援系 / recursion scheme / coq |
|---|
| 研究実績の概要 |
本年度の研究は、主に、並列スケルトンの数学的な定式化の基礎である recursion schemes の定理証明支援系上での形式化を行った。また、提案手法による検証対象となるような、並列スケルトンを用いたアプリケーションの開発を行った。
map や reduce に代表される、効率化のための融合変換を備えたスケルトンは、数学的に recursion schemes により定式化されている。この定式化により、様々なデータ構造に対する並列スケルトンが統一的に扱えるようになっている。本研究では、それらに対する形式的検証を可能とするために、並列スケルトンの定式化などに使われる代表的な recursion schemes について、定理証明支援系 Coq での形式化をおこなった。この研究成果は査読付き国際会議 APLAS2019 に採択され、発表した。
また、その形式化の際に、ストリームなどを扱う一部の並列スケルトンの定式化の基礎となる recursion schemes については、定理証明支援系 Coq での形式化が難しいという課題を発見した。この課題については、二通りの解決策を提案し、その評価等を進めているところである。これについては国内の査読付き研究会に採択され、発表を行った。
さらに、並列スケルトンの一種である Hadoop MapReduce を用いたアプリケーションとして、大規模ランダムグラフの生成を行うプログラムを構築した。これは、大規模なデータを扱うため、想定通りの計算量であることが強く期待される並列プログラムである。そのため、本研究の構築する計算量証明手法の適用例となる予定である。これについては国内学会の大会にて口頭発表を行った。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
まず、融合機能を持つ並列スケルトンの定理証明支援系を用いた形式化の基礎となる、recursion schemes の形式化を行った。これは、基本的な map や reduce といった並列スケルトンを統一的に扱う基盤となる。
また、ストリームを対象とするような一部の並列スケルトンに対し、そもそも定理証明支援系によるの定式化の難しさがあるという課題を発見することができた。また、それに対する解決策の提案も行えた。
さらに、手法の適用先となるアプリケーションの用意も行った。
以上の成果を得たことにより、おおむね順調に研究が進展していると判断する。
|
| 今後の研究の推進方策 |
今後、まずは具体的な並列計算モデルを定め、その上での各並列スケルトンの並列計算量の検証に取り組む。具体的には、現実の並列計算機をよく表現するが単純である、BSP（Bulk Synchronous Parallel）モデルを並列計算モデルを対象とする。この BSP の元で、recursion schemes ないし個々の並列スケルトンに対する計算量を定理証明支援系を用いて形式化する。ただし、並列スケルトンや recursion schemes が本質的に高階関数であることから、既存の具体的な関数に対する形式化手法を単純に適用することはできない。そのため、計算量に関する変換器としての適切な形式化が主なポイントとなる。
|
| 次年度使用額が生じた理由 |
COVID-19 により予定通りの物品購入・出張ができなかったことによる。
予定通りの出張ができない状況が続くため、当初計画よりも一段高性能の計算機を購入するなど、状況に応じて効果的に研究を遂行できるよう柔軟に予算執行を行う。
|
