A Provably Sound TAL for Back-end Optimization について

Presentation on theme: "A Provably Sound TAL for Back-end Optimization について"— Presentation transcript:

1 A Provably Sound TAL for Back-end Optimization について
前田俊行

2 この論文が主張するところの 既存の TAL の問題点
TCB (Trusted Computing Base)が大きい 型チェッカ自体が複雑で大きい 型チェッカにバグがあるかもしれない 現実には存在しない「マクロ命令」がある malloc 命令など 最適化の障害になる

3 この論文の提案する解決策 “TCBを小さくするには?”
FPCCを使え (終) FPCC = Foundational Proof-carrying code TCBをできるだけ小さくした PCC 約2700行 (参考) TALx86 : 約30000行 Linux カーネル : 約 行

4 この論文の提案する解決策 “マクロ命令をなくすには?”
より低レベルな命令に分解する 安全性を検証できるように より洗練された型システムを構築する LTAL: Low-level TAL

5 従来のTALのメモリ確保の例 alloc: malloc $8, %EAX mov $1, (%EAX) mov $2, 4(%EAX)
TALx86 ソースコード 実際の機械語命令列 alloc: malloc $8, %EAX mov $1, (%EAX) mov $2, 4(%EAX) alloc: push $8 call malloc_func test %EAX, %EAX jz err_handler mov $1, (%EAX) mov $2, 4(%EAX)

6 従来のTALのメモリ確保が 最適化の妨げになる例
TALx86 ソースコード 連続してメモリを確保する場合 alloc: malloc $8, %ECX mov $1, (%ECX) mov $2, 4(%ECX) malloc $4, %EAX mov %ECX, (%EAX) この3ヶ所でいちいち 関数呼び出し + 返値チェックをしなければならない この2ヶ所でいちいち 関数呼び出し + 返値チェックをしなければならない

7 こんな風に最適化したい alloc: sub %EBX, %ECX sub $12, %ECX jb err_handler
のぞましいコード Linear allocation 右コードにおいて %EBX = allocポインタ %ECX = limitポインタ(のコピー) 頻繁にメモリを確保する場合に有効 MLなど 関数呼び出しなし エラーチェックは まとめて一回 alloc: sub %EBX, %ECX sub $12, %ECX jb err_handler mov $1, (%EBX) mov $2, 4(%EBX) mov %EBX, 8(%EBX) lea 8(%EBX), %EAX add $12, %EBX

8 こんな風に最適化したい alloc: sub %EBX, %ECX sub $12, %ECX jb err_handler %EBX
のぞましいコード 空きメモリが 十分あるかチェック alloc: sub %EBX, %ECX sub $12, %ECX jb err_handler mov $1, (%EBX) mov $2, 4(%EBX) mov %EBX, 8(%EBX) lea 8(%EBX), %EAX add $12, %EBX %EBX %ECX 空きメモリ

9 こんな風に最適化したい alloc: sub %EBX, %ECX sub $12, %ECX jb err_handler %EBX
のぞましいコード メモリを初期化 alloc: sub %EBX, %ECX sub $12, %ECX jb err_handler mov $1, (%EBX) mov $2, 4(%EBX) mov %EBX, 8(%EBX) lea 8(%EBX), %EAX add $12, %EBX %EBX 1 2 空きメモリ

10 こんな風に最適化したい alloc: sub %EBX, %ECX sub $12, %ECX jb err_handler
のぞましいコード allocポインタを 確保した分だけずらす alloc: sub %EBX, %ECX sub $12, %ECX jb err_handler mov $1, (%EBX) mov $2, 4(%EBX) mov %EBX, 8(%EBX) lea 8(%EBX), %EAX add $12, %EBX 1 2 %EBX 空きメモリ

11 こんな風に最適化したい alloc: sub %EBX, %ECX sub $12, %ECX jb err_handler
のぞましいコード Linear allocation 右コードにおいて %EBX = allocポインタ %ECX = limitポインタ(のコピー) 頻繁にメモリを確保する場合に有効 MLなど 関数呼び出しなし エラーチェックは まとめて一回 alloc: sub %EBX, %ECX sub $12, %ECX jb err_handler mov $1, (%EBX) mov $2, 4(%EBX) mov %EBX, 8(%EBX) lea 8(%EBX), %EAX add $12, %EBX

12 LTALではどう書けるか? (注: 実際の論文とは少し変えてある)
実際の機械語命令列 LTALソースコード alloc: testm $12 iffull err_handler store $1, 0 store $2, 4 record %EAX incalloc $8 store %EAX, 0 incalloc $4 alloc: cmp %EBX, %ESI jb err_handler mov $1, (%EBX) mov $2, 4(%EBX) mov %EBX, %EAX add $8, %EBX mov %EAX, (%EBX) add $4, %EBX

13 LTALではどう書けるか? (注: 実際の論文とは少し変えてある)
実際の機械語命令列 LTALソースコード alloc: testm $12 iffull err_handler store $1, 0 store $2, 4 record %EAX incalloc $8 store %EAX, 0 incalloc $4 alloc: cmp %EBX, %ESI jb err_handler mov $1, (%EBX) mov $2, 4(%EBX) mov %EBX, %EAX add $8, %EBX mov %EAX, (%EBX) add $4, %EBX testm命令: 空きメモリが 十分あるかチェック

14 LTALではどう書けるか? (注: 実際の論文とは少し変えてある)
実際の機械語命令列 LTALソースコード alloc: testm $12 iffull err_handler store $1, 0 store $2, 4 record %EAX incalloc $8 store %EAX, 0 incalloc $4 alloc: cmp %EBX, %ESI jb err_handler mov $1, (%EBX) mov $2, 4(%EBX) mov %EBX, %EAX add $8, %EBX mov %EAX, (%EBX) add $4, %EBX %EBX = allocポインタ %ESI = limitポインタ – 4096 確保するメモリのサイズが4096B以下ならば (%ESI – %EBX) が 0 以上であればOK

15 LTALではどう書けるか? (注: 実際の論文とは少し変えてある)
実際の機械語命令列 LTALソースコード alloc: testm $12 iffull err_handler store $1, 0 store $2, 4 record %EAX incalloc $8 store %EAX, 0 incalloc $4 alloc: cmp %EBX, %ESI jb err_handler mov $1, (%EBX) mov $2, 4(%EBX) mov %EBX, %EAX add $8, %EBX mov %EAX, (%EBX) add $4, %EBX iffull命令: 後続の命令で十分なメモリがあることを仮定できる

16 LTALではどう書けるか? (注: 実際の論文とは少し変えてある)
実際の機械語命令列 LTALソースコード alloc: testm $12 iffull err_handler store $1, 0 store $2, 4 record %EAX incalloc $8 store %EAX, 0 incalloc $4 alloc: cmp %EBX, %ESI jb err_handler mov $1, (%EBX) mov $2, 4(%EBX) mov %EBX, %EAX add $8, %EBX mov %EAX, (%EBX) add $4, %EBX store命令: allocポインタ(+オフセット) の指すメモリを初期化

17 LTALではどう書けるか? (注: 実際の論文とは少し変えてある)
実際の機械語命令列 LTALソースコード record命令: allocポインタを レジスタに保存 alloc: testm $12 iffull err_handler store $1, 0 store $2, 4 record %EAX incalloc $8 store %EAX, 0 incalloc $4 alloc: cmp %EBX, %ESI jb err_handler mov $1, (%EBX) mov $2, 4(%EBX) mov %EBX, %EAX add $8, %EBX mov %EAX, (%EBX) add $4, %EBX

18 LTALではどう書けるか? (注: 実際の論文とは少し変えてある)
実際の機械語命令列 LTALソースコード incalloc命令: allocポインタをずらす alloc: testm $12 iffull err_handler store $1, 0 store $2, 4 record %EAX incalloc $8 store %EAX, 0 incalloc $4 alloc: cmp %EBX, %ESI jb err_handler mov $1, (%EBX) mov $2, 4(%EBX) mov %EBX, %EAX add $8, %EBX mov %EAX, (%EBX) add $4, %EBX

19 LTALではどう書けるか? (注: 実際の論文とは少し変えてある)
実際の機械語命令列 LTALソースコード alloc: testm $12 iffull err_handler store $1, 0 store $2, 4 record %EAX incalloc $8 store %EAX, 0 incalloc $4 alloc: cmp %EBX, %ESI jb err_handler mov $1, (%EBX) mov $2, 4(%EBX) mov %EBX, %EAX add $8, %EBX mov %EAX, (%EBX) add $4, %EBX

20 LTALの型システム と、いっても論文には文法と型システムのほんの一部しか載ってない
ここでは linear allocation に関する部分に絞って紹介する

21 型判定1(値の型判定) Δ;Γ v : τ 型変数リストΔ、型環境Γにおいて値vの型はτである

22 型判定2(命令の型判定) (Δ;Γ; H; cc) {ι} (Δ’;Γ’; H’; cc’)

23 型判定3(命令列の型判定) Δ;Γ; H; cc L
型変数リストΔ、型環境Γ、ヒープ状態H、コンディションコード cc においてラベルLがあらわす命令列を実行できる (ラベルLにジャンプできる)

24 ヒープ状態 H H = ( n, m, t ) n = 存在が確認されている空きメモリのサイズ m = 初期化済みメモリのオフセットの最大値

25 ヒープ状態の例 H = ( 24, 12, (field 0 int) ∩(field 4 int) ∩(field 12 int))
Allocation ポインタ 空きメモリ H = ( 24, 12, (field 0 int) ∩(field 4 int) ∩(field 12 int)) 1 4 4 8 12 8 16 存在が確認されているが 未初期化なメモリ 20 初期化済みのメモリ

26 型付け規則の一部: testm (注: 規則に直接関係ないところは省略してある)
0 ≦ n ≦ 4096 (cc) { testm n } (cc_testm(n))

27 型付け規則の一部: iffull (注: 規則に直接関係ないところは省略してある)
cc = cc_testm(n) (H, cc) L (H; cc) { iffull L } ((n, -1, boxed); cc) 本当にこれでOK?

28 型付け規則の一部: store (注: 規則に直接関係ないところは省略してある)
0 ≦ i ＜ n v1 : t1 m’ = max (m, i) v2 : int= i t’ = t ∩ (field i ti) ((n, m, t)) { store v1, v2 } ((n, m’, t’))

29 型付け規則の一部: record (注: 規則に直接関係ないところは省略してある)
(Γ; (n, m, t)) { record v } ((Γ,v : t) ; (n, m, t))

30 型付け規則の一部: incalloc (注: 規則に直接関係ないところは省略してある)
cc’ = cc_none (if cc = cc_testm(k)) cc (else) { v : int= n’ m ≦ n’ ＜ n ((n, m, t); cc) { incalloc v } ((n – n’, –1, boxed), cc’)

31 その他にこの論文で やられていること User-defined variant 型をマクロ命令を使わずに扱う
MLRISCという型情報を保存しないコンパイラバックエンドと組み合わせた

32 参考文献 Juan Chen, Dinghao Wu, Andrew W. Appel, and Hai Fang. “A Provably Sound TAL for Back-end Optimization” In proc. of PLDI 2003.