ATSプログラミング入門:
Prev	Chapter 16. 抽象観と観型 (viewtype)	Next

メモリの確保と解放

メモリの確保と解放にまつわる問題は、実行時のガベージコレクション (GC) が許されないシステムプログラミングにおいて最重要です。メモリ管理を安全にかつ効率よく扱うことは、プログラミングの挑戦において長期にわたる未解決問題です。そして ATS におけるその新しい解決策は、定理証明によるプログラミング (PwTP) のパラダイムに堅く根差しています。

次の関数 malloc_gc がメモリ確保のために ATS では用意されています:

fun malloc_gc
  {n:nat}(n: size_t n)
  : [l:agz] (b0ytes n @ l, mfree_gc_v (l) | ptr l)
// end of [malloc_gc]

種 agz は NULL でないアドレスとして定義されたサブセット種です:

sortdef agz = {a:addr | a > null} // [gz] for great-than-zero

整数 N が与えられた時、型 b0ytes(N) は N バイトの未初期化の配列を表わす @[byte?][N] の略記です従って、駐観 b0ytes(N)@L は L をメモリ位置とすると、配列観 array_v(byte?, L, N) と同じです。観コンストラクタ mfree_gc_v は抽象的です。与えられた位置 L について、観 mfree_gc_v(L) は次の関数 mfree_gc によって解放されるべき位置 L に確保したメモリを許可する能力を表わします:

fun mfree_gc
  {l:addr}{n:nat}
  (pfat: b0ytes(n) @ l, pfgc: mfree_gc_v (l) | p: ptr l): void
// end of [free_gc]

今まで紹介してきた中では、mfree_gc_v(L) はどのような駐観の上にも構築されていないはじめての観の形であることに注意してください。

実際には、バイト数を直接扱うのはいくぶん面倒です。 (ある型の) 単一の値を保管するメモリを確保する関数 ptr_alloc と、そのようなメモリを解放する関数 ptr_free が用意されています:

fun{a:vt0p}
ptr_alloc ()
  :<> [l:agz] (a? @ l, mfree_gc_v (l) | ptr l)
// end of [ptr_alloc]

fun ptr_free
  {a:t@ype}{l:addr}
  (pfgc: mfree_gc_v (l), pfat: a @ l | p: ptr l):<> void = "mac#%"
// end of [ptr_free]

さらに、(ある型の) 値の配列を格納するメモリを確保する関数 array_ptr_alloc と、そのようなメモリを解放する関数 array_ptr_free があります:

fun{a:vt0p}
array_ptr_alloc
  {n:int}
(
  asz: size_t n
) : [l:agz]
(
  array_v (a?, l, n), mfree_gc_v (l) | ptr l
) // end of [array_ptr_alloc]

fun{}
array_ptr_free
  {a:vt0p}{l:addr}{n:int}
(
  array_v (a?, l, n), mfree_gc_v (l) | ptr l
) : void // end of [array_ptr_free]

ここで配列の確保と解放の両方を必要とする現実的で興味深い例を紹介します。次の2つの関数テンプレート msort1 と msort2 は与えられた配列をマージソートします:

typedef cmp (a:t@ype) = (&a, &a) -> int

extern
fun{
a:t@ype
} msort1 {n:nat}
  (A: &(@[a][n]), n: size_t n, B: &(@[a?][n]), cmp: cmp(a)): void
// end of [msort1]

extern
fun{
a:t@ype
} msort2 {n:nat}
  (A: &(@[a][n]), n: size_t n, B: &(@[a?][n]) >> @[a][n], cmp: cmp(a)): void
// end of [msort2]

与えられた配列の2つのソート済み部分をマージするには追加領域が必要になることがよく知られています。 msort1 が配列 A と B に対して呼び出された時、配列 A はソートされる対象で、配列 B は (ソート済みの配列の領域の) マージを行なうのに必要なスクラッチ領域の一種です。 msort1 呼び出しが返ると、A のソートされたバージョンはまだ A に保管されています。 msort2 が行なうことも同様ですが、msort2 呼び出しが返ると A のソートされたバージョンは B に保管されます。興味を持った読者には、良い練習問題として msort1 と msort2 の相互再帰的な実装をしてみることをおすすめします。 msort1 を用いたマージソートの実装は次のようにたやすく与えることができます:

extern
fun{
a:t@ype
} mergeSort{n:nat}
  (A: &(@[a][n]), n: size_t n, cmp: cmp(a)): void
// end of [mergeSort]

implement
{a}(*tmp*)
mergeSort (A, n, cmp) = let
  val (pfat, pfgc | p) = array_ptr_alloc<a> (n)
  val ((*void*)) = msort1 (A, n, !p, cmp)
  val ((*void*)) = array_ptr_free (pfat, pfgc | p)
in
  // nothing
end // end of [mergeSort]

明確に、配列は (スクラッチ領域として使われるために) はじめに確保され、それからもはや使わなくなった後に解放されます。

また、特殊な関数 alloca を呼び出すことでコールスタックにメモリを確保する関数も作ることができます。それには ATS では次のような型が与えられます:

(*
staload "libc/SATS/alloa.sats"
*)
fun alloca
  {dummy:addr}{n:int} (
  pf: void@dummy | n: size_t (n)
) : [l:addr] (bytes(n) @ l, bytes(n) @ l -> void@dummy | ptr(l))

alloca に割り当てられた型は、型付けされた ATS コードが alloca 関数呼び出しが返った後に誤ってその関数呼び出しから得られたメモリにアクセスすることを防止します。

次の関数 array_ptr_alloca_tsz は動的には alloca と同じです。しかしより便利な型が付けられています:

fun
array_ptr_alloca_tsz
  {a:vt0p}{dummy:addr}{n:int}
(
  pf: void@dummy | asz: size_t(n), tsz: sizeof_t(a)
) : [l:addr] (array(a?,n)@l, array(a?,n)@l -> void@dummy | ptr(l))

例として、上記で実装された関数テンプレート mergeSort 次のように実装することもできます:

implement
{a}(*tmp*)
mergeSort (A, n, cmp) = let
  val tsz = sizeof<a>
  var dummy: void = ()
  prval pf = view@dummy
  val (
    pfat, fpfat | p
  ) = array_ptr_alloca_tsz{a}(pf | n, tsz)
  val ((*void*)) = msort1<a> (A, n, !p, cmp)
  prval ((*void*)) = view@dummy := fpfat (pfat)
in
  // nothing
end // end of [mergeSort]

ここではマージを行なうのに必要なスクラッチ領域として使われる配列を mergeSort のコールスタックに確保しています。この mergeSort の実装は興味深いものですが、実際には以前の実装より劣っています。大きなメモリチャンクを確保する alloca 呼び出しはクラッシュをたやすく引き起こし、その原因を見つけ出すのはしばしば困難です。一般に、malloc よりも alloca を使うことは正当化しずらく、後者に対する呼び出しは綿密に精査すべきです。

配列に対するマージソートの実装全体とテストコードはオンラインから入手できます。

Prev	Home	Next
抽象観と観型 (viewtype)	Up	例: 配列を用いたリングバッファ