Document

A Provably Sound TAL
for Back-end Optimization
について
前田俊行
この論文が主張するところの
既存の TAL の問題点
• TCB (Trusted Computing Base)が大きい
– 型チェッカ自体が複雑で大きい
– 型チェッカにバグがあるかもしれない
• 現実には存在しない「マクロ命令」がある
– malloc 命令など
– 最適化の障害になる
この論文の提案する解決策
“TCBを小さくするには?”
• FPCCを使え (終)
– FPCC = Foundational Proof-carrying code
• TCBをできるだけ小さくした PCC
– 約2700行
• (参考)
– TALx86 :
約30000行
– Linux カーネル : 約5670000行
この論文の提案する解決策
“マクロ命令をなくすには?”
• より低レベルな命令に分解する
– 安全性を検証できるように
より洗練された型システムを構築する
• LTAL: Low-level TAL
従来のTALのメモリ確保の例
TALx86 ソースコード
alloc:
malloc $8, %EAX
mov
$1, (%EAX)
mov
$2,
4(%EAX)
実際の機械語命令列
alloc:
push
call
test
jz
mov
mov
$8
malloc_func
%EAX, %EAX
err_handler
$1, (%EAX)
$2, 4(%EAX)
従来のTALのメモリ確保が
最適化の妨げになる例
•連続してメモリを確保する場合 TALx86 ソースコード
この2ヶ所でいちいち
この3ヶ所でいちいち
関数呼び出し + 返値チェック
をしなければならない
alloc:
malloc $8,
mov
$1,
mov
$2,
malloc $4,
mov %ECX,
%ECX
(%ECX)
4(%ECX)
%EAX
(%EAX)
こんな風に最適化したい
• 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
こんな風に最適化したい
空きメモリが
十分あるかチェック
%EBX
%ECX
空きメモリ
のぞましいコード
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
空きメモリ
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
こんな風に最適化したい
のぞましいコード
allocポインタを
確保した分だけずらす alloc:
1
2
%EBX
空きメモリ
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
こんな風に最適化したい
• 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
LTALではどう書けるか?
(注: 実際の論文とは少し変えてある)
LTALソースコード
実際の機械語命令列
alloc:
testm
$12
iffull err_handler
store
$1, 0
store
$2, 4
record
%EAX
incalloc $8
store
%EAX, 0
record
%EAX
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)
mov %EBX, %EAX
add
$4, %EBX
LTALではどう書けるか?
(注: 実際の論文とは少し変えてある)
LTALソースコード
実際の機械語命令列
alloc:
alloc:
cmp %EBX, %ESI
testm
$12
jb
err_handler
iffull err_handler
mov
$1, (%EBX)
store
$1, 0
mov
$2, 4(%EBX)
store
$2,
4
testm命令:
record
%EAX
空きメモリが mov %EBX, %EAX
add
$8, %EBX
incalloc $8 十分あるかチェック
mov %EAX, (%EBX)
store
%EAX, 0
mov %EBX, %EAX
record
%EAX
add
$4, %EBX
incalloc $4
LTALではどう書けるか?
(注: 実際の論文とは少し変えてある)
LTALソースコード
実際の機械語命令列
alloc:
alloc:
cmp %EBX, %ESI
testm
$12
jb
err_handler
iffull err_handler
mov
$1, (%EBX)
store
$1, 0
mov
$2, 4(%EBX)
store
$2, 4
= allocポインタ mov %EBX, %EAX
record %EBX
%EAX
– 4096
$8, %EBX
incalloc%ESI
$8= limitポインタadd
確保するメモリのサイズが4096B以下ならば
mov %EAX, (%EBX)
store
%EAX, 0
– %EBX) が 0mov
以上であればOK
%EBX, %EAX
record (%ESI
%EAX
add
$4, %EBX
incalloc $4
LTALではどう書けるか?
(注: 実際の論文とは少し変えてある)
LTALソースコード
実際の機械語命令列
alloc:
alloc:
cmp %EBX, %ESI
testm
$12
jb
err_handler
iffull err_handler
mov
$1, (%EBX)
store
$1, 0
mov命令: $2, 4(%EBX)
store
$2, 4
iffull
mov %EBX, %EAX
record
%EAX
後続の命令で十分なメモリが
add
$8, %EBX
incalloc $8
あることを仮定できる
mov %EAX, (%EBX)
store
%EAX, 0
mov %EBX, %EAX
record
%EAX
add
$4, %EBX
incalloc $4
LTALではどう書けるか?
(注: 実際の論文とは少し変えてある)
LTALソースコード
実際の機械語命令列
alloc:
alloc:
cmp %EBX, %ESI
testm
$12
jb
err_handler
iffull err_handler
mov
$1, (%EBX)
store
$1, 0
mov
$2, 4(%EBX)
store
$2, 4
mov %EBX, %EAX
record
%EAX
store命令:
add
$8, %EBX
incalloc $8
mov %EAX, (%EBX)
store
%EAX, allocポインタ(+オフセット)
0
mov %EBX, %EAX
record
%EAX の指すメモリを初期化
add
$4, %EBX
incalloc $4
LTALではどう書けるか?
(注: 実際の論文とは少し変えてある)
LTALソースコード
実際の機械語命令列
record命令:
alloc:
allocポインタを
cmp %EBX, %ESI
レジスタに保存
alloc:
testm
$12
iffull err_handler
store
$1, 0
store
$2, 4
record
%EAX
incalloc $8
store
%EAX, 0
record
%EAX
incalloc $4
jb
mov
mov
mov
add
mov
mov
add
err_handler
$1, (%EBX)
$2, 4(%EBX)
%EBX, %EAX
$8, %EBX
%EAX, (%EBX)
%EBX, %EAX
$4, %EBX
LTALではどう書けるか?
(注: 実際の論文とは少し変えてある)
LTALソースコード
実際の機械語命令列
incalloc
命令:
alloc:
alloc:
allocポインタをずらす
cmp %EBX, %ESI
testm
$12
jb
err_handler
iffull err_handler
mov
$1, (%EBX)
store
$1, 0
mov
$2, 4(%EBX)
store
$2, 4
mov %EBX, %EAX
record
%EAX
add
$8, %EBX
incalloc $8
mov %EAX, (%EBX)
store
%EAX, 0
mov %EBX, %EAX
record
%EAX
add
$4, %EBX
incalloc $4
LTALではどう書けるか?
(注: 実際の論文とは少し変えてある)
LTALソースコード
実際の機械語命令列
alloc:
testm
$12
iffull err_handler
store
$1, 0
store
$2, 4
record
%EAX
incalloc $8
store
%EAX, 0
record
%EAX
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)
mov %EBX, %EAX
add
$4, %EBX
LTALの型システム
• と、いっても論文には文法と型システムの
ほんの一部しか載ってない
• ここでは linear allocation に関する部分に
絞って紹介する
型判定1(値の型判定)
Δ;Γ
v:τ
• 型変数リストΔ、型環境Γにおいて値vの型
はτである
型判定2(命令の型判定)
(Δ;Γ; H; cc) {ι} (Δ’;Γ’; H’; cc’)
• 型変数リストΔ、型環境Γ、ヒープ状態H、コンディ
ションコード cc において命令ιを実行すると、型
変数リストはΔに、型環境はΓ、ヒープ状態はH’
に、コンディションコードは cc’になる
型判定3(命令列の型判定)
Δ;Γ; H; cc
L
• 型変数リストΔ、型環境Γ、ヒープ状態H、コ
ンディションコード cc においてラベルLが
あらわす命令列を実行できる (ラベルLに
ジャンプできる)
ヒープ状態 H
H = ( n, m, t )
• n = 存在が確認されている空きメモリのサイズ
• m = 初期化済みメモリのオフセットの最大値
• t = 初期化済みメモリの型
ヒープ状態の例
Allocation
ポインタ
空きメモリ
0
4
1
4
8
12
16
20
H = ( 24, 12,
(field 0 int)
∩(field 4 int)
∩(field 12 int))
8
存在が確認されているが
未初期化なメモリ
初期化済みのメモリ
型付け規則の一部: testm
(注: 規則に直接関係ないところは省略してある)
0 ≦ n ≦ 4096
(cc) { testm n } (cc_testm(n))
型付け規則の一部: iffull
(注: 規則に直接関係ないところは省略してある)
cc = cc_testm(n)
(H, cc) L
(H; cc) { iffull L } ((n, -1, boxed); cc)
• 本当にこれでOK?
型付け規則の一部: store
(注: 規則に直接関係ないところは省略してある)
0 ≦ i ＜ n m’ = max (m, i)
v 1 : t1
v2 : int= i
t’ = t ∩ (field i ti)
((n, m, t)) { store v1, v2 } ((n, m’, t’))
型付け規則の一部: record
(注: 規則に直接関係ないところは省略してある)
(Γ; (n, m, t)) { record v }
((Γ,v : t) ; (n, m, t))
型付け規則の一部: 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’)
その他にこの論文で
やられていること
• User-defined variant 型をマクロ命令を使
わずに扱う
• MLRISCという型情報を保存しないコンパ
イラバックエンドと組み合わせた
参考文献
• Juan Chen, Dinghao Wu, Andrew W.
Appel, and Hai Fang. “A Provably
Sound TAL for Back-end Optimization”
In proc. of PLDI 2003.

Download Report