Proposal: A verified region based memory manager for Low*

Regions in F* and Low* are, currently, purely for specificational purposes only

Yet, regions and references are an integral part of Low*'s memory model with their compilation via F*+KreMLin granted special status: region-associated references and buffers are compiled to pointers in C.

• The rid type is erased at runtime

• The core type of references is defined in FStar.Monotonic.HyperStack:

private noeq
type mreference' (a:Type) (rel:preorder a) =
  | MkRef : frame:rid -> ref:Heap.mref a rel -> mreference' a rel

And the core type of buffers is in LowStar.Monotonic.Buffer:

val mbuffer (a:Type0) (rrel rel:srel a) :Tot Type0

Both of these types have special status in extraction by F* and KreMLin yielding pointers in C---a bit of Low* metatheory justifies this compilation strategy.

• Logical refinements tie mreference and mbuffer allow grouping references and buffers into regions

• Allocating references/buffers via one of several (~10) allocation functions in the Low* libraries is compiled by KreMLin to a malloc or alloca, passing a sizeof t to the allocation routine to allocate raw bytes, and then to cast the resulting void * back to the expected type.

Regions with runtime significance

Starting with the POPL '16 paper on Mumon and then in the Low* paper, we discussed the possibility of making regions concrete, hinting that we may do so in the future. I think it would be nice to do.

In particular, I see it as a useful primitive to support efficient, en masse deallocation of all objects in a region and efficient bump-pointer allocation of objects with a region. Here's what it might look like (sketch).

We define a region-based memory allocator in Low*, with the following API:

module RegionAllocator

// implemented as:
//  - a linked list of memory pages
//  - each page is an `lbuffer uint8 page_size`
//  - an offset into the head page that is that start of the free zone
type region_handle 

// Allocates a page, initializes the linked list, setting the offset to 0
val new_region_handle: unit -> ST region_handle

// checks that there is enough space in the current free zone
//     returns the size-lengthed sub-buffer starting from the current offset
//     bumps the offset
// otherwise, allocates a new page, chains it to the list, and retries
val ralloc: region_handle -> size:uint32 -> ST (B.lbuffer uint8 size)

// frees all pages
val rfree: region_handle -> ST unit

This is done once and for all as part of the Low* libraries.

Then in, say, a new library on top of LowStar.Buffer, say, LowStar.Region, we surface the RegionAllocator API to client Low* programs:

type region_handle
val as_rid: region_handle -> rid
val new_region: unit -> ST region_handle
val ralloc: r:region_handle -> x:t -> ST (mreference (as_rid r) t) 
val rallocbuf: r:region_handle -> size:u32 -> init:t -> ST (lbuffer (as_rid rid) t size)
...
val rfree: region_handle -> ST unit

Each reference/buffer allocated in a concrete region handle is "live so long as the region is live".

At F*+KreMLin extraction time, we extract and link with the RegionAllocator. new_region is wired up to RegionAllocator.new_region; likewise for rfree. For the ralloc and friends we extract to RegionAllocator.ralloc instead of malloc, passing in sizeof t and casting the result back from void* to the expected type, i.e. just as we do for malloc now.