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 is most likely forbidden or only supported in a highly restricted manner. 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] (freebyte_gc_v (n, l), b0ytes n @ 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

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?, n, l). The view freebyte_gc_v(n, l) stands for a form of capability allowing that the n bytes located at the address l be freed (or reclaimed) by the following function free_gc:

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

Note that freebyte_gc_v is so far the first 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. Instead, the following two functions are more convenient for allocating and deallocating arrays:

fun{a:viewt@ype}
array_ptr_alloc {n:nat} (asz: size_t n)
  :<> [l:agz] (free_gc_v (a?, n, l), array_v (a?, n, l) | ptr l)
// end of [array_ptr_alloc]

fun array_ptr_free
  {a:viewt@ype} {n:int} {l:addr} (
  pfgc: free_gc_v (a?, n, l), pfarr: array_v (a?, n, l) | p: ptr l
) :<> void // end of [array_ptr_free]

Given a type T, an integer N and an address L, the view free_gc_v(T?, N, L) means that the memory for the array located at L of N elements of the type T can be freed. In particular, the view freebyte_gc_v(N, L) is just free_gc_v(byte?, N, L).

I now give a realistic and interesting example involving both array allocation and deallocation. The following two functions templates msort1 and msort2 perform mergesort 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 mergesort 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}
mergesort (A, n, cmp) = let
  val (pfgc, pfat | p) = array_ptr_alloc<a> (n)
  val () = msort1 (A, n, !p, cmp)
  val () = array_ptr_free (pfgc, pfat | 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.

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