ATS‎ > ‎

Manipulating flat memory

This guide gives an overview about manipulating flat memory data structure in ATS. The types of flat memory supported by ATS have the t@ype sort.

Flat type and size

The following built-in primitive types have the sort t@ype and are all flat: bool, char, double, int, uint, size_t and void. In addition, ATS supports flat data structure types for tuple, record, and array.

t@ype Type
Tuple @(t1, t2, ... tn)
Record @{lab1 = t1, lab2= t2, ... labn= tn}
Array
@[t][n]

Every t@ype has an associated size information, but the size information is unknown to the ATS compiler. The static sizeof(t) function (where t is a t@ype or a viewt@ype) gives you the unique static variable of the int sort, assigned to represent the size of t. The dynamic "{t:viewt@ype} sizeof()" function (which is a template function parameterized by t@ype or viewt@ype t) gives you an integer indexed by the static variable associated with static sizeof(t). It is possible to write "sif sizeof(t) == 4 then ... else ..." or "assert {t} sizeof() == 4" to make assumption about the size of t, but in general the size of any t@ype is unknown to us.

View of memory region

Flat t@ype on its own isn't very useful. If anything, it describes just the layout of memory but doesn't tell you anything else. In particular, it doesn't tell you:

  • If we do own a piece of memory with that layout.
  • The address of the memory.
  • Whether the memory is well-aligned.
  • How the memory is allocated: from the garbage collector, malloc(), shmget()/shmat(), mmap(), or even on the stack.

Terminology

The dynamic world of ATS has three kind of terms.
  • A type (also t@ype, viewt@ype) characterizes an expression.
  • A view characterizes a linear proof term.
  • A prop characterizes a propositional proof term.
After compilation, all linear and propositional proof terms are erased, and the program is left with expressions to be evaluated at run-time when someone executes the program.
In order to access flat memory, we need two pieces of information: a proof of the view "t @ l", which states that we have type t at memory location l, and a value of type "ptr l", which is a pointer pointing to memory location l.

Typically, each heap allocator will also give you a linear proof of an abstract view of the sort "addr -> view" which testifies that location l:addr is allocated by that allocator. This way, the memory allocated from one heap cannot be freed to another heap.

To allocate flat data structure on stack, ATS introduces a new form of "var" binding.

t@ype Expression Type
Tuple @(e1, e2, ... en) @(t1, t2, ... tn)
Record @{lab1 = e1, lab2 = e2, ... labn= en} @{lab1 = t1, lab2= t2, ... labn= tn}

Flat array on stack is a bit different.

t@ype Syntax Binding
Array
(single initializer)
var !p with pf = @[t][n](e)
p:ptr l
pf:@[t][n] @ l
Array
(uninitialized)
var !p with pf = @[vt][n]() p:ptr l
pf:@[vt?][n] @ l

(TODO: unfinished)

Comments