リージョンについて

このエントリは言語実装Advent Calendar 2015 10日目の記事です

κeenです。今日はある程度gcに頼らずメモリを管理する手法、リージョンについて話そうと思います。 リージョン推論とそのアルゴリズムまで話せればよかったのですがサーベイが間に合わず…

スタックベースのメモリ管理

gcのない言語、例えばcでも自動で解放される類のメモリがあります。ローカル変数です。

ローカル変数のメモリ確保/解放戦略は単純です。ブロックの開始に確保され、ブロックの終わりに解放されます。

{
  int x;         // <- xが確保される
  {
    int y = 2;   // <- yが確保される
    {
      int z = 3; // <- zが確保される
      x = y + z;
    }            // <- zが解放される
  }              // <- yが解放される
}                // <- xが解放される

ブロックはネスト構造をとるのでメモリ管理はスタックがあれば十分で、概念としても実装としても非常にシンプルです。

しかしシンプルな一方で柔軟性に欠ける部分もあります。 初心者の時に次のようなコードを書いてコンパイラに怒られた、あるいはバグらせたことは誰しもあるのではないでしょうか。

{
  int i;
  int *x;
  {
    int y[5] = {1, 2, 3, 4, 5};
    x = y + 1; 
  }     // <- yに割り当てられたメモリはここで解放されるため、外のブロックにあるxで参照出来ない
  for(i = 0; i < 4; ++i) {
    printf("%i\n", x[i]);
  }
}

ちょっとわざとらしい例ですがこのようにブロック内で確保されたメモリが必ずブロックが終わった時に解放されるのは嬉しくないケースがあります。

リージョン

リージョンはブロックと基本的には同じ考え方です。リージョンの開始でメモリが準備され、リージョンの終わりでメモリが解放される。そしてリージョンは入れ子構造を作る。 リージョンとブロックの違いはリージョンには名前があることと、メモリを割り当てる時にどのリージョンに置くかを指定できることです。

リージョンについて説明するためにml風の小さな言語で説明しましょう。この言語にgcはありません。

let
  x = [1, 2, 3]
in
  let
    l = let
      y = append ([4, 5], x)
    in
      y
    end 
  in
    len l
  end
end

スコープによるメモリ管理を考えてみましょう。yについて考えます。先程の考え方でいくと一番内側のスコープで作られたyはスコープの外まで生きていないのでlに渡すのは不正です。 これはつらいですね。代入を許さない言語だと値を返せなくなります。

次に、リージョンを導入してみます。リージョンを作る構文として、letregionを導入します。

リージョンr1, r2を導入するには

letregion r1, r2 in
  ...
end

と書きます。そしてリージョンr1[1, 2, 3]をアロケートするには

[1, 2, 3] at r1

と書きます。また、関数fの返り値をリージョンr1にアロケートするには

f[r1] args ...

と書きます。今回端折り気味の説明なのでこの記法の詳細は後回しにします。

リージョンとこの記法を導入した時に、先程の何がしたいのか分からないプログラムは次のように書けます。

letregion r1, r2 in
  let
    x = [1, 2, 3] at r1
  in
    letregion r3, r4 in
      let
        l = let
          letregion r5 in
            y = append[r3] (([4, 5] at r4, x) at r5)
          end
        in
          y
        end 
      in
        len[r2] l
      end
  end
end

さて、このプログラムはちゃんと齟齬なく値を渡せていて、アロケートしたメモリも全て解放されています。 リージョンを導入することでこのような小さなプログラムならgc無しでもメモリ管理が出来るようになりました。 特に、このプログラムのメモリ管理は静的です。つまりメモリをアロケートする箇所と解放する箇所がコンパイル時に決定します。

リージョンと関数

先程までは値の計算だけでした。今度は関数を定義してみましょう。 関数は返り値をどこかに返さないといけないので返り値の置き場となるリージョンを外から与える必要があります。 ということで関数はリージョンパラメータを取ります。先程の関数を返り値のリージョンを指定する構文は厳密には関数にリージョンを渡していた訳です。

試しにappendを定義してみましょう。

letlec append[r1] p =
  let (xs, ys) = p
  in case xs of
      nil => ys
    | x::xs' => (x::letregion r2 in
      (append[r1] ((xs', ys) at r2))
    end at r1)
  end
end

この関数appendはリージョンr1とタプルpを受け取って、r1にアロケートされた値を返します。

(xs', ys)のようにappendの呼び出しのためだけに作られたタプルは短命なr2にアロケートしつつ、再帰呼び出しのappの返り値は 関数全体の返り値の一部になるのでr1にアロケートしています。

このように、リージョンさえなければ普通のmlと変わらないのにgcに頼らずメモリ管理が出来ています。

リージョン推論

さてさて、先程リージョンなしのml言語にリージョンを導入することでメモリを静的に管理出来ました。しかしリージョンを手で指定していくのは中々つらいものがあります。ということでリージョンをコンパイラで勝手に推論してしまおうというのがリージョン推論です。

リージョン推論を導入することで今までgcでメモリを管理していたのをある程度静的に管理することが出来ます。 リージョン推論のアルゴリズムは冒頭で述べたようにサーベイが間に合いませんでした。

sml処理系のml kitはリージョン推論を導入することでgcをほとんど無くし、リアルタイム性に優れる処理系になりました。 先程から「ほとんど」といっているのは既存のプログラミング言語だとリージョンを綺麗に割り当てることが出来なくてほとんどのオブジェクトがトップレベルリージョンに推論されてしまい、あまり意味がなくなってしまうからだとか。丁度動的型付き言語に型推論を入れてもほとんどobject型になってしまうのと同じような話なんですかね。

発展的話題

リージョンサイズ解析

今まで、リージョンによるメモリの確保/解放については話してきましたが確保するサイズについては触れてきませんでした。 簡単にはmalloc realloc free相当の機能を考えれば済むのですが、例えばコンパイル時点で最大確保サイズが分かっているのなら コールスタックに載せて確保/解放を高速化することが出来ます。

そのコンパイル時に出来るだけリージョンの最大サイズを判明させようというのがリージョンサイズ解析です。

線形/アフィン型

線形型は全てのリソースに対が必ず丁度1回消費されることを要求する型システムです。必ず消費されるのでメモリの解放が必ず行われることを型レベルで保障します。そして最大1回しか消費されないので他者が同じリソースを触って大惨事になるデータ競合を防ぐことが出来ます。 しかし推論は完全には出来ず、ユーザがちょくちょく整合性が取れていることの証明を書く必要があります。ATS2は線形型を持っており、厳密なリソース管理が出来ます。

アフィン型は線形型よりは少し緩い型システムで、リソースが最大でも1回しか消費されないことを要求します。メモリなどの管理は出来ませんがデータ競合を防ぐことは出来ます。

Rustはアフィン型を導入してるらしいです。多分所有権回りの話なんでしょう。リージョンも導入してるらしいです。生存期間回りの話なんでしょう。

余談ですがリージョンとアフィン型の関係を調べようとしたら画像の特定領域に台形変換を掛ける話しかヒットしませんでした。ググラビリティ低い…

まとめ

  • リージョンについて話した
  • リージョン推論のアルゴリズムについては話さなかった
  • リージョン以外にもリソースを管理する方法はあるよ
  • みんなRust使おう。

全然理解が追い付かないまま期限が来て半知半解で書いてるので詳しい方κeenまでツッコみお願いします。

参考文献

  1. A Brief Introduction to Regions 今回の記事はこの論文の内容をかい摘んで書いてある。
  2. Implementation of the Typed Call-by-value lambda-calculus using a Stack of Regions (多分)リージョンの初出論文
  3. A Region Inference Algorithm リージョン推論のアルゴリズム。70ページある…
  4. ML Kitの論文たち ここに色々論文ある。
Written by κeen
Older article
SML#でDBに接続