准教授
えもと けんと
同じことを計算するプログラムなのになぜ私のプログラムは遅いのか？どうしたら速いプログラムを書けるのか？この辺りの疑問を持ってしまったことが現在の研究に至るきっかけだと思います。優秀な並列アルゴリズムを実装すれば良いだけなのですが，毎度それをやるのは面倒なので，楽をできる部分は楽をできるようにと研究をしています。
速くて正確なプログラムを簡単に
情報学基礎・ソフトウェア、並列プログラミング
スケルトン並列プログラミング、プログラム変換、分散並列処理、言語処理系
今の研究を一言で言うと，「正しく速いプログラムを作る簡単なプログラミング環境の実現」です。特に，近年は「速いプログラムとは，複数の計算機（コア）を同時に利用することで高速に計算を行う並列プログラムでなければならない」という状況にあるため，本研究も必然的に並列プログラミングを対象としています。一台の計算機を使うだけの逐次プログラムに比べ，複数の計算機上で複雑に動作する並列プログラムの開発は一般に困難であり，その困難さの低減が研究目標です。
この困難の一因は並列プログラムが構造化されていないことにあります。現在の逐次プログラムは「順次・反復・分岐」という３種類のブロックで構造化されており，我々はそれらの組合せとして正しい逐次プログラムを簡単に作ることができます。この研究では，同様に並列プログラムをブロック（スケルトンと呼ぶ）で構造化することを目標に，様々な並列プログラムを構造化できるブロックとその最適化を開発しています。これらの研究成果はオープンソースライブラリとして一般に広く公開しています。
並列プログラム開発の困難の一因として，効率的な並列アルゴリズムの設計が一般に困難であるという点もあります。ただ，効率を無視すれば並列に動くアルゴリズムはしばしば簡単に設計が可能です。故に，この研究では，効率を無視した愚直なアルゴリズム記述から効率的な並列プログラムを自動合成する手法を開発しています。例えば，宇宙の終焉まで計算が終わらない愚直なアルゴリズム記述から，数秒で答えが得られる効率的並列プログラムを自動的に合成することも可能です。研究成果は随時オープンソースライブラリ等として広く一般に公開しています。
最後に。プログラムに関して最も重要な事はその正しさです。この研究では，我々の提供するライブラリ等の正しさを定理証明支援系で機械的に証明することを試みています。ライブラリを証明することにより，ライブラリユーザのプログラムの正しさが証明できるようになります。
