ATTAPL Seminar 10/25 Types for Low-Level Languages (2) 米澤研究室 D1　吉野 寿宏 <tossy-2@yl.is.s.u-tokyo.ac.jp>

前回(4.1～4.2)のおさらい RISC-like な低級言語 TAL-0 を設計 言語と型システムの定義 mov, add, jump, brz の命令 Control-Flow Safety を満たすことを証明 Progress, Preservation の手法による

今回の概要 TAL-1: Simple Memory Safety (4.3～4.5) その他の言語機構への拡張 (4.6, 4.7) Object、Closure Existential Type Arrays、Arithmetics Dependent Type の応用

TAL-1: Simple Memory Safety

TAL-1 データに関するプリミティブサポートを追加 メモリ安全性を保証する型システムを設計 オブジェクトの参照(ポインタ)によるアクセス ヒープ、スタック エリアスとの闘い メモリ安全性を保証する型システムを設計 確保済みのメモリ以外にはアクセスしないこと

型理論的な観点からすると… データを扱う場合、型の strong update が必要 低級言語では、データの初期化を組み合わせで表現しなければならない 高級言語では、まとめて初期化するプリミティブを用意できる レジスタについては TAL-0 で導入済 たとえば以下のようなコードは排除したい 5 行目で r4 == 0 なので control-flow safe でない {r1: ptr(code(...))} r3 := 0; Mem[r1] := r3; r4 := Mem[r1]; jump r4

型理論的な観点からすると… しかしエリアシングの問題がある メモリは 2 箇所以上から同じ場所を参照可能 たとえば次のコードで r1 == r2 だったら？ 先ほどのスライドと同じ現象になる しかし r1 と r2 が同じ場所を指していないなら全く問題はない {r1: ptr(code(...)), r2:...} r3 := 0; Mem[r1] := r3; r4 := Mem[r2]; jump r4

エリアスとどう付き合うか 完全なロジックは存在しないが、いくつか静的 解析の理論はある Alias types [Smith et al. 2000; Walker et al. 2001; DeLine et al. 2001] 型システムによりリファレンスを追跡 TAL-1 では、ポインタを 2 種類に分類する アプローチをとる Shared pointer: エリアスするかもしれないポインタ 型は上書きできない Unique pointer: エリアスのないポインタ strong update できるが、ポインタのコピーはできない

TAL-1 Syntax レジスタ オペランド ヒープに割り当てられるオブジェクト sp (スタックポインタ)レジスタ追加 　 : コードまたは shared data へのポインタ uptr(h) : unique data ポインタ ヒープに割り当てられるオブジェクト タプル　　　　　　　 追加

TAL-1 Syntax 命令セット (追加分) rd := Mem[rs + n] ロード Mem[rd + n] := rs ストア rd := malloc n n ワードを確保 割り当てられたポインタは unique pointer になる commit rd shared pointer 化 Unique pointer を shared pointer に coerce salloc n スタックで n ワード確保 sfree n スタックを n ワード解放

TAL-1 Semantics MOV-1 ルール MALLOC ルール COMMIT ルール RHS が unique pointer でない場合のみ代入を許す MALLOC ルール 　　　　　　　　　　　 をレジスタに返す この段階ではまだヒープ(H)は書き換えない COMMIT ルール uptr の中身を取り出して H に追加、ラベル　 を 割り当てる uptr はスタックにも使われているので、sp レジスタはとれない

TAL-1 Semantics LD-S・LD-U / ST-S・ST-U ルール SALLOC/SFREE ルール ほぼ直感的といえるでしょう Shared/unique の違いは、ヒープ(H)から取るか uptr から取り出すかの違い SALLOC/SFREE ルール スタックを前のほうに n ワード伸ばす/前から n ワード切り捨てる スタック内のオブジェクトへの参照は sp レジスタを 介してのみ可能にするため、uptr を使う

例: malloc を使う malloc の例: tuple の deep copy H copy: {r1:ptr(int, int), r2, r3:int} r2 := malloc 2; r3 := Mem[r1]; Mem[r2] := r3; r3 := Mem[r1 + 1]; Mem[r2 + 1] := r3; commit r2; {r1: ptr(int,int), r2: ptr(int,int), r3: int} H r1 1 2 r2 ??? r3 int 1 2 1 ??? 2

Exercise 4.3 4.3.1 4.3.2 push v ≡ salloc 1; Mem[sp] := v pop rd ≡ rd := Mem[sp]; sfree 1 最適化としては、salloc/sfree をまとめて発行 4.3.2 Semantics の書き換えは straightforward Unique pointer が share されていないことは、命令列の長さに関する帰納法で証明可能

TAL-1 Type System ポインタ型を追加 ヒープ内のデータの型 σ ptr(σ) : shared pointer type uptr(σ) : unique pointer type ヒープ内のデータの型 σ ε : 空 τ : value σ1,σ2 : 連結 連結は、結合則を満たし ε を単位元とするモノイドになる ⇒ () のつけ・はずしによって変わらない ρ : allocated type の型変数

TAL-1 Type System Typing Rules ヒープ上のデータのルールについては 直観的なので省略 命令列 S-MOV-1 ルール RHS が uptr 型でないことのチェック追加 S-MALLOC ルール n ≧ 0 チェック n 個の int からなる tuple を作成 Semantics での <m1, …, mn> と対応がついている

TAL-1 Type System Typing Rules 命令列 (cont’d) S-COMMIT ルール COMMIT ルールと同様のチェック(sp でないこと) S-LDS, S-LDU ルール RHS の型が ptr か uptr かの違い S-STS, S-STU ルール S-LDS, S-LDU とほぼ同じ ただし MOV と同様に、RHS が uptr でないことを確認する必要がある

TAL-1 Type System Typing Rules 命令列 (cont’d) S-SALLOC ルール スタックの伸張を連結で記述 この型システムではスタックオーバーフローは検出できない 意味論の SALLOC ルールではオーバーフロー防止があった S-SFREE ルール 先頭 n 要素を削る オーバーフローとは逆に、アンダーフローは検出 できる uptr の中身が空になると S-SFREE のルールは失敗

TAL-1 Type System “Allocated Type Variables”? メモリのチャンクを変数として扱う α, β, … といった型変数はワードサイズの値を表現 Allocated type variables は任意の長さのデータを表現 Allocated type variables は型検査ルールでは消去できない データ長がわからないので

Exercise 4.4.1 Soundness of TAL-1 Type System Proof Sketch Canonical Values, Canonical Operands に ついて追加された部分を証明 タプルについては長さに関する帰納法で証明 code(Γ), ptr(σ) は　　に対応 uptr(σ) はヒープにないタプルに対応 その後 TAL-0 と同様の議論を繰り返す Well-typed になるための条件から、意味論の事前条件が導出できればよい

Exercise 4.4.1 Soundness of TAL-1 Type System rd := v; I の場合 型付け規則の逆と Canonical Values より v = n または　 (≠ uptr(h))である したがって MOV-1 の前提条件が満たされる commit rd; I の場合 (rd) = <...> かつ rd ≠ sp である したがって COMMIT の事前条件が満たされる rd := Mem[rs + n]; I の場合 …

Compiling to TAL-1 TAL-1 はコンパイラターゲットとして十分な表現力を 持っている 整数、タプル、レコード、関数ポインタ (closure はまだない) prod: ∀a,b,c,s. {...} r2 := Mem[sp]; r3 := Mem[sp + 1]; r1 := 0; jump loop loop: ∀s. {r1,r2,r3: int, sp:uptr(...), ...} if r2 jump done; r1 := r1 + r3; r2 := r2 + (-1); done: ∀s. {r1,r2,r3: int, sp:uptr(...), ...} sfree 2; jump r4 int prod(int x, int y) { int a = 0; while(x != 0) { a = a + y; x = x – 1; } return a;

Compiling to TAL-1 コーリングシーケンスは以下の通りとする prod の例でわかるとおり、コードは直観的 引数はスタックに積んで渡され、callee が 解放する 戻り先アドレスは r4 に格納されている 関数の返値は r1 に格納される prod の例でわかるとおり、コードは直観的

Compiling to TAL-1 Type Translation 重要なのは、型がどのように変換されるか 例: prod の型は？ ⇒∀a, b, c, s. code{ r1:a, r2:b, r3:c, sp:uptr(int, int, s), r4: ∀d, e, f. code{ r1:int, r2:d, r3:e, r4:f, sp:uptr(s) } } なんでもいい 引数 返値

Compiling to TAL-1 Type Translation prod: ∀a, b, c, s. code{ r1:a, r2:b, r3:c, sp:uptr(int, int, s), r4: ∀d, e, f. code{ r1:int, r2:d, r3:e, r4:f, sp:uptr(s) } 引数なので prod が解放 r1 sp 結果: int ? 7: int 4: int s として抽象化 r2 ? ? r3 ? ? : r4 コード

Compiling to TAL-1 再帰呼び出しの型付け 関数呼び出しの手順 r4、引数をスタックに積み、r4 に戻り先を代入して関数本体に jump 関数から戻ってきたら r4 を書き戻してスタックを 1 要素解放 しかしこの呼び出し規約は本質的ではない 例えば戻り先もスタックに積むという方法もとれる (Exercise 4.5.1)

Exercise 4.5.1 型はひとまず省略 cont: salloc 1; Mem[sp] := r1; fact: r1 := Mem[sp]; if r1 jump retn; r2 := r1 + (-1); salloc 2 Mem[sp + 1] := cont; Mem[sp] := r2; jump fact cont: salloc 1; Mem[sp] := r1; jump prod // tail call retn: r1 := 1; r4 := Mem[sp + 1]; sfree 2; jump r4

Exercise 4.5.1 fact の型 cont, retn の型 ∀a,b,c,d,s. code{ r1:a, r2:b, r3:c, r4:d, sp:uptr(int,∀e,f,g. code{ r1:int, r2:e, r3:f, r4:g, sp:uptr(s) }, s) } cont, retn の型 ∀b,c,d,s’. code{ r1:int, r2:b, r3:c, r4:d, sp:uptr(int, ∀e,f,g. code{ r1:int, r2:e, r3:f, r4:g, sp:uptr(s’) }, s’) } 同じ形になります

Scaling to Other Language Features

Objects and Closures Existential Type を導入 ∃α.τ … オペランドの抽象化 S-PACK, S-UNPACK ルール ∃ρ.τ … allocated type の抽象化 Operand の existential と同様のルール α はワードなのに対し、ρ は任意の長さの タプルを抽象化する、という違い

Objects and Closures Existential の導入 S-PACK ルール: 型の中の共通している部分を抽象化する ptr(code{r1:int, r2:int, ...}, int) ⇒ ∃α.ptr(code{r1:α, r2:int, ...}, α) S-UNPACK ルール: αが context に存在する とき ∃ を eliminate する しかし α は abstract として残される Context 中の他の型と distinct として扱う

Objects and Closures オブジェクトの実装 interface Point { int getX(); int getY(); } Class C1 implements Point { int x = 0, y = 0; int getX() { return x; } int getY() { return y; } } Class C2 implements Point { int x = 0, y = 0, n = 0; int getX() { n++; return x; } int getY() { n++; return y; } } ptr(int,int) → int ptr(int,int,int) → int

Objects and Closures オブジェクトの実装 getX の型は…？ C1 から ptr(int,int) → int C2 から ptr(int,int,int) → int ⇒ 左辺を抽象化して∃α. α→int getY についても同様 したがって Point インターフェイスの型は ∃α.ptr(ptr(α→int, α→int), α) いわゆる vtable データフィールド

Objects and Closures Discussion ML 等の高級言語からコンパイルするときに 必要 もっと実用的に表現するには、再帰型を 導入すればよい[Bruce 1995; 2002] ∃ρ.μα.ptr(ptr(α→int, α→int), ρ) そのほかにもいくつもの表現手段がある

Objects and Closures Discussion 再利用可能な型構築子の集合を見つけることが重要 F-bounded existential など それによって、多くのオブジェクトモデルを表現できるようになる CLI, JVML はオブジェクトモデルを固定しており、対象とする以外の言語へのサポートは貧困 しかしダウンキャストは問題になる 動的に型検査を行う必要がある 表現型を応用できる[Crary et al. 1998]が、重い上に 実用的なオブジェクトの表現をサポートしない

配列 TAL-1 では固定長のデータしかとれない 配列をサポートするには？ CISC 風のアプローチ Dependent Type を用いるアプローチ [Xi, Harper 2001] 実際に TALx86 に実装されている

配列 CISC 風アプローチ CISC 風のアプローチ ≡ プリミティブを増やす rd := newarray(ri, rs) rd := ldarr(rs, ri) / starr(rs, rd, ri) 範囲外アクセスをしないようにすることが重要 サイズを最初の要素に持たせたタプルを配列として扱う等 範囲外をアクセスしようとしたら例外ハンドラに飛ばす

配列 CISC 風アプローチ 利点 欠点 型システムの設計が単純 配列のアクセス範囲内チェックを動的にやる必要がある サイズが静的に定まる場合でも必ず実行時にサイズを管理しなければならない コード最適化との相性が悪い

配列 Dependent Type によるアプローチ Compile time expression の導入 整数値、算術式(加減算・乗算)、変数から成る 型がこれらの式を含むことを許す arr(τ, 30+12) ≡ arr(τ, 42) 42 要素からなるτ型の配列 int(36) 「36」という値を表す型 (singleton integer) ∃i. int(i * 2) 偶数 ∀i1,i2. code{r1:int(i1), r2:arr(T,i1), r3:int(i2)} r2 は T 型の配列、r1 はその要素数を格納 r3 はまた別の整数

配列 Dependent Type によるアプローチ 算術式から変数の間の大小関係を静的に求めれば配列の境界チェックを消せる 教科書のコードにはミスあり (3行目 RHS) コンテクストに変数の制約を追加して計算 if 文で分岐しない場合の条件を求める sub: … if r3 < 0 jump L; rt := r3 - r1; if rt >= 0 jump L; rd := ldarr(r2, r3) 範囲チェック済み なので ldarr での 検査は必要ない

配列 Dependent Type によるアプローチ どういった制約がかけるか？ DTAL では型付けを decidable にするために制約は linear なものに限られている 配列くらいならばこれでなんとかなる 実際にはコード生成側が proof をつければ 任意の制約を扱える Proof-Carrying Code Framework を作れる 型システムの設計者側で、sound な inference rule のみ受け付けるようにする必要は残る

Exercise 4.6.1 意味論 例外ルール

Exercise 4.6.1 型システム τに arr(τ) を追加 型付け規則 境界チェックは例外生成

Some Real World Issues メモリ領域に対して読み込み・書き込みのアクセス制限をかける Subtyping の追加 領域の型に対してフラグをつけることで可能 Subtyping の追加 σの連結に関する subtyping rw-access <: ro-access, wo-access ...

Some Real World Issues スタックの型を拡張する free 命令の追加 Capability types 中を指すポインタを作れるようにする Nested procedure にも対応できる STAL [Morrisett et al. 2002] Intersection type の応用 TALT [Crary, 2003] free 命令の追加 ヒープオブジェクトの解放 Capability types Region のサポートを追加することができる [Walker et al. 2000]

Some Real World Issues これらの拡張は型システムの肥大化を招く 健全性の証明を手でやるのは非常に大変 定理証明系の応用 TALT [Crary 2003] Coq を利用した例 [Hamid et al. 2002] もうひとつのアプローチとして「Foundational ×××」の世界がある[Appel, Felty 2000] 高階論理を用いて型をつくる

4 章まとめ

まとめ 低級言語のための型システムは面白い 型情報を生成・処理するのが機械のため、 人的要因をある程度排除できる 高級言語の設計においてはこのあたりが心配 もちろん型システム自体の健全性は(定理証明系などによって)証明しておくべき メモリ操作のための型システムなどは高級 言語では必要ない