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

Cyclone とは ? 安全な C の方言 – 型による静的安全性チェック – 配列境界検査などの動的安全性チェック それでいてプログラマに低レベルなメ モリ制御をさせたい

Cyclone プログラムの例 ほとんど C と変わらない – 書換率 = 10% 以下 ( 著者らの経験による ) void factorial(int* result, int n) { int x = 1; if (n > 1) { factorial(&x, n – 1); } *result = x * n; }

Cyclone で region ベースメモリ 管理が必要なわけ スタックにデータを置けるようにした い – そしてそのデータへのポインタを使いたい void factorial(int* result, int n) { int x = 1; if (n > 1) { factorial(&x, n – 1); } *result = x * n; } ポインタ操作 スタック上に データを置く

Region ベースメモリ管理と は ? メモリの確保と解放を Region という単位 で行う手法 Region は LIFO に確保、解放される

LIFO な region の確保と解放 Region の確保 = スタックへ push Region の解放 = スタックから pop

Region の種類 : 2 つ 静的 region – 実行時にサイズが変わらない region – 本当のメモリスタック上に確保できる 動的 region – 実行時にサイズが変わるかもしれない region – メモリスタック上には確保できない

Cyclone における Region の種 類 関数 region ( 静的 region) ローカルブロック region ( 静的 region) 動的 region ヒープ region ( 動的 region)

関数 Region ( 静的 region) 関数の引数を保存する region int sys_mlock(int start, int length) { … } 関数 region int start int length Region スタック 関数呼び出し 新たに region を生成

関数 Region ( 静的 region) 関数の引数を保存する region int sys_mlock(int start, int length) { … } Region スタック 関数からのリターン 生成した region を解放

ローカルブロック Region ( 静的 region) ローカル変数を保存する region { int i; struct stat s; … } Region スタック ローカルブロック region int i struct stat s

動的 Region region プリミティブによって確保される region Region スタック 動的 region int i struct stat s region x { int i; struct stat s; … }

動的 Region の特徴 rnew プリミティブで動的にメモリを確保で きる region x { int? array = rnew(x) { for i < n : i }; … } Region スタック 動的 region Int? array Region ハンドル Region ハンドルを指定して 長さ n の配列をメモリに確保 長さ n の配列

ヒープ region ( 動的 region) プログラム実行中ずっと存在する region グローバル変数を保存する region malloc などがメモリを確保する region int global_counter; … void func() { … malloc(); … } int global_counter ヒープ region 新たに確保

Cyclone における メモリ安全性の保証 メモリ安全性を破るプログラムは コンパイル時の型チェックではじく int* function() { int x; return &x; } メモリ安全でないプログラムの例 型チェックではじ く！

Cyclone におけるポインタ型 全てのポインタ型は、そのポインタが 指している region の情報を保持する ( 例 ) int*ρ –region ρ 中の整数値を指す ρ は region を識別する名前

シンプルな型チェックの例 その 1 int*ρ p; ρ { int x = 0; p = &x; } *p = 123; 型エラー p の宣言の時点では まだ ρ はスコープにない

シンプルな型チェックの例 その 2 int*σ p; ρ { int x = 0; p = &x; } *p = 123; 型エラー p と &x の型が違う p : int*σ &x : int*ρ

関数の Region 多相性 関数はアクセスする region が具体的に分 からなくてもよい char?ρ1 strcpy (char?ρ1, const char?ρ2); char?ρH strdup (const char?ρ); char?ρ1 rstrdup (region_t, const char?ρ2); 例 : Cyclone の文字列ライブラリのプロトタイプ宣言 ( 注 ) ρH はヒープ region を表す

関数の Region 多相性の例 文字列複製関数 strdup の定義 char?ρ1 rstrdup (region_t, const char?ρ2); char?ρH strdup (const char?ρ str) { return rstrdup (heap_regions, str); } ( 注 )ρH, heap_regions は ヒープ region を表す

構造体の Region 多相性 構造体はアクセスする region が具体的に 分からなくてもよい struct List { int*ρ1 head; struct List *ρ2 tail; }; 例 : リスト構造体の定義

Subtyping 型は、より短命な region を持つ型にキャストで きる void f (int b, int*ρ1 p1, int*ρ2 p2) ρ3 { int*ρ3 p; if (b) p = p1; else p = p2; … } ρ1 と ρ2 は ρ3 より長生き なのでキャストできる

うっとおしい region 注釈を無 くす 巧みな “ デフォルトルール ” によって プログラマが明示しなければならない 注釈の量を減らす – ルール 1: ローカル変数は、推論する – ルール 2: 関数の引数や返り値の region は全 て新しい region を割り当てる – ルール 3: それ以外は全部ヒープ region にし てしまう

list_t list_copy(list_t lst) { list_t res = NULL; for (list_t t = lst; t != NULL; t = t->tail) res = new List(new *t->hd, res); return res; } list_t list_copy (list_t lst) { list_t res = NULL; for (list_t t = lst; t != NULL; t = t->tail) res = new List(new *t->hd, res); return res; } ルール 2 より引数には 新しい region 名を与える list_t list_copy (list_t lst) { list_t res = NULL; for (list_t t = lst; t != NULL; t = t->tail) res = new List(new *t->hd, res); return res; } ルール 3 により ヒープ region となる list_t list_copy (list_t lst) { list_t res = NULL; for (list_t t = lst; t != NULL; t = t->tail) res = new List(new *t->hd, res); return res; } ルール 1 により推論 list_t list_copy (list_t lst) { list_t res = NULL; for (list_t t = lst; t != NULL; t = t->tail) res = new List(new *t->hd, res); return res; } ルール 1 により推論 list_t list_copy (list_t lst) { list_t res = NULL; for (list_t t = lst; t != NULL; t = t->tail) res = new List(new *t->hd, res); return res; } デフォルトルール適用の例 struct List { int*ρ1 head; struct List *ρ2 tail; }; typedef struct List *ρ2 list_t ;

Existential Existential 型とは、型のある部分を抽象 化することによって複数の型を統一的 に扱うための型である Cyclone はこの existential 型をサポート している

Existential 型の例 struct IntFn ∃ α { int (*func)(α); α env; } Existential 型 struct IntFn_int { int (*func)(int*ρ); int*ρ env; } struct IntFn_List { int (*func)(struct List*ρ); struct List* env; } 型変数 α を実際の型で 置き換えた型の値は全 てこの existential 型に 変換 (pack という ) でき る Pack 可能

Existential の pack の例 struct IntFn ∃ α { int (*func)(α); α env; } int read (int*ρ x) { return *x; } L { int x = 0; struct IntFn pkg = {.func = read,.env = &x }; } Existential の pack 型 int*L を抽象化

Existential の unpack の例 struct IntFn ∃ α { int (*func)(α); α env; } int read (int*ρ x) { return *x; } int apply_IntFn(struct IntFn pkg) { let IntFn {.func = f,.env = x } = pkg; return f ( x ); } Existential の unpack 関数 f の型 : int (*)(α) 引数 x の型 : α

Existential と メモリ安全性上の問題 Existential は型を隠蔽してしまうので dangling ポインタが発生する可能性があ る

Existential による dangling ポインタの発生の例 struct IntFn ∃ α { int (*func)(α); α env; } int read (int*ρ x) { return *x; } L1 { struct IntFn pkg; L2 { int x = 0; pkg = {.func = read,.env = &x }; } … } Dangling ポインタ発生！ だが型エラーにはならない …

解決策第 1 段階 関数の effect を考慮する –Effect = 関数がアクセスする ( かもしれない )region の集 合 生きている region の集合を追跡し、 呼び出そうとしている関数の effect と比較す る –Effect 中の region は全て生きていなければならな い

関数の effect はどう求めるか ? 引数と返り値の型にあらわれる region を 全て effect に含める – 最も conservative な推論 – 利点 : プロトタイプ宣言だけで effect を求 められる

関数の effect の例 普通の関数 int*ρ1 f ( int*ρ2, int*ρ1*ρ3); Effect : {ρ1, ρ2, ρ3} 多相型関数 int compare(α, α); Effect : { regions_of (α) } ただし regions_of は以下のとおり : regions_of (int) = 0 ( 空集合 ) regions_of (τ*ρ) = { ρ } ∪ regions_of (τ) regions_of ((τ1, …, τn) → τ) = regions_of (τ1) ∪ regions_of (τ2) ∪ regions_of (τ)

解決策第 2 段階 Region 制約を考慮する –Region 制約 = どの region がどの region より長生きしなければならな いか Existential の定義に region 制約を指定する –Existential を pack するには指定された region 制約を満 たしていなければならない Existential の unpack 後は指定した region 制約が満 たされているとみなして型チェックを行う

Region 制約を指定した existential の例 struct IntFn ∃ α: regions_of (α) <: ρ { int (*func)(α); α env; } regions_of (α) の全ての region が ρ より長生きであるという制約を表す

Region 制約を満たした existential pack の例 struct IntFn ∃ α : regions_of (α) <: ρ { int (*func)(α); α env; } int read (int*ρ x) { return *x; } L { int x = 0; struct IntFn pkg = {.func = read,.env = &x }; } region 制約 L <: L を満たす

Region 制約を満たさない existential pack の例 struct IntFn ∃ α : regions_of (α) <: ρ { int (*func)(α); α env; } int read (int*ρ x) { return *x; } L1 { struct IntFn pkg; L2 { int x = 0; pkg = {.func = read,.env = &x }; } 型エラー region 制約 L1 <: L2 を満たさない

Existential の unpack の例 L { struct IntFn pkg; … let IntFn {.func = f,.env = x } = pkg; f ( x ); } struct IntFn ∃ α : regions_of (α) <: ρ { int (*func)(α); α env; } 関数 f の effect = { regions_of (α) } 生きている region = { L } Region 制約 = { regions_of (α) <: L } つまり、関数 f は呼んでも安全！

まとめ Cyclone は region-based メモリ管理を用 いた安全な C の方言である – 安全性は型チェックにより保証される – スタックにデータを置くことが可能で、さ らにポインタで指すことも可能 Existential によって生じるメモリ安全性 の問題は関数の effect と region 制約に よって解決されている

References Cyclone homepage Region-based Memory Management in Cyclone, Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. PLDI2002. To appear.