Locality and stack allocation

This section is about lifetime. A value has a lifetime: the time when it is valid to use that value.

OxCaml can put short-lived values on the allocation stack instead of the GC heap (in OxCaml, the allocation stack is separate from the call stack).

Regions describe when parts of the allocation stack can be reclaimed. To ensure stack allocation is safe, the compiler checks that no one uses a value after its region ends.

By the end of this section, you should be able to:

The notes below cover the same ground as the lecture slides, in more depth. The exercises are collected at the end of the page. If you attended the lecture, you can work through the exercises directly; each exercise points back to the section of the notes that explains its concept.

Why stack allocation matters

OxCaml allocation is cheap, but GC is high latency. Heap allocation creates work for the GC. In low-latency code, that future GC work can be a problem.

Stack allocation is one way to avoid that heap work. The tradeoff is lifetime: a stack-allocated value must not be used after its region ends.

A small stack allocation example

Use stack_ to put new allocations on the allocation stack. In this example, the list xs is used inside sum3. Then sum3 returns only the integer result.

OxCaml can often infer stack allocation without stack_. We write stack_ when we want to require stack allocation: if the value would have to escape to the heap, the compiler reports an error.

stack_ is shallow and attaches to an allocation construct. It does not copy values that are already available. For example, in stack_ (x, y), the pair is stack allocated, but x and y are not copied to the stack.

let rec sum (xs : int list @ local) = match xs with | [] -> 0 | x::xs' -> x + sum xs' let sum3 a b c = let xs = stack_ [a;b;c] in let n = sum xs in (* xs gets deallocated here *) n let () = let n = sum3 1 2 3 in print_endline (string_of_int n)

The important fact is simple: xs is temporary. For this first example, think of the function body as the region. The allocation stack is cleared when that region ends, so xs cannot be used after sum3 returns.

Stack allocated values cannot escape their region

A stack-allocated value cannot be stored somewhere that may outlive its region. A global reference may outlive the function call, so the code below is rejected.

let saved = ref [] let rec sum xs = match xs with | [] -> 0 | x::xs' -> saved := xs :: !saved; x + sum xs' let sum3 a b c = let xs = stack_ [a;b;c] in let n = sum xs in n let () = let n = sum3 1 2 3 in print_endline (string_of_int n)

The bug would be a dangling pointer: saved would contain a list that points into a region that has already been cleared.

Returning a stack allocated value is also an escape

Returning the integer n is fine. Returning xs is not fine, because xs points into the current region.

let rec sum (xs : int list @ local) = match xs with | [] -> 0 | x::xs' -> x + sum xs' let sum3 a b c = let xs = stack_ [a;b;c] in let n = sum xs in n, xs let () = let n, _xs = sum3 1 2 3 in print_endline (string_of_int n)

Use exclave_ to build a returned local value

Sometimes we do want to return a stack-allocated value. The keyword exclave_ ends the current region and evaluates the following expression in the caller's region.

That means the returned value is not smuggled out of the old region. It is built in the caller's region.

The function result is still at @ local. It is local to the caller's region, not global.

let rec sum (xs : int list @ local) = match xs with | [] -> 0 | x::xs' -> x + sum xs' let sum3 a b c = exclave_ let xs = stack_ [a;b;c] in let n = sum xs in n, xs let () = let n, xs = sum3 1 2 3 in print_endline (string_of_int n); print_endline (string_of_int (sum xs))

The next sections explain exclave_ in terms of regions. That region model is also what explains tail calls and mid-function exclave_.

How OxCaml manages the allocation stack

The compiler can be explained with two simple operations. A normal function starts a new region. Before the function returns, the current region ends. The diagrams below are a model for where the region boundary is.

Normal function
let f x =
  ...
  result
Region view
let f x =
  let region = start_region () in
  ...
  end_region region;
  result

start_region () returns the current allocation stack pointer. end_region region resets the allocation stack pointer to that saved pointer.

An exclave_ result is different. It moves result construction to the parent region.

exclave_ result
let f x =
  exclave_
  ...
  result
Region view
let f x =
  let region = start_region () in
  end_region region;
  ...
  result

When exclave_ is at the beginning, the function region starts and ends immediately. The result is then built in the caller's region.

Regions end before tail calls

A tail call transfers control to another function instead of returning a value. So the current region ends before the tail call.

This choice keeps tail-recursive loops from accumulating allocation-stack space as the loop runs.

Tail call
let rec loop x =
  ...
  loop next_x
Region view
let rec loop x =
  let region = start_region () in
  ...
  end_region region;
  tail call loop next_x

The attribute [@nontail] suppresses the tail call. Then the region stays alive during the call and ends only after the call returns.

Non-tail call
let f x =
  ...
  g x [@nontail]
Region view
let f x =
  let region = start_region () in
  ...
  let result = g x in
  end_region region;
  result

exclave_ in the middle of a function

If exclave_ appears after some work, the early work still belongs to the function's region. The region ends at the exclave_ point.

Source
let f x =
  let y = stack_ [1; 2; 3] in
  consume y;
  exclave_
  build_result x
Region view
let f x =
  let region = start_region () in
  let y = stack_ [1; 2; 3] in
  consume y;
  end_region region;
  build_result x

The result cannot use y, because y was allocated in the region that just ended. The result can use x, because x came from the caller.

This is the same rule as before, but the boundary is later in the function. Code before the boundary belongs to the function's region; code after the boundary builds the result in the caller's region.

The locality axis

The locality axis records how long a value may live. It answers this question: how long does this value live?

x @ global

May outlive the current region. It is safe to store or return.

outer-local

May live in an outer region. It can live past the current end_region region.

x @ local

May live in the current region. It cannot be used as a global value.

Immediate values can cross locality

Locality matters when a value may contain a pointer whose lifetime matters. An immediate value such as an int has no heap block, so it can cross from local to global.

let id_local_int (x : int @ local) : int @ global = x

A heap value such as a string does not cross locality by default. If the value is local, returning it as global would let it outlive its region.

let id_local_string (x : string @ local) : string @ global = x

Functions and exclave_

After exclave_, values from the function's region are gone. Function arguments can still be used if they came from the caller. Values allocated after exclave_ can also be used.

Source
let f (x : int list @ local) =
let y = stack_ [1; 2; 3] in
ignore (sum y);
exclave_
after exclave_
let z = stack_ [4; 5; 6] in
sum x + sum z
(* not allowed here: sum y *)
Region view
let f x =
let region = start_region () in
let y = stack_ [1; 2; 3] in
ignore (sum y);
end_region region;
(* y dies here *)
after exclave_
let z = stack_ [4; 5; 6] in
sum x + sum z
(* x came from caller *)
(* z is after exclave_ *)

What can survive exclave_?

Several kinds of values can still be used after exclave_:

Summary: locality and stack allocation rules

Use local parameters to prevent retention

So far, locality has controlled returned values. The same lifetime check also controls function parameters.

A local parameter means this: a function may use a temporary value during a call, but it may not retain that value.

The function passed to with_scratch can use the temporary state during the call, but cannot retain it. This is forced by the @ local parameter.

type scratch = { mutable total : int } let with_scratch (f : scratch @ local -> 'a) = let s = stack_ { total = 0 } in f s [@nontail] let add_with_scratch x y = with_scratch (fun s -> s.total <- x + y; s.total)

Submoding: use global data locally

A local parameter lets a function accept temporary values. The reverse direction is also useful: a long-lived value can be used where only local mode is required.

A value at global mode can be used at local mode. This is called submoding.

In this example, escape s records the string in a global history. The same string can still be passed to length, because length only requires local mode.

let saved : string list ref = ref [] let escape (s : string @ global) = saved := s :: !saved let length (s : string @ local) = String.length s let global_string @ global = "hello" (* the string is global *) let demo () = escape global_string; (* allowed because global_string is global *) length global_string (* global_string is submoded to local *) let () = print_endline (string_of_int (demo ()))

Problem: plain local containers lose the global mode

In the following example, the top-level string starts at @ global.

After matching through outer : string list @ local, the extracted inner is only local.

let saved : string list ref = ref [] let escape (s : string @ global) = saved := s :: !saved let length (s : string @ local) = String.length s let global_string @ global = "hello" (* the string is global *) let demo () = escape global_string; (* allowed because global_string is global *) let outer = stack_ [global_string] in (* global_string is submoded to local *) match outer with | [] -> () | inner :: _ -> escape inner (* we lost the information that the list elements are @ global *)

Modalities preserve the global mode

Sometimes we want to place global data into a local container without losing the information that the inner data was global. The solution is modalities.

Modalities wrap the inner data in a record field annotated with the stronger mode global, which preserves the information that the inner data is global.

type 'a global = { global : 'a @@ global } let saved : string list ref = ref [] let escape (s : string @ global) = saved := s :: !saved let demo () = let inner @ global = "hello" in escape inner; (* allowed because inner @ global *) let outer = stack_ [{ global = inner }] in (* modality preserves @ global *) match outer with | [] -> () | inner :: _ -> escape inner.global (* allowed because inner.global @ global *)

Constructing { global = inner } requires inner at @ global. Reading inner.global gives the field back at @ global, even when the record itself is used at @ local.

Runtime stack and GC heap regions with compile-time braces for local modes, submoded heap data, and global data preserved by an @@ global modality.
Locality: the heap and stack picture with modalities. Runtime placement and compile-time mode are different aspects.

Allocation recap

Exercises

These exercises check your understanding of the material from the lecture. They only assume the concepts covered above, in roughly the order the notes introduce them.

Each exercise starts with a line saying what it checks and which section of the notes to reread if you get stuck.

let rec sum (xs : int list @ local) = match xs with | [] -> 0 | x :: xs -> x + sum xs let rec range (n : int) : int list @ local = if n <= 0 then [] else stack_ (n :: range (n - 1)) let () = print_endline (string_of_int (sum (range 4)))
Answer key let rec sum (xs : int list @ local) = match xs with | [] -> 0 | x :: xs -> x + sum xs let rec range (n : int) : int list @ local = if n <= 0 then [] else exclave_ stack_ (n :: range (n - 1)) let () = print_endline (string_of_int (sum (range 4)))
let rec length (xs : int list @ local) = match xs with | [] -> 0 | _ :: xs -> 1 + length xs let use (xs : int list @ local) = length xs let bad () = let xs = stack_ [1; 2; 3] in use xs
Answer key let rec length (xs : int list @ local) = match xs with | [] -> 0 | _ :: xs -> 1 + length xs let use (xs : int list @ local) = length xs let good () = let xs = stack_ [1; 2; 3] in use xs [@nontail] let () = print_endline (string_of_int (good ()))
let rec sum (xs : int list @ local) = match xs with | [] -> 0 | x :: xs -> x + sum xs let bad (x : int list @ local) = let y = stack_ [1; 2; 3] in exclave_ sum x + sum y
Answer key

Sum y while its region is still open, and carry the int across the boundary. An int is immediate data, so it crosses locality and stays usable after exclave_. The behavior is unchanged: the function still returns sum x + sum y.

let rec sum (xs : int list @ local) = match xs with | [] -> 0 | x :: xs -> x + sum xs let good (x : int list @ local) = let y = stack_ [1; 2; 3] in let sy = sum y in exclave_ sum x + sy let () = print_endline (string_of_int (good [10]))

If a function genuinely needs a temporary list after the boundary, it can also allocate a fresh one after exclave_, like z in the diagrams above — but here that would compute a different result.

let rec range (n : int) : int list @ local = if n <= 0 then [] else exclave_ stack_ (n :: range (n - 1)) let rec sum (xs : int list @ local) = match xs with | [] -> 0 | x :: xs -> x + sum xs let expensive_search n = exclave_ let scratch = range n in let total = sum scratch in if total mod 2 = 0 then stack_ (Some (total, n)) else None
Answer key

The first exclave_ ends expensive_search's own region before range n runs, so the recursive list cells produced by range are allocated in the parent region. Move exclave_ after the list has been consumed, and only use it before allocating the returned Some.

let rec range (n : int) : int list @ local = if n <= 0 then [] else exclave_ stack_ (n :: range (n - 1)) let rec sum (xs : int list @ local) = match xs with | [] -> 0 | x :: xs -> x + sum xs let expensive_search n = let scratch = range n in let total = sum scratch in if total mod 2 = 0 then exclave_ stack_ (Some (total, n)) else None let print_result n = match expensive_search n with | None -> print_endline "None" | Some (total, original_n) -> Printf.printf "Some (%d, %d)\n" total original_n let () = print_result 3; print_result 4
let rec range (n : int) : int list @ local = if n <= 0 then [] else exclave_ stack_ (n :: range (n - 1)) let rec sum (xs : int list @ local) = match xs with | [] -> 0 | x :: xs -> x + sum xs let expensive_search n = exclave_ let scratch = range n in let total = sum scratch in if total mod 2 = 0 then stack_ (Some (total, n)) else None let expensive_search' n = let result = expensive_search n in exclave_ result
Answer key let rec range (n : int) : int list @ local = if n <= 0 then [] else exclave_ stack_ (n :: range (n - 1)) let rec sum (xs : int list @ local) = match xs with | [] -> 0 | x :: xs -> x + sum xs let expensive_search n = exclave_ let scratch = range n in let total = sum scratch in if total mod 2 = 0 then stack_ (Some (total, n)) else None let expensive_search' n = match expensive_search n with | None -> exclave_ None | Some (total, original_n) -> exclave_ stack_ (Some (total, original_n)) let print_result n = match expensive_search' n with | None -> print_endline "None" | Some (total, original_n) -> Printf.printf "Some (%d, %d)\n" total original_n let () = print_result 3; print_result 4
type scratch = { mutable total : int } let saved : scratch list ref = ref [] let with_scratch (f : scratch @ local -> 'a) = let s = stack_ { total = 0 } in f s [@nontail] let add_with_scratch x y = with_scratch (fun s -> saved := s :: !saved; (* keep s for later inspection *) s.total <- x + y; s.total)
Answer key

The lambda receives s at @ local: it may use s during the call but not retain it. Storing s in saved would let it outlive its region, so that line is rejected. The mutation and the read are allowed, so deleting the store is the whole fix.

type scratch = { mutable total : int } let with_scratch (f : scratch @ local -> 'a) = let s = stack_ { total = 0 } in f s [@nontail] let add_with_scratch x y = with_scratch (fun s -> s.total <- x + y; s.total) let () = print_endline (string_of_int (add_with_scratch 40 2))