Home >

news ヘルプ

論文・著書情報


タイトル
和文:自動的等価性差分の抽出によるSSAコンパイラ最適化器の生成するコードの正しさの検証 
英文:Verification of Compiler Optimization Using Temporal Logic by Checking Value Equality Difference 
著者
和文: Fang Ling, 佐々政孝.  
英文: Fang Ling, Masataka Sassa.  
言語 Japanese 
掲載誌/書名
和文:情報処理学会論文誌 プログラミング 
英文: 
巻, 号, ページ Vol. 2    No. 4    pp. 35-52
出版年月 2009年8月 
出版者
和文: 
英文: 
会議名称
和文: 
英文: 
開催地
和文:東京 
英文: 
アブストラクト 目的コードの効率を向上させる最適化はコンパイラの重要なフェーズである．しかし最近の進んだ最適化器の多くは複雑なソフトウエアであるため，最適化器に誤りがあることは稀ではなく，そのときその原因を突き止めることが難しい．本論文では，最適化前後の差分を自動的に抽出し，時相論理に基づいて変数等の等価性を評価することによりSSA 形式上のコンパイラ最適化器の正しさを検証する手法を提案する．まず，変形箇所がプログラムの意味を保つために満たすべき性質を時相論理のCTL 式で記述しておく．次に，最適化前後のSSA 形式の中間言語を比較照合し，最適化による変形を抽出する．それらの結果に従ってモデルを生成し，すべての変形がその種の変形に応じたCTL 検査式を満たすかどうかをモデル検査により検査する．本手法によりCOINS コンパイラの最適化器の誤りや曖昧な変形をいくつも発見した．本手法では，検証者は最適化アルゴリズムを知る必要がなく，テストコードを実行する必要もない点に特徴がある．

©2007 Institute of Science Tokyo All rights reserved.