Introduction to Programming in ATS:
PrevChapter 16. Abstract Views and ViewtypesNext

Memory Allocation and Deallocation

The issue of memory allocation and deallocation is of paramount importance in systems programming, where garabage collection (GC) at run-time may not even be allowed. Handling memory management safely and efficiently is a long standing problem of great challenge in programming, and its novel solution in ATS is firmly rooted in the paradigm of programming with theorem-proving (PwTP).

The following function malloc_gc is available in ATS for memory allocation: 

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

The sort agz is a subset sort defined for addresses that are not null: 

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

Given an integer N, the type b0ytes(N) is a shorthand for @[byte?][N], which is for an array of N uninitialized bytes. Therefore, the at-view b0ytes(N)@L is the same as the array-view array_v(byte?, L, N), where L is a memory location. The view constructor mfree_gc_v is abstract. For a given location L, the view mfree_gc_v(L) stands for a form of capability that allows allocated memory at location L to be freed (or reclaimed) by the following function mfree_gc: 

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

Note that mfree_gc_v(L) is so far the first form of view we have encountered that is not built on top of any at-views.

In practice, it is rather cumbersome to deal with bytes directly. The function ptr_alloc is available for allocating memory to store a single value (of certain type) and the function ptr_free for deallocating such memory: 

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]

In addition, the function array_ptr_alloc is for allocating memory to store an array of values (of certain type), and the function array_ptr_free is for deallocating such memory: 

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]

I now give a realistic and interesting example involving both array allocation and deallocation. The following two functions templates msort1 and msort2 perform merge-sort on a given array: 

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]

It is well-known that merging two sorted segments of a given array requires additional space. When msort1 is called on arrays A and B, the array A is the one to be sorted and the array B is some kind of scratch area needed to perform merging (of sorted array segments). When a call to msort1 returns, the sorted version of A is still sotred in A. What msort2 does is similar but the sorted version of A is stored in B when a call to msort2 returns. As a good exercise, I suggest that the interested reader take the effort to give a mutually recursive implementation of msort1 and msort2. An implementation of merge-sort based on msort1 can be readily given as follows: 

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]

Clearly, an array is first allocated (to be used as a scratch area) and then deallocated after it is no longer needed.

It is also allowed for a function to allocate memory on its call-stack by calling a special function alloca, which is given the following type in 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))

The type assigned to alloca makes it extremely unlikely for someone to unintentionally write well-typed code in ATS that may erroneourly attempt to access memory obtained from calling alloca after the calling function has returned.

The following function array_ptr_alloca_tsz is the same as alloca dynamically but it is given a type that is often more convenient to use: 

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))

As an example, the function template mergeSort implemented above can also be implemented as follows: 

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]

where the array used as a scratch area during merge-sort is allocated on the call-stack of mergeSort. While this implementation of mergeSort may seem interesting, it is actually inferior to the previous implementation as calling alloca to allocate a large chunk of memory can readily lead to a crash for which the cause is often very difficult to determine. In general, choosing alloca over malloc is difficult to justify, and any call to the former should be scrutinized.

The entire implementation of merge-sort on arrays plus some testing code is available on-line.

PrevHomeNext
Abstract Views and ViewtypesUpExample: Array-Based Circular Buffers