Support for Low Memory

[DavePearce]

(see also #97)

An interesting use case for Whiley is to run on embedded systems. In some cases, such systems do not support dynamic memory allocation and Whiley currently makes quite a lot of assumptions here. In particular, around arrays, open records and lambdas.

Some examples:

int[] xs = [0;n]

This allocates an array of arbitrary size. Normally this would be done on the heap so that, for example, it can be passed out of the function in question. However, it could also be allocated on the stack provided it did not escape the function in question.

int[] ys = xs

This copies an array of arbitrary size, again typically by allocating it into the heap. However, this depends on whether xs is live after this statement or not.

type fun_t is function(int)->(int)

function make(int x) -> fun_t:
     return &(int y -> x + y) 

This is constructing a closure which must be allocated on the heap. There is really no other way to do it.

Overview

The following provides a rough rule of thumb about where problems arise.

• Sized Types. A statically sized type can always be stack allocated. Its only dynamically sized types that are a concern here.
• Parameters. Dynamically sized types in parameter positions are not a concern. Since they are being passed into a function, their memory is already allocated safely elsewhere.
• Returns. Dynamically sized return types are a problem. In particular, if a function attempts to return a dynamically sized object allocated in its lifetime.
• Cloning. Assigning a dynamically sized object to another variable is often problematic, though it depends on the type in question. In particular, if the type is immutable then its fine (i.e. as pointers can be simply copied). Likewise, if the source is not live afterwards then we have a move (which is fine). An interesting example here is that closures are always immutable.
• Allocation. Allocating a dynamically sized type is inherently problematic.

One option is to include an analysis to ensure the above requirements are met. We might have a modifier (e.g. static) which forces this analysis to run. All methods on a low memory embedded device might be required as static.

Valid Examples

static function head(int[] items) -> (int r)
requires |items| > 0:
   return items[0]

This is straightforward to implement in finite memory, even though it uses a variable of dynamic size.

Invalid Examples

static function f(int n) -> int:
   int[] xs = [0;n]
   return g(xs)

In principle, xs could be stack allocated. We need to infer the type int[n] for xs to make this possible.