佐藤 周行/SATO Hiroyuki

佐藤 周行 准教授

【研究分野】
メディア・知能・計算分野
【研究領域】
プログラミング言語・情報セキュリティとInternetトラスト
【研究室URL】
http://www-sato.cc.u-tokyo.ac.jp/

研究内容

プログラムといわれて何をイメージするかが個々人によって大きく異なるのは当然だし、健全なことであるが、そのバラエティはプログラムの持つ多様な側面を反映していることを理解しておくことが必要になる。その中でコンパイラを中心とする言語処理系はプログラムの持つ抽象的な側面(アルゴリズムまたはそれより高位の仕様の表現)と具体面における側面(ターゲットアーキテクチャで実際に動作するコードの表現)の間の「良い」かけはしになることが強く期待されている。この研究室で行われていることはコンパイラを構成する時の、上記から見たさまざまな問題に解を与えること、方法論を与えることとまとめることができる。具体的に以下にあげる活動内容はいずれもプログラム解析を軸とした理論のバックグラウンドを持っている。

最適化効果の正確な予測

現在最適化はコンパイラ研究の中心である。しかし、その効果を定量的に分析することは従来あまり行われていなかった。しかし、効果を正確に予測して適用するかどうかを判断することはコンパイラのサイエンスとしてぜひとも必要なことである。われわれはループアンローリングという最近のアーキテクチャに非常に効果的な最適化をターゲットとしてその精度の高い性能モデルを構築することに成功した。

最適化効果の正当性の証明

コンパイラ最適化は、適用後に不正確なコードを生成するようでは役に立たない。最適化の正当性の証明は、セキュリティの確保に直結する非常に重要なプロセスであり、世界的に研究が本格化している。本研究室では、最適化の正当性を保証する型システムを構築することに成功した。ここではプログラム解析に本質的なデータフロー解析を型理論で表現している。本研究の目的は検証付きコンパイラ(Verifying Compiler)をコンパイラ最適化に適用し、最適化の数理的な性質を明らかにし、適用の地平を拡大することにある。コンパイラの研究の中心である最適化において、従来、研究の展開はアドホックなノウハウの蓄積によってなされてきた。しかし、副作用を許容する最適化、性能的にトレードオフを持つ最適化群の登場など、最適化が複雑・高度になった現在では、理論的基盤を持たなければ最適化適用の正しさの証明さえ危うくなってきている。事実Gnu-Cでは、いまだに大量のバグレポートがなされている。検証付きコンパイラ(Verifying Compiler)は、もともとHoareの提唱したプログラムの正当性を併せて証明するコンパイラシステムとして21世紀の課題として提唱した概念である。本研究で目指すのは、コンパイラ最適化における上のような危機的状況に対応すべく最適化をその正しさの証明を込めて適用するコンパイラの構築であり、最適化検証つきコンパイラ(Optimization Verifying Compiler)と呼ぶべきものである。

プログラム理論のセキュリティ基盤への応用

コンパイラの研究は、プログラム言語において様々な理論的枠組をもたらした。われわれは、プログラム解析のための理論をセキュリティ解析の場に持ち込むことにより、アクセス制御やドキュメントの意味論などにおいて多くの新しい成果を得ることに成功した。現在の社会基盤の一部をなすセキュリティにおいても、われわれの研究は意味を持っているのである。

学生へのメッセージ

数学者は言う。「数学はひとつだ。」コンピュータサイエンスも同じだ。計算に関するあらゆる結果が想像もつかないような分野で花を開かせることがある。日曜大工の延長でプログラミングをするのではなくて、プログラムの表と裏で表現されているさまざまなことに興味を持って研究してみよう。豊かな世界が展開されるはずだ。

図1:最適化検証つきコンパイラの2つの側面
図2:最適化検証つきコンパイラの2つの側面