Region-based Memory Management in Cyclone について

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を生成
}
関数region
int start
int length
Regionスタック
関数Region (静的region)
• 関数の引数を保存するregion
int sys_mlock(int start, int length)
{
…
}
生成したregionを解放
関数からのリターン
Regionスタック
ローカルブロックRegion
(静的region)
• ローカル変数を保存するregion
ローカルブロック
region
{
int i;
struct stat s;
int i
struct stat s
…
}
Regionスタック
動的Region
• regionプリミティブによって確保されるregion
region x {
int i;
struct stat s;
動的region
int i
struct stat s
…
}
Regionスタック
動的Regionの特徴
• rnewプリミティブで動的にメモリを確保できる
Region ハンドル
region x {
int? array =
rnew(x) { for i < n : i };
…
}
Region ハンドルを指定して長
さnの配列をメモリに確保
動的region
Int? array
長さnの配列
Regionスタック
ヒープregion (動的region)
• プログラム実行中ずっと存在するregion
• グローバル変数を保存するregion
• malloc などがメモリを確保するregion
int global_counter;
…
void func()
{
…
malloc();
新たに確保
…
}
ヒープregion
int global_counter
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が具体的に分
からなくてもよい
例 : Cycloneの文字列ライブラリのプロトタイプ宣言
char?ρ1 strcpy <ρ1, ρ2> (char?ρ1, const char?ρ2);
char?ρH strdup <ρ> (const char?ρ);
char?ρ1 rstrdup <ρ1, ρ2> (region_t<ρ1>, const char?ρ2);
(注) ρH はヒープregionを表す
関数のRegion多相性の例
• 文字列複製関数strdupの定義
char?ρ1 rstrdup <ρ1, ρ2> (region_t<ρ1>, const char?ρ2);
char?ρH strdup <ρ> (const char?ρ str)
{
return rstrdup <ρH, ρ> (heap_regions, str);
}
(注)ρH, heap_regionsは
ヒープregionを表す
構造体のRegion多相性
• 構造体はアクセスするregionが具体的に
分からなくてもよい
例 : リスト構造体の定義
struct List <ρ1, ρ2> {
int*ρ1 head;
struct List <ρ1, ρ2>*ρ2 tail;
};
Subtyping
• 型は、より短命なregionを持つ型にキャストできる
void f<ρ1, ρ2> (int b, int*ρ1 p1, int*ρ2 p2)
ρ3 {
int*ρ3 p;
ρ1とρ2はρ3より長生き
if (b)
なのでキャストできる
p = p1;
else
p = p2;
…
}
うっとおしいregion注釈を無くす
• 巧みな“デフォルトルール”によって
プログラマが明示しなければならない注釈
の量を減らす
– ルール1: ローカル変数は、推論する
– ルール2: 関数の引数や返り値のregionは全
て新しいregionを割り当てる
– ルール3: それ以外は全部ヒープregionにして
しまう
デフォルトルール適用の例
struct List <ρ1, ρ2> {
int*ρ1 head;
struct List <ρ1, ρ2>*ρ2 tail;
};
typedef struct List <ρ1, ρ2>*ρ2 list_t <ρ1, ρ2>;
list_t <ρH,
list_copy(list_t
list_copy
ρH><ρ1,
list_copy
ρ2>
lst) (list_t
<ρ1, ρ2>
<ρ1,(list_t
ρ2> lst)
<ρ1, ρ2> lst)
{
list_t res
<ρH,
= ρH>
NULL;
resルール1により推論
= NULL;
ルール2より引数には
ルール3により
ルール1により推論
新しいregion名を与える
forヒープregionとなる
(list_t <ρ1,
t = lst;ρ2>
t !=t NULL;
= lst; t !=
t =NULL;
t->tail)t = t->tail)
res = new List(new *t->hd, res);
return res;
}
Existential
• Existential型とは、型のある部分を抽象化
することによって複数の型を統一的に扱う
ための型である
• Cycloneはこのexistential型をサポートし
ている
Existential型の例
Existential型
struct IntFn ∃α {
int (*func)(α);
α env;
}
Pack可能
struct IntFn_int {
int (*func)(int*ρ);
int*ρ env;
}
型変数αを実際の型で置
き換えた型の値は全てこ
のexistential型に変換
(packという)できる
Pack可能
struct IntFn_List {
int (*func)(struct List*ρ);
struct List* env;
}
Existentialのpackの例
struct IntFn ∃α {
int (*func)(α);
α env;
}
int read <ρ> (int*ρ x) { return *x; }
L{
Existentialのpack
型int*Lを抽象化
int x = 0;
struct IntFn pkg =
<int*L>{ .func = read <L>, .env = &x };
}
Existentialのunpackの例
struct IntFn ∃α {
int (*func)(α);
α env;
}
int read <ρ> (int*ρ x) { return *x; }
int apply_IntFn(struct IntFn<L1> 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 {
Danglingポインタ発生!
struct IntFn pkg;
だが型エラーにはならない…
L2 {
int x = 0;
pkg =
<int*L2>{ .func = read <L2>, .env = &x };
}
…
}
解決策第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{
region制約 L <: L
を満たす
int x = 0;
struct IntFn<L> pkg =
<int*L>{ .func = read <L>, .env = &x };
}
Region制約を満たさない
existential packの例
struct IntFn<ρ> ∃α : regions_of (α) <: ρ {
int (*func)(α);
α env;
}
int read <ρ> (int*ρ x) { return *x; }
L1 {
型エラー region制約
L1 <: L2 を満たさない
struct IntFn<L1> pkg;
L2 {
int x = 0;
pkg =
<int*L2>{ .func = read <L2>, .env = &x };
}
}
Existentialのunpackの例
struct IntFn<ρ> ∃α : regions_of (α) <: ρ {
int (*func)(α);
α env;
関数fのeffect = { regions_of (α) }
}
生きているregion = { L }
Region制約 = { regions_of (α) <: L }
つまり、関数fは呼んでも安全!
L{
struct IntFn<L> pkg;
…
let IntFn<α> { .func = f, .env = x } = pkg;
f ( x );
}
まとめ
• Cycloneはregion-basedメモリ管理を用い
た安全なCの方言である
– 安全性は型チェックにより保証される
– スタックにデータを置くことが可能で、さらにポ
インタで指すことも可能
• Existentialによって生じるメモリ安全性の問
題は関数のeffectとregion制約によって解
決されている
References
• Cyclone homepage
http://www.cs.cornell.edu/projects/cyclone
• Region-based Memory Management in
Cyclone, Dan Grossman, Greg Morrisett,
Trevor Jim, Michael Hicks, Yanling Wang,
and James Cheney. PLDI2002. To appear.