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

Slides:



Advertisements
Similar presentations
Region-based Memory Management in Cyclone について 発表者 : 前田俊行.
Advertisements

オブジェクト指向 言語 論 知能情報学部 新田直也. 講義概要  私の研究室: 13 号館 2 階 (13-206)  講義資料について :  参考図書 : 河西朝雄 : 「原理がわかる プログラムの法則」,
2006/10/26 山下 諒蔵 佐藤 春旗 前田 俊行 大山 恵弘 佐藤 秀明 住井 英二郎
プログラミング演習II 2004年11月 30日(第6回) 理学部数学科・木村巌.
2006/11/9 山下 諒蔵 佐藤 春旗 前田 俊行 大山 恵弘 佐藤 秀明 住井 英二郎
ML 演習 第 8 回 2007/07/17 飯塚 大輔, 後藤 哲志, 前田 俊行
情報基礎演習B 後半第5回 担当 岩村 TA 谷本君.
2006/11/30 山下 諒蔵 佐藤 春旗 前田 俊行 大山 恵弘 佐藤 秀明 住井 英二郎
実行時のメモリ構造(1) Jasminの基礎とフレーム内動作
LMNtalからC言語への変換の設計と実装
オブジェクト指向言語論 知能情報学部 新田直也.
2006/10/12 山下 諒蔵 佐藤 春旗 前田俊行 大山 恵弘 佐藤 秀明 住井 英二郎
LMNtalからC言語への変換の設計と実装
ソフトウェアを美味しく 解析する方法 Security Ark
侵入検知システム(IDS) 停止 IDS サーバへの不正アクセスが増加している
プログラミング言語論 理工学部 情報システム工学科 新田直也.
プログラミング言語論 理工学部 情報システム工学科 新田直也.
2006/10/19 山下 諒蔵 佐藤 春旗 前田 俊行 大山 恵弘 佐藤 秀明 住井英二郎
F11: Analysis III (このセッションは論文2本です)
コンパイラ演習 第 4 回 (2011/10/27) 中村 晃一 野瀬 貴史 前田 俊行 秋山 茂樹 池尻 拓朗 鈴木 友博 渡邊 裕貴
  【事例演習6】  数式インタプリタ      解 説     “インタプリタの基本的な仕組み”.
オブジェクト指向 プログラミング 第一回 知能情報学部 新田直也.
データ構造と アルゴリズム 第八回 知能情報学部 新田直也.
プログラミング演習Ⅰ 課題2 10進数と2進数 2回目.
2007/1/11 山下 諒蔵 佐藤 春旗 前田 俊行 大山 恵弘 佐藤 秀明 住井 英二郎
POPLミーティング 5/11 型付きアセンブリ言語の 一般化実装に関する展望
TAL : Typed Assembly Language について
修論進捗状況報告 型付きアセンブリ言語のマルチアーキテクチャ化実装に向けて
型付きアセンブリ言語を用いた安全なカーネル拡張
卒業論文に向けて(5) 学部4年生 島本 大輔 2004年12月14日.
コンパイラの解析 (3) クラスとインスタンスの初期化.
セキュリティ(3) 05A2013 大川内 斉.
プログラミング 4 記憶の割り付け.
プログラミング言語入門.
2005年度 データ構造とアルゴリズム 第3回 「C言語の復習:再帰的データ構造」
コンパイラ 2012年11月15日
第7回 プログラミングⅡ 第7回
順序付き線形型に基づく 木構造処理プログラムから ストリーム処理プログラムへの変換
依存型で型付けされた 副作用のある関数のための 型保存コンパイラ
コンパイラ資料 実行時環境.
データ構造と アルゴリズム 第五回 知能情報学部 新田直也.
ASIAN 2003 報告 前田俊行.
C言語を用いたマシン非依存な JITコンパイラ作成フレームワーク
Development of Certified Program Translators to Verify Low-Level Language Programs Toshihiro YOSHINO (Yonezawa Lab, Univ. of Tokyo)
オブジェクト指向プログラミングと開発環境
情報とコンピュータ 静岡大学工学部 安藤和敏
コンピュータアーキテクチャ 第 2 回.
2004 Fall. Term Report Immune Project
プログラムが実行されるまで 2002年4月14日 海谷 治彦.
実装について 前田俊行.
ポインタとポインタを用いた関数定義.
コンピュータアーキテクチャ 第 2 回.
Mondriaan Memory Protection の調査
コンピュータアーキテクチャ 第 4 回.
発表者: 稲葉 一浩 複雑ネットワーク・地図グラフ セミナー 2017/1/19
卒業論文に向けて(3) 学部4年生 島本 大輔 2004年11月11日.
SMP/マルチコアに対応した 型付きアセンブリ言語
コンパイラ 第12回 実行時環境 ― 変数と関数 ― 38号館4階N-411 内線5459
全体ミーティング(6/3) 修士2年 飯塚 大輔.
オブジェクト指向言語論 第一回 知能情報学部 新田直也.
関数と再帰 教科書13章 電子1(木曜クラス) 2005/06/22(Thu.).
プログラミング演習II 2004年11月 16日(第5回) 理学部数学科・木村巌.
POPL ミーティング 6/7 Inside ADL
プログラミング演習II 2003年12月10日(第7回) 木村巌.
TList リスト構造とは? 複数のデータを扱うために、 データの内容と、次のデータへのポインタを持つ構造体を使う。
6.3 インタプリタ (1)インタプリタ(interpreter)とは
岩村雅一 知能情報工学演習I 第13回(後半第7回) 岩村雅一
プログラミング演習II 2003年10月29日(第2,3回) 木村巌.
6.5 最終コード生成 (1)コードの形式 ①絶対2進コード(AB : absolute binary) 命令後のオペランドが絶対番地指定。
Safety Checking of Machine Code
Presentation transcript:

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のメモリ確保の例 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)

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

こんな風に最適化したい 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

こんな風に最適化したい 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 空きメモリ

こんな風に最適化したい 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 空きメモリ

こんな風に最適化したい 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 空きメモリ

こんな風に最適化したい 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

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

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命令: 空きメモリが 十分あるかチェック

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

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命令: 後続の命令で十分なメモリがあることを仮定できる

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ポインタ(+オフセット) の指すメモリを初期化

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

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

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

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

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

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

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

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

ヒープ状態の例 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 初期化済みのメモリ

型付け規則の一部: 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 v1 : t1 m’ = max (m, i) 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.