| 研究概要 |
1. 時相論理を用いたコンパイラ最適化器の検証
最適化器が正しいかどうかを,時相論理で記述した仕様が満たされているか否かによって検証する方法を開発した.これは,最適化前と最適化後の中間コードを,合同集合を作成しながら比較する.最適化前の中間コードを基にKripke構造とそのラベルを作成し,比較結果が異なっている場合には,ラベルに「追加」,「削除」,「置換」の情報を追加する.「追加」,「削除」,「置換」が満たすべき仕様を時相論理の一種であるCTL論理によってあらかじめ作成しておき,これを用いてモデル検査を行う.モデル検査の結果,バグがあると報告される.この手法は,既存の手書きの最適化二器に適用でき,しかも検証者は最適化アルゴリズムやその実装を知る必要がない点が大きな特徴である.これにより,コンパイラ・インフラストラクチャCOINSの最適化のバグをいくつか見つけることができた.
2. 要求駆動型部分無用コード除去
プログラムの実行経路によっては使用されないことがある代入文を,適切なプログラム点に移動させて除去する部分無用コード除去を,必要に応じて行う効率的な手法を提案した。本手法を,プログラム中の実行コストの高い部分に適用することによって,必要最低限のコンパイルコストで,部分無用コード除去を適用することができる.
|
