Compiler

Ownership analysis and memory verification

How the compiler decides which allocations die with their function, and the options that report and verify that analysis.

since 0.1.0-alpha.1linux

Description

Leviathan manages memory for you, and the analysis described here never changes what a program prints or when it ends. It only decides how cheaply memory can be released. The compiler examines every place a program creates an object, an array, a map, a range or a closure and sorts each one into one of three groups:

Scope-owned: the value provably dies with the function that created it. The compiler can free it when the function returns without any bookkeeping at run time.
Transferred by return: the function hands the value to its caller, so the caller's scope becomes responsible for freeing it.
Reference counted: the value is stored in another object or collection, captured by a closure, thrown, passed to a function the compiler cannot see into, or otherwise might outlive its function. These values are counted and freed when the last reference goes away.

Three options expose this to you. --ownership prints the classification, --ir-verify runs the program and checks the classification against what really happens, and --mem-verify reports how the program's allocations lived and died.

--ownership prints one block per function. Each line names the instruction that creates the value, the instruction's position in the function's bytecode, and the verdict. It ends with a summary of the totals. The report covers the standard library as well as your code, so it is long; filter it for the function you care about.

A value that never leaves its function

class Box {
    int v;
    new Box(int x) {
        v = x;
    }
}

int sum(int n) {
    Box b = Box(n);
    return b.v + 1;
}

console.writeln(sum(41));

Run it ▶

For that program --ownership reports the Box created in sum as scope-owned:

$ leviathan --ownership box.lev | grep -A1 '^sum:'
sum:
  @0 NewObject -> scope-owned

--ir-verify executes the program on the bytecode interpreter and, whenever a scope-owned value should have died, checks that nothing still refers to it. The program's own output goes to standard output. The summary goes to standard error, and for the program above it contains the line

[ownership] 1 scope-owned allocation(s) tracked, 0 violation(s)

which says how many scope-owned allocations were tracked and how many violations were found.

A violation means the analysis was wrong. Each one is reported on standard error and the compiler exits with status 1. --mem-verify also runs the program on the bytecode interpreter and reports on standard error how many heap allocations it made, how many were alive at once, and how many became unreachable before the program ended.

Rules

The analysis never changes a program's output. It only affects how memory is released.
A value that is returned, thrown, stored in an object or collection, captured by a closure, or passed somewhere the compiler cannot see is reference counted, not scope-owned.
--ir-verify and --mem-verify run the program in the compiler's process on the bytecode interpreter. Neither produces an executable.
With --ir-verify a single violation makes the compiler exit with status 1.
The --ownership report is written to standard output. The verification summaries of --ir-verify and --mem-verify are written to standard error.

Examples

Looking only at one function of a report:

leviathan --ownership app.lev | grep -A5 '^sum:'

Verifying a whole program. --ir-verify exits with status 0 when the analysis held, so it can run in a continuous-integration job:

leviathan --ir-verify app.lev

Notes

Reference counting cannot release a cycle of objects that refer to each other. Break such a cycle with a weak back-reference.

Ownership analysis and memory verification

Description

Rules

Examples

Notes

See also