正しさと効率の形式的証明を備えたスケルトン並列プログラミング環境に関する研究

点击翻译按钮获取中文摘要

今年度は、大きくふたつの観点で研究を進めた。ひとつ目の観点として、まず、BSP モデルに基づく並列スケルトンの組み合わせにコンパイル可能な大規模グラフ計算記述言語について、その記述性向上のための拡張を行った。この言語は、頂点集合変数を用いた並列性を意識しない大域的視点でのグラフ計算記述を可能とする言語として設計されたものであり、今回、辺集合変数の導入と通信削減等のコンパイル時最適化の導入を行った。これにより、辺集合を用いて記述されるマッチングアルゴリズムなどの並列プログラムを、並列性を意識せずに自然に記述できるようになった。また、命令の順序入れ替えによるスーパーステップ数の削減や自明な冗長通信の削除等の最適化を導入し、コンパイル後の並列プログラムの実行性能の向上を行った。この成果については国内ワークショップでの発表を行った。もうひとつの観点として、昨年度の研究により明らかになった「並列プログラムの証明の手間がかかりすぎる」という問題点に対し、その証明の手間を軽減するための手法の開発を開始した。整数算術などの特定分野については自動証明タクティックが存在するものの、「並列プログラムの（計算量）証明」については新たな手法の開発が必要となる。基本的なアプローチとして深層学習による部分的証明の自動生成を考え、深層学習に基づく証明全体の自動生成に関する既存研究の調査してその学習モデルの拡張に着手した。