Document

時相論理を用いた
コンパイラ最適化器の
実行の正しさの検査
東京工業大学
佐原聡一郎佐々政孝
研究背景

コンパイラの最適化


重要な技術で研究が盛ん
複雑でバグが混入しやすい



プログラムの意味を変えてしまう致命的なものかも
バグが発見しずらい
最適化器の正しさを保証できないか？

３つのアプローチ
1.
2.
3.
最適化器そのものにバグがないことを検査
最適化の実行に誤りがなかったことを検査
多くのテストによる信頼性の向上
関連研究
1.
バグがないと保証された最適化器

Laceyらの研究 [2002]

CTL-FVとモデル検査による最適化システム


2.
システム上では最適化器の正しさの証明が簡単
扱える最適化に制限がある
最適化の実行に誤りがなかったことの検査

Neculaの研究 [2000]

最適化実行後の記号実行を用いた検査


高速で最適化に依存せず実用的
検査が正しく行える保証がない
目標

最適化器実行の正しさを保証する手法
 現実に存在する最適化器を扱えるように
 実用的であるように


実装が困難すぎない、現実的な時間内の検査、など
誤った最適化に気付ければよい
 最適化器自身の正しさを保証できなくてもよい
 毎回の最適化の実行が正しかったかどうか
最適化器の構成
解析

変形
プログラムの解析
 変形すべき箇所を探し出す
 データフロー方程式など

プログラムの変形
 解析により求めた箇所を変形する
提案手法の概要
解析
変形
検査

正しい
変形が正しかったかどうかを検査
 変形箇所の満たすべき性質をCTL-FVで記述
実行パスに沿った論理で直観的
 モデル検査のコストが小さい

 最適化実行後にモデル検査

変形箇所ごとの検査
提案手法の詳細
x=a+b
end
x は使用されない

簡単な無用命令除去
 使われない変数への代入文削除
提案手法の詳細
¬E(true U use(x)) ?
x=a+b

 使われない変数への代入文削除
rm, x
OK
簡単な無用命令除去

変形箇所の正しさ
x
end
x は使用されない

は以後使用されることはない
 ¬EF(use(x))
E (true U use( x))
変形箇所にマーク付け
 最適化器を拡張（AOP利用）

モデル検査
 マークに関するCTL-FV式の検査
最適化器の拡張
optimize() {
pos = analyze()
foreach (p in pos) {
transform(p)
}
}

拡張ポイント
 変形を行うコードの箇所

 マーク付けコードの挿入


optimize() {
pos = analyze()
foreach (p in pos) {
transform(p)
marking(p)
}
}
transform(p)
marking(p)
AOPの利用
 pointcut

transform(p)
 weave

marking(p)
CTL-FVの構文と意味
φ:: prop
| φ
|φφ
| Eψ
| Aψ

| Eψ

| Aψ
ψ:: Xφ
| Gφ
|φUφ
|φWφ
ループ不変式移動

ループ不変式を移動
 一時変数への代入文を挿入
 元の式の計算を一時変数で置換

正しいための条件
 挿入箇所
 一時変数 t は他で定義されない
x=a+b

E (true U (node(n)  def
¬EF(¬node(n)∧def(t))
∧ (t ))) 

¬rEF(¬node(n)∧def(t))
E (true U (node(n)  def (t )))
 置換箇所
 前方に挿入箇所が必ず存在する
 その間、式の値は変わらない

 rA(trans(e)
A(trans(e) W
W mark(ins,t,e))
mark(ins, t, e))
＊SSA形式を仮定
ループ不変式移動
t=a+b

ループ不変式を移動
 一時変数への代入文を挿入
ins,t,e OK
 元の式の計算を一時変数で置換

正しいための条件
 挿入箇所
 一時変数 t は他で定義されない
x=a+b
x=t
rpl,t,e OK
＊SSA形式を仮定

E (true U (node(n)  def
¬EF(¬node(n)∧def(t))
∧ (t ))) 

¬rEF(¬node(n)∧def(t))
E (true U (node(n)  def (t )))
 置換箇所
 前方に挿入箇所が必ず存在する
 その間、式の値は変わらない

 rA(trans(e)
A(trans(e) W
W mark(ins,t,e))
mark(ins, t, e))
ループ不変式移動のバグ

例外の発生する式の移動
 計算のないパスに挿入不可
 例外が発生するようになるかも
 挿入点が追加で満たすべき性質
 全てのパスに元々計算があった
A(trueW
Wmark(rpl,t,e))
m ark(rpl, t , e))
 A(true
x=a/b

COINSのバグ
 未知のバグ
 SPECを用いて検査中に発見
 テストで発見されなかった潜在的バグ
＊SSA形式を仮定
ループ不変式移動のバグ
t=a/b

例外の発生する式の移動
 計算のないパスに挿入不可
 例外が発生するようになるかも
ins,t,e NG
 挿入点が追加で満たすべき性質
 全てのパスに元々計算があった
A(trueW
Wmark(rpl,t,e))
m ark(rpl, t , e))
 A(true
x=a/b
x=t
rpl,t,e

COINSのバグ
 未知のバグ
 SPECを用いて検査中に発見
 テストで発見されなかった潜在的バグ
＊SSA形式を仮定
条件分岐を考慮した定数伝播
B1

t0=0
抽象実行に基づく最適化

プログラムを順にたどることで解析

B2
t1=φ(t0,t3)
t1==0 ?
t2=t1+1
B3


B4
複雑な最適化

Laceyらの手法では行えない最適化

B5
t3=φ(t1,t2)
g=2*t3
g<=0 ?
常にt1==0が成立
B4は通らない


全ての辺を通るかもという前提
⇒ t1が0となることが解析できない
単純なデータフロー方程式でも行えない
本手法による最適化後検査は可能

t1==0が本当に正しいかは検査は可能
B6
＊SSA形式
＊詳細は省略
条件分岐を考慮した定数伝播
B1

t0=0
抽象実行に基づく最適化

プログラムを順にたどることで解析

B2
t1=φ(t0,t3)
t1==0 ?
t2=t1+1
B3


B4
複雑な最適化

Laceyらの手法では行えない最適化

B5
t3=φ(t1,t2)
g=2*t3 0
g<=0 ?
常にt1==0が成立
B4は通らない


全ての辺を通るかもという前提
⇒ t1が0となることが解析できない
単純なデータフロー方程式でも行えない
本手法による最適化後検査は可能

t1==0が本当に正しいかは検査は可能
B6
＊SSA形式
＊詳細は省略
COINSの最適化器への適用

行数
拡張
357
2
cstp
1143
5
2
 条件分岐付定数伝播
cpyp
143
3
2
(cstp)
 コピー伝播(cpyp)
 共通部分式除去(cse)
 無用命令除去（dce)
cse
408
7
1
dce
480
3
lcm
1259
2
SSA形式
 ループ不変式移動(hli)

hli

 部分冗長除去(lcm)
拡張箇所は少ない

通常形式


改変
⇒ マークも少ない
探し出すのも容易
ソースの改変もほぼない

ポイントカットの都合のみ
本手法の考察

論理式の記述について
 記述量は少ない
 変形箇所自体が少ない
 論理式は変形箇所一つにつき、1～3行程度
 最適化のきちんとした理解が必要
 論理式の記述は決して容易というわけではない
 最適化器製作者なら可能な範囲か

バグの原因特定の容易さについて
 論理式のモデル検査で反例
⇒ 式に関する変形は誤りであった
 バグを発見した際の原因特定は容易
本手法の考察

正しさの保証について
 検査付コンパイルは高信頼
 「誤った最適化に気づかずプログラム実行」とはならない
 テストだけでは得られない信頼性

次に最適化コンパイルするプログラムの正しさは保証外
 厳密なプログラムの意味保存を示すものではない
 論理式を満たす≠プログラムの意味が保存される


ギャップを埋めるための証明が必要になる
ただし、直観的にはほぼ明らかか
 Lacey＞本手法≒ Necula≫テスト
 Laceyらの最適化器は常に正しい（証明付の場合）

ただし、扱えるのは簡単な最適化のみという制限がある
検査時間の計測実験

目的
 検査にかかる時間が現実的であることを確かめる

実験環境
 Intel Pentium 4 CPU 2.80GHz
 Linux 2.6.17-13msmp
 JavaVM 1.5.0_08
 Heap 256Mbyte、Stack 2Mbyte
 COINS 1.4.1
 最適化O2 に相当するSSA最適化オプション
 GluonJ 1.2
 ベンチマーク
 SPEC CPU2000 version1.2 から14本
1.m
cf
p
m
m
ke
su
8.a
m
ua
9.a
rt
17
3.e
q
18
18
19
af
ty
7.p
ar
se
r
25
4.g
ap
25
5.v
or
te
x
25
6.b
z ip
2
30
0.t
wo
lf
17
1.s
wi
m
17
2.m
gr
id
17
7.m
es
a
6.c
r
18
18
r
17
5.v
p
p
m
m
su
18
8.a
m
ke
9.a
rt
ua
18
3.e
q
17
p
5.v
or
te
x
25
6.b
z ip
2
30
0.t
wo
lf
17
1.s
wi
m
17
2.m
gr
id
17
7.m
es
a
25
r
rs
e
af
ty
cf
4.g
a
25
7.p
a
19
18
6.c
r
r
5.v
p
18
1.m
17
検査時間の計測実験
最適化時間の比
30

25
5

総コンパイル時間の比
2
1.5
1
0.5
0
コンパイル時間の比較

20
15
10

0

3
2.5

検査on/offの比





最適化時間比
総コンパイル時間比
あくまで参考値
検査した最適化は一部
考察
速度比
最適化のみでは15倍
総コンパイル時間では1.7倍
高速化も十分可能
 現実的な時間の範囲内
まとめ

最適化実行後に正しかったかどうかを検査
 変形箇所がCTL-FV式を満たせば正しいと判断
 最適化後のプログラムをモデル検査

特徴
 既存の手書きの最適化器に適用可能
 複雑な最適化器でも扱える可能性
 バグを発見した際の原因特定が容易
 常に検査を行うことで高い信頼性
 検査時間は現実的な範囲
今後の課題

正しさの厳密な証明
 時相論理による証明はいくつか行われている
Laceyらの証明法、各最適化ごとの証明、など
 本手法においても同様にして行えると期待


さらに多くの最適化器に適用
 演算の強さ軽減、PREQPなどに適用可能か？

検査の高速化
 本手法に特化したモデル検査

データフロー方程式のビットベクトル法の応用
おわり
CTL-FVの例

A(φ1Uφ2)
 全パスでφ2の成立までφ1が常に成立

φ2の成立する状態が必ずある
{

s |= A(φ1Uφ2) } = {3,4,8}
A(φ1Wφ2)
 全パスで以下のいずれかが成立


{
φ2の成立までφ1が常に成立
φ2が成立せず、永遠にφ1が成立でもよい
 ループし続けるパスの考慮の回避
s |= A(φ1Wφ2) } = {3,4,5,6,7,8}
本手法の考察

厳密な意味での正しさについて
 厳密な意味での「検証」ではない
式を満たした≠最適化が正しく行われた
 厳密には証明が必要


ただし、直観的にはほぼ明らかといえる
 Lacey＞本手法≒
Necula＞テスト
Laceyらの最適化器は常に正しい（証明付の場合）
 プログラムは無限にあるので、全テストは無理


次に最適化コンパイルするプログラムの正しさは保証外
条件分岐を考慮した定数伝播
B1
B2

t0=0
抽象実行に基づく最適化


t1=φ(t0,t3)
t1==0 ?

CTL-FVの記述では…

t2=t1+1
B3
常にt1==0
B4は通らない
B4
t1が取る値を解析するのは無理


B5
t3=φ(t1,t2)
g=2*t3
g<=0 ?

t1==0という解析結果の検査は可能


Laceyらの手法では行えない最適化
データフロー方程式でも行えない
本手法では検査可能
Laceyらが扱えない最適化も検査可能

「解析」は「結果の検査」より大変
B6
＊詳細は省略
条件分岐を考慮した定数伝播
B1
B2

t0=0
抽象実行に基づく最適化


t1=φ(t0,t3)
t1==0 ?

CTL-FVの記述では…

t2=t1+1
B3
常にt1==0
B4は通らない
B4
t1が取る値を解析するのは不可能


B5
t3=φ(t1,t2)
g=2*t3 0
g<=0 ?

t1==0という解析結果の検査は可能


Laceyらの手法では行えない最適化
データフロー方程式でも行えない
本手法では検査可能
Laceyらが扱えない最適化も検査可能

「解析」は「結果の検査」より大変
B6
＊詳細は省略

Download Report