自動的等価性差分の抽出によるSSAコンパイラ最適化器の生成するコードの正しさの検証

情報処理学会 Web Site

書誌事項

タイトル別名
  • ジドウテキ トウカセイ サブン ノ チュウシュツ ニ ヨル SSA コンパイラ サイテキ カキ ノ セイセイ スル コード ノ タダシサ ノ ケンショウ
  • Verification of SSA Compiler Optimizer Generated Code by Finding Value Equality Difference

この論文をさがす

抄録

目的コードの効率を向上させる最適化はコンパイラの重要なフェーズである．しかし最近の進んだ最適化器の多くは複雑なソフトウエアであるため，最適化器に誤りがあることは稀ではなく，そのときその原因を突き止めることが難しい．本論文では，最適化前後の差分を自動的に抽出し，時相論理に基づいて変数などの等価性を評価することにより SSA 形式上のコンパイラ最適化器の正しさを検証する手法を提案する．まず，変形箇所がプログラムの意味を保つために満たすべき性質を時相論理の CTL 式で記述しておく．次に，最適化前後の SSA 形式の中間言語を比較照合し，最適化による変形を抽出する．それらの結果に従ってモデルを生成し，すべての変形がその種の変形に応じた CTL 検査式を満たすかどうかをモデル検査により検査する．本手法により COINS コンパイラの最適化器の誤りや曖昧な変形をいくつも発見した．本手法では，検証者は最適化アルゴリズムを知る必要がなく，テストコードを実行する必要もない点に特徴がある．

Optimization is a very important phase of compilation. It can improve the performance of a program by a large factor. However, many recent optimizers are complex, which may compromise program correctness. It is essential that the compiler optimizer is implemented without changing the semantics of a program. Guaranteeing the correctness of optimization for realistic programs is still an open problem. In this paper, we propose a technique for validating the optimization transformation of the program by checking if the optimization transformations are equivalent transformations. First, we define the semantic equivalence of every kind of transformation and formalize them using CTL formulas. Then, we compare the intermediate programs in Static Single Assignment (SSA) form before and after optimization and extract the differences. After analysis and modelling, every transformation is checked against the corresponding CTL formula via model checking. We do not need to know the details of the optimization algorithms and execution of the test program. We applied this technique to the optimizer in the COmpiler INfraStructure (COINS) compiler. It worked with great efficiency, and found several bugs and ambiguous transformations.

収録刊行物

関連プロジェクト

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ