TR-1: Memory management in Mica

Mica Technical Report 1 - first edition, September 2026. States the compiler as of release 7.5.

Abstract

Mica manages heap memory without a garbage collector, without a borrow checker, and without lifetime annotations - and still makes a promise most systems languages do not make. A program that compiles has no memory leak, no use of memory after its release that the compiler could see, and no pointer into an activation that has already returned. The few cases no compile-time analysis can decide are caught while the program runs, on a build made for testing.

This report explains how, for readers who know what a stack and a heap are but have not studied compilers. The design rests on four ideas, and each is simple on its own.

• Values are copied. An assignment copies everything you can see, and the only sharing a program has is a pointer its own source spells out. So at any moment, every value is in exactly one place.
• The structure of calls is the structure of lifetimes. Every piece of heap memory has exactly one owner - usually the activation that made it, sometimes a named enclosing activation, sometimes the program as a whole - and when the owner ends, its memory comes back all at once. The mechanism behind this, the region, costs one addition per allocation and nothing per release.
• A cell your code allocates itself is a debt. Memory taken with new is an obligation the compiler follows along every path until one of four constructs pays it.
• A returned value travels through a small dedicated area. The calling statement opens that area before the call and closes it afterwards, so values handed back from a call are neither kept forever nor copied twice.

Text follows the same rules as everything else: a string built inside a statement lives for that statement, and a string stored somewhere is copied into the memory of whatever holds it.

Every mechanism is described with a picture and with the textbook algorithm it is an instance of. The report states exactly what is guaranteed and at which point - by the compiler, or while the program runs - what is deliberately not guaranteed, and what each guarantee costs, with measurements from the compiler’s own test programs.

1. Introduction

Every language that gives programs a heap has to answer one question: when does a piece of memory come back? The industry has three families of answers. A garbage collector answers when the collector next runs, at the price of a runtime that must scan, pause, or trace, and a memory footprint that is a multiple of the live data. Manual management answers when the program says so, at the price of the classic defects - leaks, double frees, uses after free - that decades of tooling have failed to eliminate. Ownership type systems answer when the owner goes out of scope, statically, at the price of a type discipline the programmer must satisfy at every function boundary.

Mica’s answer draws on an older idea that the ownership systems generalized: memory has structure, and the structure is already written in the program. Every running program is a tree of activations - calls in progress - and every value a program holds is held somewhere: in a variable of some activation, in a global, or in a cell - one piece of memory taken from the heap while the program runs, with an address of its own - reached through a pointer that is itself held somewhere. If each piece of memory is owned by exactly one such place, and each place has a well-defined end, then the end of the place is the end of the memory, and no separate accounting is needed.

What makes this workable in Mica, where it was not workable in older structured languages, is the value model. When an assignment copies a value rather than sharing it, a value cannot be reached from two places at once unless the source spells a pointer, and pointers are visible where they are written. The compiler can then reason about every place a value can be: it knows the owner of every cell, it knows when every owner ends, and it can check that no use of a cell happens after the end of its owner. The result is a memory model in which the programmer writes ordinary code - allocate, assign, call, return, and dispose the cells the code owns outright - and the compiler either proves that memory is handled correctly or says, at the exact line, which release is missing.

None of the mechanisms is new in isolation, and the report names the textbook form of each where it appears: the activation tree and the access link of every compiler text [1, 10], stack-like sequential allocation [2], lifetime-based arenas [3], region-based memory management [4, 5], the secondary stack of Ada implementations [6], typestate for the obligation analysis [8], and the exact-fit free list of the allocator literature [7]. What is Mica’s own is the combination, and the one decision that makes the combination close without annotations: values are copied at lifetime boundaries, so a value is always in exactly one place.

This report is written for programmers and for computer science students who know what a stack frame and a heap are but have not studied compilers. It proceeds from the model to the mechanisms to the guarantees:

• Section 2 introduces every word this report uses, one at a time and each with a picture, so that no later sentence steps from one unknown term to another.
• Section 3 states the value model, the rule everything else rests on.
• Section 4 describes the lifetime structure: activations, scopes, and the three kinds of owner - and where in the toolchain each decision is made.
• Section 5 describes regions, the mechanism that turns ownership into memory, and the two memory classes a program can be built for.
• Section 6 describes explicit cells - new and dispose - and the obligation analysis that governs them.
• Section 7 describes the result region, through which values travel from a callee to its caller.
• Section 8 describes text: strings, views, and builders, and the rule that gives a string its lifetime.
• Section 9 describes what changes under concurrency, and why almost nothing does.
• Section 10 states the guarantees in one table, with where each is established, and what is deliberately not guaranteed.
• Section 11 gives the cost model and measurements.
• Section 12 places the design among its precedents; Section 13 concludes.

A glossary and the references close the report. A reader who has never met the words activation, region, or arena should read Section 2 first; the rest of the report uses them exactly as Section 2 defines them and never redefines them.

2. The words, one at a time

Texts about memory management lose most readers on the words rather than on the ideas. Heap, arena, region, frame, activation, cell, owner are used differently by different books, and two of them - arena and region - are often used for the same thing. This section introduces every word this report needs, in an order where each is built only from the ones before it, with one small program and one picture per step. Nothing here is advanced; everything later depends on it.

2.1 A program runs as calls, and each call has storage

procedure Helper(n : int64);
var
    x : int64;
begin
    x := n * 2;
end;

procedure Work();
var
    i : int64;
begin
    i := 3;
    Helper(i);
end;

begin                { the main body }
    Work();
end.

While Helper is running, three calls are in progress at once: the main body, Work, and Helper. Each has storage of its own - Work has its i, Helper has its n and its x. The storage that belongs to one call in progress is that call’s activation. Most textbooks call the same thing a stack frame; this report says activation because, as Section 2.5 shows, a call in Mica owns more than the frame itself. When Helper returns, its activation is gone and x with it; when Work returns, i is gone.

   newest ─►  ┌─ Helper ─────────┐  n = 3, x = 6   gone when Helper returns
              ├─ Work ───────────┤  i = 3          gone when Work returns
   oldest ─►  ├─ main body ──────┤  the program's own variables
              └──────────────────┘

Figure 1 - three activations, one per call in progress. The newest ends first.

2.2 Some values do not fit in the activation: heap memory

A variable such as x : int64 has one fixed size, so the activation can hold it directly. A dynamic array grows while the program runs, and a string may be any length, so their storage cannot be sized when the activation is set up. It lives elsewhere - in heap memory, a pool of memory from which a program takes pieces while it runs. The activation then holds only a small, fixed-size handle: for a string, a pointer to the characters and their count.

   activation of Work                      heap memory
   ┌──────────────────────────┐            ┌──────────────────────────┐
   │ i : 3                    │            │                          │
   │ s : [pointer ●─]────────────────────────► "hello, world"         │
   │     [count   12]         │            │                          │
   └──────────────────────────┘            └──────────────────────────┘

Figure 2 - a string’s characters live in heap memory; the activation holds the handle.

Every language that has heap memory must answer one question: when does a piece of heap memory come back, so that it can be used again? The whole of this report is Mica’s answer.

2.3 Where heap memory comes from: the memory class

Before any rule about when memory comes back, one fact about where it comes from. A Mica program is built for one of two memory classes, chosen with a compiler flag and changing nothing in the source:

• hosted - heap memory comes from the operating system, through the same allocator every program on a server or a desktop uses;
• fixed arena - there is no operating system heap. The program carries one byte array of a size chosen at build time, and all of its heap memory is taken from that array. This is the shape an embedded device needs: no operating system, a fixed amount of memory, and nothing allowed to grow beyond it.

   hosted
   ┌──────────┐  take / give back  ┌──────────────────────────────┐
   │ program  │ ◄────────────────► │ the operating system's heap  │
   └──────────┘                    └──────────────────────────────┘


   fixed arena
   ┌──────────┐  take / give back  ┌──────────────────────────────┐
   │ program  │ ◄────────────────► │ one byte array of N bytes,   │
   └──────────┘                    │ carried by the program;      │
                                   │ no operating-system heap     │
                                   └──────────────────────────────┘

Figure 3 - the two memory classes. Only the source of the bytes differs.

Two things to hold on to for the rest of the report. First: the class changes only where the bytes come from; every rule that follows is the same in both classes. Second: in this report the word arena means exactly this one byte array of the fixed-arena class, and nothing else. Many books use “arena” for the technique introduced in Section 2.6; this report calls that technique a region, precisely to keep the two apart.

2.4 The unit of heap memory: the cell

One piece of heap memory, taken while the program runs, is a cell. A cell has an address; a pointer is a variable that holds an address, so a pointer names a cell. A string’s characters are a cell, a dynamic array’s elements are a cell, and new Node makes a cell. When the report says “a cell comes back”, it means the cell’s memory is available to be taken again.

   p : [pointer ●─]───────────►  ┌──────────────┐
                                 │ a cell:      │
                                 │ Node { ... } │
                                 └──────────────┘

Figure 4 - a pointer names a cell.

2.5 Who answers for a cell: the owner

Mica’s first rule about when: every cell has exactly one owner, and an owner is a place with a definite end. The usual owner is the activation whose variable holds the value. In the program of Section 2.1, suppose Work had a dynamic array: its elements would be a cell owned by Work’s activation, and they would come back when Work returns - with nothing written to make it so. This is what “a call owns more than its frame” meant in Section 2.1.

   activation of Work            what Work owns in heap memory
   ┌───────────────────┐      ┌────────────────────────────────────────┐
   │ i : 3             │      │ [elements of a][chars of s]            │
   │ a : handle ●──────┼────► │                                        │
   │ s : handle ●──────┼────► │ all of it comes back when Work returns │
   └───────────────────┘      └────────────────────────────────────────┘

Figure 5 - an activation owns the cells its variables hold, and they end when it ends.

There are two other kinds of owner, both met later: a named enclosing activation (spelled until Owner at the allocation, Section 4.2), and the program - meaning the whole run, from start to exit, which is how this report uses that word wherever it names an owner (a global variable’s cells, and until program). And there is one deliberate exception: a cell made with new and no until has no owner in this sense - your own code must end it with dispose, and Section 2.7 says how the compiler makes sure it does.

2.6 How an owner keeps its cells: the region

How can an activation give back all its cells at once, without keeping a list of them? By keeping them together. An owner’s cells are carved one after another out of large blocks of heap memory - taking a cell is moving a pointer forward inside the current block - and the owner’s chain of blocks is its region. Giving everything back is returning the blocks. The blocks themselves come from the memory class of Section 2.3: from the operating system’s heap, or from the arena.

   region of Work
   ┌ block 1 ──────────────────────────────┐
   │ [cell][cell][cell][cell]  next ─►     │ ◄─ a block
   └───────────────────────────────────────┘
   ┌ block 2 ──────────────────────────────┐
   │ [cell]  next ─►                       │ ◄─ a block
   └───────────────────────────────────────┘
         Work returns: both blocks go back where they came from

   where blocks come from (the memory class):
   hosted: the operating system's heap · fixed arena: the arena

Figure 6 - a region: one owner’s chain of blocks. The blocks come from whichever memory class the program was built for.

This is where the two look-alike words part ways, and the distinction is worth a table:

2.7 Cells your code owns outright: the obligation

For a cell made with new and no until, your code decides the end and spells it with dispose. The compiler then checks that it really does, on every path from the new to the end of the run; the debt a new creates is an obligation, and the check is the obligation analysis. A path that reaches the end without a dispose is a compile-time error that names the line. A cell made with new ... until Owner or new ... until program needs no dispose at all: the until hands the obligation to the owner, and the owner’s end is the release. Such a cell’s last pointer may be dropped whenever you like - a cell nobody can reach any more is not a leak, because the owner releases it regardless. While a pointer to it is still held, an early dispose is permitted and ends the obligation then; it is the exception, not the expectation. Section 6 gives the four ways an obligation may be met.

   p := new Node ─► ... ─► dispose p ─► end      ✓ the obligation is met
   p := new Node ─► ... ─► (no dispose) ─► end   ✗ refused at compile time

Figure 7 - an obligation follows a cell along every path.

2.8 Values that travel from a call to its caller: the result region and the window

Consider kept := Build(seed), where Build returns an array. Build makes that array inside its own activation, and that activation ends the moment Build returns — so the array cannot live there. It cannot live in the caller’s region either, because a routine cannot name its caller’s region. Mica gives this hand-over a region of its own, the result region, and one rule for using it: the statement that makes the call opens a window on that region, and closes it when the statement ends.

Read the four moments below. The result region is drawn as one row of memory that fills from left to right, and the caret marks the position the statement remembered.

          the result region [...] at four moments of 'kept := Build(seed)'

              1. before the call   [ earlier values                   ]
   the                                               ^ the mark: the
   window ─┐                                           statement notes
   opens   │                                           this position
           │
           │  2. inside 'Build'    [ earlier values ][ the array      ]
           │                                                           ^
           │                       'Build' has nowhere else to put its
           │                       result, so it builds it past the mark
           │
           │  3. the store         [ earlier values ][ the array      ]
           │                                              │ copied out ^
           │                                              ▼
           │                       kept, in its own region: [ the array ]
           │
   closes ─┘  4. statement ends    [ earlier values                   ]
                                                     ^ the release: back
                                                       to the mark, and
                                                       everything past
                                                       it is free again

Figure 8 - a statement’s window on the result region. The value crosses from callee to caller in step 2, is copied to its real owner in step 3, and the space it borrowed is handed back in step 4.

Read the picture in two directions, because it holds two different things. The boxes are memory: the result region’s contents, drawn as one row that fills from left to right. The bracket down the left is time: the window is not a piece of memory at all but the stretch between the mark and the release, and what makes it a window is that everything written into the region during it is gone at its end.

One thing the drawing can mislead about: the result region is not the machine stack. Build’s parameters and locals live on the stack and vanish when it returns; the result region is separate memory, and that is the whole point — it is where a value can outlive the activation that made it without outliving the statement that asked for it. What is stack-like is only the discipline: marks and releases nest last-in-first-out.

So where does its memory actually come from? From exactly where every other region’s memory comes from. The result region is a region in the sense of Section 2.6 — a chain of blocks, filled by moving a position forward — and its blocks are requested from, and handed back to, the memory class of Section 2.3: the operating system’s heap in a hosted build, the byte array in a fixed-arena build.

   the memory class (Section 2.3): the hosted heap, or the fixed arena
          │  blocks out, blocks back
     ┌────┴─────────┬──────────────┬─────────────────────────┐
   Main's         Work's        the program's         the result region
   region         region        region                one per task
     │              │              │                         │
   ends when      ends when     ends at process       truncated back to a
   Main ends      Work ends     exit                  mark at each window's
                                                      end - never as a whole

Figure 9 - every region draws its blocks from the same source; what differs is when each one gives them back.

Only two things separate the result region from the owners’ regions of Section 2.5. Who ends it: an owner’s region is released whole when the owner ends, while the result region is never released whole — it is truncated back to a mark at the end of every statement that opened a window. How many there are: each owner has its own, and the result region is one per task — a task being one thread of execution: the program itself until a concurrent block schedules more, each of which then runs its own activations on its own core (Section 9). A returned value’s bytes are therefore ordinary heap memory from the ordinary source; the only special thing about them is when they are given back.

Two details are worth keeping. Step 4 costs nothing per value: the region gives memory back by moving its position marker, not by releasing values one at a time. And the window belongs to the statement, not to the call — which matters when the statement is a loop like for x in Build(...), because the returned array has to survive every round of that loop, and the statement that encloses it is the first moment at which the value is certainly dead.

Readers who know Ada will recognise this: it is the secondary stack that Ada implementations use to return values whose size the caller cannot know, down to the mark-and-release pair and the one-per-task rule, and Mica adopts it deliberately [6]. Mica puts one more kind of value in it, which Section 8 needs: a string that is materialized and never returned at all — the result of a + used as an argument or a condition — also lives here, and dies when its statement ends.

2.9 The remaining words, briefly

• task - one thread of execution: the program itself, or one of the tasks a concurrent block schedules onto the cores. Each task runs its own activations and keeps its own regions (Section 9).
• statement scope - a variable declared inside a loop body lives for one iteration; its cells come back at the end of each round.
• cleanup list - what an activation does at its end, newest-first: run its defer statements, release the cells it still owes, and finally return its region.
• materialize - to make a new string: +, ToString, and the string-returning library verbs.
• view and builder - stringpart, a window over a string’s characters that owns nothing, and stringbuffer, growable text storage.
• checked tier - the develop-and-test build on which every explicit cell carries a live/released marker, so what the compiler could not prove is caught when it runs.

2.10 The whole picture

   at compile time, the compiler decides
     owners and scopes · the obligation analysis · window decisions
   ────────────────────────────────────────────────────────────────────
   at runtime, the program keeps
     program ── owns the globals' cells; region "until program"
     │
     ├─ main body ── activation, region
     │    │
     │    └─ Work ── activation, region: [block][block]
     │         │
     │         └─ Helper ── activation, region
     │
     ├─ explicit cells: new ... dispose, each its own piece
     └─ result region, one per task: [ ... ] marks and releases
   ────────────────────────────────────────────────────────────────────
   chosen per build, the memory class supplies every byte above
     hosted heap: the operating system's heap
     fixed arena: one byte array

Figure 10 - everything in one picture: the compiler decides at compile time, the running program keeps owners, regions, explicit cells, and the result region, and all of their bytes come from whichever memory class was chosen.

2.11 Who uses what, across the two memory classes

Because this is the question that confuses readers longest, it gets its own table. Every row is used in both classes; the last column is the whole of the difference.

With the words in place, the report can now say what the rules are.

3. The value model

The rule is one sentence, and it is worth reading twice: an assignment copies the value, and the only sharing a program has is a pointer its own source declares.

var
    a, b : Numbers;         { Numbers = array of int64 }
begin
    a := new Numbers reserve 2;
    Append(address a, 1);
    Append(address a, 2);
    b := a;                 { b now has its own elements }
    Append(address b, 3);
    WriteLn("%lld %lld", Length(a), Length(b));   { 2 3 }
end.

After b := a, the two arrays are independent. There is no handle inside b that quietly points at a’s elements, no reference count that the two share, no copy-on-write bookkeeping deferred to the first mutation. The same holds for a record that contains an array, for a fixed array of records, and for a string. Value types are values all the way down.

Sharing, when you want it, is a pointer, and it is spelled: address x creates one, value p reads or writes through it, and a parameter that receives a pointer says so in its type. Every call site that can change your variable is visible at the call site, because it hands over an address.

Two consequences shape everything that follows.

The first is that a copy happens at every lifetime boundary, never at an aliasing boundary. Because two places never share storage, a value that is stored into a longer-lived place is copied into that place - and once it is, the place owns the copy for the rest of its life. There is no moment at which storage belongs to two owners, and therefore no moment at which the end of one owner could invalidate the other. This is the property the whole memory model depends on, and it is a property of the language, not of the implementation.

The second is that the compiler knows where every value is. A value lives in the variable that holds it; a variable belongs to an activation, to a program, or to a record or array that in turn belongs to one; and the only way to reach a value from anywhere else is a pointer the compiler can see being created. This knowledge is what makes the analyses of Sections 6 and 8 decidable without annotations.

The price of the model is copies, and Section 11 measures them. The design position is that a copy at a lifetime boundary is the honest cost of a value that outlives its maker, that it is paid exactly where the source shows it, and that the alternatives - a count on every cell, a trace over the live set, or a proof obligation on the programmer - each cost more in a way that is harder to see.

4. The lifetime structure

4.1 Activations and scopes

A call creates an activation: the frame that holds the callee’s parameters and local variables, alive from the call until the return. Activations nest - a callee’s activation sits inside its caller’s - and at any moment the live activations form a chain from the program’s main body down to the innermost running call. Over the whole run they form the activation tree of the compiler textbooks [1, §7.2], and a routine declared inside another reaches the enclosing routine’s frame through an static link [1, §7.3.5] - the discipline N. Wirth described for nested functions or procedures [10].

   program ── owns the globals; ends at process exit
   │
   ├─ main ── activation: its locals, its region
   │    │
   │    ├─ Load(...) ── ends at its return: the region
   │    │
   │    └─ Encode(text) ── activation: its locals, its region
   │          │
   │          ├─ [statement scope] ── a 'var' in a loop body: a fresh
   │          │                       variable each round, gone at the
   │          │                       back edge
   │          │
   │          └─ Merge(parts) ── activation nested in Encode: reaches
   │                             Encode's cells through the static link
   │
   └─ Report() ── activation: its locals, its region

Figure 11 - the activation tree. Every value lives in exactly one node of this tree, and every node has a well-defined end.

Inside an activation, Mica has a second, finer structure: a variable may be declared inside a statement list rather than in the activation’s declaration part, and such a variable lives from its declaration to the end of the enclosing statement list. A loop body that declares a variable gets a fresh one every iteration, and the old one ends at the back edge. These statement scopes matter for memory because a value held by such a variable can be reclaimed at the end of the scope rather than at the end of the whole activation.

4.2 The three owners

Every allocation in a Mica program belongs to exactly one owner, and there are three kinds:

The first row is the one most code lives in. A local dynamic array, a string built inside an activation, a record with a heap-carrying field - each is made in its activation and gone at the return, with nothing written to make it so.

function Work(seed : int64) : int64;
var
    scratch : Numbers;
begin
    scratch := new Numbers reserve 64;
    { ... fill and use scratch ... }
    Work := Length(scratch);
end;                                    { scratch's memory returns here, wholesale }

The second row is for the case where the maker is not the natural owner - a helper that builds items for a pool, where the pool’s activation should own them:

procedure Pool();
var
    a, b, made : pointer int64;

    procedure MakeItem(v : int64);
    begin
        made := new int64 until Pool;   { owned by Pool, however deep the activation that made it }
        value made := v;
    end;

begin
    MakeItem(10);
    a := made;
    MakeItem(20);
    b := made;
    WriteLn("%lld", value a + value b);
end;                                    { both items drain here }

When is a named owner the right tool? Whenever a helper builds parts of something whose lifetime is the owner’s - the nodes of a list or a tree, the entries of a table - and would otherwise have to hand each part’s obligation back to its caller. The helper’s own pointer variable ends with the helper; that does not matter, because every node lives on in a place that outlives the helper: the owner’s own variable (made above, or the head of a list), a field of another owned node (a tree’s child pointer), or a global for until program. A helper may also simply return the cell it made:

function Build(count : int64) : int64;
var
    head, walk : pointer Node;
    i, sum : int64;

    function MakeNode(v : int64) : pointer Node;
    var
        made : pointer Node;
    begin
        made := new Node until Build;   { owned by Build, however deep the activation }
        made.item := v;
        made.tail := head;
        MakeNode := made;               { returned, but nobody owes a dispose }
    end;

begin
    head := nil;
    for i := 1 to count do
        head := MakeNode(i);            { the node lives on in head and in the next node's tail }
    ...
end;                                    { the whole list returns here, at once }

Two thousand calls of this function, each building a fifty-node list, run inside a sixty-four-kilobyte arena: every list is gone before the next call begins, and no line of the program frees a node.

The third row is the program itself, the owner that never ends before the process does. A global variable’s contents belong to it, and so does anything allocated until program.

One allocation is deliberately absent from the table: an explicit new T with no lifetime clause. Such a cell has no owner in this sense - its life is yours to end with dispose, and Section 6 describes the analysis that makes sure it does.

4.3 One rule for where a stored value lives

The three rows combine into one rule the rest of the report applies over and over: a value lives exactly as long as the longest-lived place that holds it, and a store into a place copies the value into that place’s owner. A string assigned to a local is copied into the activation; the same string assigned to a global is copied into the program; an array appended to a record’s field is copied into whatever owns the record. The copy is the mechanism by which the rule is kept true, and the owner of the destination is always known at the store.

   before the store
   Encode's region              program's region
   ┌────────────────────┐       ┌────────────────────┐
   │ piece ──► "ab"     │       │ kept ──► ∅         │
   └────────────────────┘       └────────────────────┘

   after   kept := piece;
   Encode's region              program's region
   ┌────────────────────┐       ┌────────────────────┐
   │ piece ──► "ab"     │       │ kept ──► "ab"      │  a copy: the
   └────────────────────┘       └────────────────────┘  program owns it

   Encode returns: its region is gone and so is its "ab";
   kept's bytes are untouched - kept never shared them

Figure 12 - the store rule. The destination’s owner receives its own copy, so no end of any other owner can invalidate it.

4.4 Who decides what, and when

Readers who want to know “where is what managed” can keep this table beside the rest of the report. Three actors share the work: the compiler’s analyses, which run over the whole program at compile time; the code the compiler generates into each function; and the runtime library that every Mica program links.

Nothing in the first six rows costs anything at run time, and nothing in the last four requires a decision from the programmer.

5. Regions: how ownership becomes memory

5.1 Bump allocation and wholesale release

Each owner that allocates anything gets a region: a chain of large blocks from which its allocations are carved by advancing a pointer. Allocating a cell costs one comparison and one addition; there is no size class, no free-list search, no header per cell. When the owner ends, the region’s blocks are given back whole. Nothing is freed cell by cell, ever, on this road.

   region of activation W               allocate 24 bytes:
   ┌────────────────────────────────┐    if used + 24 > capacity
   │ block 1 [cell][cell][cell]     │        open a new block
   │         ◄──── used ────►│ free │    cell := base + used
   └────────────────────────────────┘    used := used + 24
   ┌────────────────────────────────┐
   │ block 2 [cell][cell]           │    W returns:
   │         ◄─ used ─►│ free       │        give back block 2
   └────────────────────────────────┘        give back block 1

Figure 13 - a region. Allocation is sequential allocation in Knuth’s sense [2, §2.2.2]; release is the whole chain at once.

This is the classic arena - Hanson’s “allocation based on object lifetimes” [3] - and it is what makes the activation-lifetime model free rather than merely correct: reclaiming a thousand cells costs the same as reclaiming one. It is also what makes a small fixed memory budget livable (Section 5.4): a function that allocates half a kilobyte per activation and frees nothing, called five thousand times, uses half a kilobyte, because every activation’s region is back before the next one begins.

A region is created lazily, at the owner’s first allocation, so an activation that allocates nothing pays nothing - not a word of bookkeeping.

5.2 The cleanup list

An owner’s region is not the only thing the owner reclaims at its end. A defer statement registers cleanup code to run at the activation’s exit; an explicit cell (Section 6) may be registered so that the owner disposes it if the code did not; a container of owned cells may need its fields released. All of these hang on one per-owner cleanup list, in registration order, and the activation’s exit drains the list newest-first - the order in which nested resources must be undone.

   registration order during W          drain order at W's exit
   ────────────────────────────         ──────────────────────────────────
   1. defer Close(file)                 3. run the deferred Close(file)
   2. cell := new Node until W          2. dispose the cell (if still owed)
   3. first region allocation           1. run the deferred WriteLn(a[0])
   4. defer WriteLn(a[0])               4. release the region  ← always last

Figure 14 - the cleanup list. Deferred code and owned cells drain newest-first; the region node drains last, so a deferred read of a region-resident value always finds it.

The region’s place at the very end is load-bearing: a deferred statement may read a value that lives in the region, so the region must still be there when it runs. The first edition of this report can name the defect that taught the lesson: a region node placed at the front of its list drained before a deferred read registered earlier, and the read touched freed memory. It was found by the analysis that prepared the string-lifetime work described in Section 8 and fixed the same day; the test corpus now pins the order.

5.3 Reuse within a region

Bump allocation never gives a cell back individually, so a variable that is assigned again and again inside a loop would, naively, leave a trail of dead cells behind it until its owner ends. Two rules keep the common loops at one cell.

Reuse in place. A dynamic array assigned into a destination that already has a large enough backing keeps that backing and copies into it - the rule the mainstream value-semantic containers follow. A destination assigned in a loop settles at zero allocations after the first.

Rebump. A destination whose old cell is the newest cell of its region - the common case when one variable is overwritten repeatedly - has that cell resized in place, grown or shrunk, instead of abandoned. This is what lets a string accumulator or a growing array reuse one cell across an entire loop.

   round n:     [ ... ][ s: "abc"  ]     used
                                         s := s + "d": the old cell is used

   round n+1:   [ ... ][ s: "abcd"  ]    the newest 
                                         it grows in place - no new cell

Figure 15 - the rebump. The newest cell of a region can grow or shrink in place because nothing lies beyond it.

Neither rule is a guarantee against all growth. Two variables of the same owner, each overwritten in turn, interleave their cells and the second cannot be rebumped; the growth is then bounded by the owner’s life, which for a loop-body variable is one iteration and for a global is the program. Section 10 measures a real instance.

5.4 The two memory classes, and what they do not change

Everything described so far - owners, regions, the cleanup list, the reuse rules, and the obligations, windows, and string rule of the sections to come is one model, and it is the same model whether a program runs on a server or inside an embedded device with no OS heap usage. What differs between those two deployments is only the bottom layer: where a region’s blocks and an explicit cell’s bytes physically come from. Mica makes that a build decision, the memory class, and keeps the whole model above it unchanged.

   the program's text
     new · dispose · := · until · defer · leave · + · ToString
   ─────────────────────────────────────────────────────────────────
   the compiler's analyses (compile time)
     owners and scopes · the obligation analysis · the walls
     (stack escape, borrow, view) · window decisions
   ─────────────────────────────────────────────────────────────────
   the runtime's model (every build, every class)
     regions and their blocks · cleanup lists · marks and releases ·
     reuse and rebump · checked-tier headers
   ─────────────────────────────────────────────────────────────────
   the block source (chosen per build)
     hosted heap: the operating system's heap - blocks and cells from it,
             returned to it; transparent to memory checkers
     fixed arena: one static byte array, a bump cursor, an exact-fit
             free list

Figure 16 - the layers. The memory class replaces only the bottom row; the model above it is identical, and so are the guarantees of Section 10.

The bottom layer has exactly three duties, and each class discharges all three: hand out a zeroed piece of memory for a cell or a bookkeeping node, hand out a block for a region, and take either back. The hosted-heap class does this with the operating system’s allocator, which is why a hosted build is transparent to the standard memory checkers - a region’s block is an ordinary allocation to them. The fixed-arena class does it inside one statically sized byte array: a bump cursor hands out fresh pieces, and everything taken back goes onto a free list from which a later request of the same size is served before the cursor advances. That exact-fit reuse is what keeps the arena from fragmenting - a loop whose activations each want a block of the same size reuses the same block forever - and it is the choice the allocator survey [7] recommends when request sizes repeat, which is exactly what activation lifetimes produce. The arena is the shape an embedded deployment requires, where there is no heap to draw from and the budget is the whole memory; the same source compiles for either class with a flag, and the same test programs run under both.

Two consequences are the same in both memory classes and worth stating plainly. Every piece of memory handed out is zero, so a Mica variable of any type starts from a known state. And running out is not undefined behavior: the arena reports exhaustion as the same deterministic runtime failure every allocation can raise, with the file and line of the allocation that asked, and a hosted build reports the allocator’s refusal the same way.

6. Explicit cells and obligations

6.1 new and dispose

Regions cover values. For the cases where you want an individually managed cell - a node of a linked structure, a resource with a lifetime the call structure does not describe - Mica has new and dispose, and it treats the pair as a debt. new creates an obligation; dispose discharges it; and the compiler follows the obligation along every control path from the allocation to the end of the run. This is a typestate analysis in the sense of Strom and Yemini [8] - a cell is owed, released, or transferred, and every operation is legal only in some states - carried out as a data-flow analysis over the control-flow graph [1, ch. 9].

   p := new Node                       state: owed
        │
        ├── dispose p ────────────────►  released           ─┐
        ├── defer dispose p ──────────►  released at leave   │ the four roads
        ├── Make := p  (return it) ───►  transferred         │ that discharge
        ├── p := new Node until Pool ─►  owned by Pool      ─┘ the obligation
        │
        └── a path reaching the end with p still owed
                                     ─► obligation error 13102, at that line

Figure 17 - the obligation. Every path from the allocation must reach one of the four discharging constructs; the analysis names the path that does not.

obligation error 13102: heap cell is not released on every path: last use at
line 9, the path leaving at line 10 releases nothing - dispose it, defer the
dispose, return it, or bind it to an owner with 'until'

The message is the whole discipline. There are exactly four ways to meet the obligation:

1. dispose it - an explicit release on every path;
2. defer the dispose - one defer dispose x at the top holds for every exit, early leaves included;
3. return it - a function whose result is an owning pointer transfers the obligation to its caller, visibly, through the type;
4. bind it to an owner - new T until Owner hands the obligation to an enclosing activation, which discharges it at its exit as part of its cleanup list.

There is a fifth road that is not a way of your own but the owner’s: a new stored into an owning pointer field of a record hands the obligation to the record, and the record’s dispose releases what the record owns, leaves first, absent children skipped, the record’s cell last - the compiler synthesizes that release per record type. An owning slot that gives its cell up is cleared: a dispose spelled through a field or an element stores nil into that place, and a field or element handed to an owning pointer parameter is nil once the call returns, so a program that releases children by hand before their owner stays correct and nothing is released twice. A plain variable keeps its pointer after its dispose, which is what the checked tier below reads.

The analysis also refuses the mirror defects: a dereference after a dispose on every path reaching it (13105), and a second dispose of a cell already released on every path (13104). These are compile-time answers; the programs do not build.

6.2 Borrowing

A pointer parameter that should read and write a cell but must not release it is spelled borrowed. The compiler enforces the word: a borrowed pointer cannot be disposed, cannot be stored where an owner is expected, and cannot be returned as an owner. The owner keeps the obligation; the callee gets the access. The same word serves a field that holds a view of a structure without owning it, and the back edge of an owned structure - a child’s pointer to its parent - which would otherwise form a cycle of owners.

6.3 The checked tier

Two temporal errors cannot always be decided at compile time: a use after a dispose that happens on some paths, and a second dispose that depends on data. For these the compiler has a checked build tier. On it, every explicit cell carries a small header with a live/disposed state; dispose poisons the state and keeps the cell in a quarantine rather than returning it to the allocator, so the poison survives for the rest of the run; and every dereference and every dispose checks the state first. A stale pointer is then caught however long after the release it is used, and reported at its line. A region cell reached through a pointer carries the same header on this tier, and when its region drains every word its cells occupied is set to the same poison and never handed out again for the rest of the run, so a stale pointer into a drained region — one a store through a pointer left where the compiler could not follow it — meets the guard’s poison exactly as a disposed cell does, and is reported at its line. The checked tier also detects a cycle of owners at an owner’s drain, by bounding the depth of the release descent. The release tier carries none of this; the checked tier is the develop-and-test tier, and its guarantee is total on the defects it exists for.

6.4 Where an explicit cell’s bytes live

An explicit cell takes one of two roads, decided by its spelling:

• new T with no clause is an individual cell: its bytes come straight from the memory class’s bottom layer, and dispose gives them straight back - to the operating system’s heap in a hosted-heap build, onto the arena’s free list in a fixed-arena build. Nothing else ever reclaims it, which is exactly why the obligation analysis insists that something does.
• new T until Owner and new T until program place the cell in the named owner’s region. The program may still dispose it early - the obligation analysis is satisfied either way - and that dispose is a no-op for the bytes: the obligation ends at the dispose, the bytes return with the region when the owner ends.

The second road is a deliberate separation of semantics (when the code may no longer use the cell) from mechanics (when the memory comes back). Both roads exist in both memory classes and on both build tiers; the obligation analysis is the same compile-time analysis over both, and the checked tier’s headers guard both.

7. The result region: values that cross activations

7.1 The problem

A function that returns a dynamic array, a string, or a record containing either produces a value inside an activation that is about to end. The value cannot live in the callee’s region, which is drained at the return; it cannot live in the caller’s region, which the callee cannot name; and giving it to the program forever means a loop over such a function grows without bound.

7.2 Marks and windows

Mica’s answer is the one Ada’s implementations chose for the same problem [6]: a result region, a bump region with a different reclaim rule. The caller takes a mark — a record of the region’s current position — before a statement that will call a value-returning function, and releases back to that mark when the statement ends; in between, the callee writes its result there and the statement copies it into whatever it assigned it to. Section 2.8 draws the four moments and says where the region’s own memory comes from; this section states the three rules that follow from it. Releasing to a mark on a bump region is truncation — nothing is freed value by value — which is the mark-and-release discipline of the classic stack-like allocators [2, §2.2.2], applied to one region with the statement as its unit.

The window is the statement, not the enclosing block. A for x in Build(...) loop walks the returned array for the whole loop, so a release on the loop’s back edge would free the array being walked; the statement that encloses the loop is the first point at which the value is provably dead. Every statement that calls a function whose result owns region memory opens a window; every other statement pays nothing.

Windows nest exactly as statements do, last-in-first-out, and a nested window’s release truncates only to its own mark:

   for x in Build(100, 5) do     ← outer window: mark M1;
   begin                            result A lives above it
       kept := Build(700, 3);    ← inner window: mark M2 above A;
   end;                             result B above M2; release to
                                    M2 - A is untouched, still walked
                                 ← after the loop: release to M1,
                                    A is gone

Figure 18 - nested windows. The inner release cannot reach past its own mark, so the value the loop is walking survives every iteration.

Some expressions get a narrower window still. A condition, a case selector, and a counted loop’s bound exist only to yield a scalar, so their window closes the moment that scalar has been extracted, before any nested statement runs. Inside a loop this releases every iteration’s temporary in that iteration, which is what keeps while Length(Step(round)) > 0 running in constant space.

7.3 The exclusions

One statement must never release: the one that writes the enclosing function’s own result. The value it produces belongs to the caller, and the release would hand back the memory the caller is about to read. The compiler therefore declines a window for a statement that writes a result variable holding region memory - directly, through a field, or anywhere inside a compound statement - and for a statement that calls into a nested routine which writes its host’s result. Such a statement’s temporaries live until the caller’s own window closes: a bounded price, paid only on these shapes.

A function whose result holds no region memory - an integer, a float, a plain record - is not excluded: Count := Length(a + b) releases its temporary the moment the statement ends.

7.4 One region per task

Marks and releases are strictly last-in-first-out within one task’s execution, and the result-region state is therefore kept per task: two tasks running on two cores each keep their own order, and neither can release back past a mark the other still has open.

8. Text

8.1 The string value

A string is an immutable value: a small descriptor - a pointer to the characters and a length counted in code points - over a block of characters that is never modified after it is made. A literal’s characters live in the program’s static data. Every other string is materialized by one of a few operations: the concatenation +, ToString over a builder or over a view, and the string-returning verbs of the standard units, which are written in Mica and use the same operations.

Because the characters are immutable, two descriptors may point at the same block without one observing a change made through the other; the only thing that can distinguish sharing from copying is lifetime. That observation gives the string its rule.

8.2 The rule

A materialized string is born in the result region, under the window of the statement that materializes it; a string stored into a place is copied into that place’s owner; a string passed as an argument is shared.

                a + b  is materialized in the statement's window
                                   │
        ┌──────────────────────────┼──────────────────────────┐
        │                          │                          │
   passed as an              used as an operand         stored into a
   argument                  or a condition             place
        │                          │                          │
   the callee shares         read, compared,            the bytes are
   the bytes; its call       measured; the window       copied into the
   ends inside this          releases them when         place's owner:
   statement's window        the statement ends         the activation,
                                                        or the program

Figure 19 - the three roads a materialized string can take, and the lifetime each one gets.

procedure Encode(piece : string);      { shares the caller's bytes for the call's duration }
begin
    ...
end;

var
    kept : string;                     { a global: owned by the program }
begin
    for i := 1 to 200000 do
        Encode(word + " " + suffix);   { born in the window, released at the end of the statement }
    kept := word + " " + suffix;       { copied into the program's region }
end.

The three roads are the value model’s three lifetime boundaries. The argument road shares because a callee’s activation is always inside its caller’s statement, so the caller’s window outlives every use the callee can make - the compiler refuses the two constructs that could break this: a task’s and a generator’s inputs must be plain values, and a string is not one, so a string input to either is refused at compile time (Section 9). The store road copies because the destination may outlive the statement. And the window road gives a temporary exactly the life of its statement, so the millions of pieces a tokenizer cuts from a corpus each live for one statement and no longer.

Two refinements keep the common store free. A literal source is never copied - its characters are static and outlive everything. And a string materialized straight into a function’s result variable is not copied either: it was born in the result region, which is exactly where the copy would go, so the result variable simply takes the descriptor - the string form of return-value optimization, free by construction.

The stores that do copy reuse the destination’s old cell whenever the rebump rule of Section 5.3 allows, so a string variable overwritten in a loop holds one cell across the loop.

8.3 Views and builders

Two further text types complete the picture, and both are described in detail in the text article. A view (stringpart) is a window over a string’s characters - a descriptor with no storage of its own. It allocates nothing and is the tool for tokenizing; the compiler walls it in so that it can never outlive its source: a view cannot be stored durably, returned unless it is rooted in a parameter the function never reassigns, or kept past the activation that formed it. Storing a view’s text is spelled ToString, which materializes it. A builder (stringbuffer) accumulates text in amortized time where repeated + would copy quadratically; it owns its growable storage under the same region rules as a dynamic array, and ToString reads it out without disturbing it.

A string that has views formed over it is treated slightly more carefully by the store road: its cells bind to the whole activation rather than to a statement scope, and the rebump rule never touches them, so every view formed anywhere in the activation outlives every read of it.

9. Concurrency

Mica’s concurrency model - tasks scheduled inside a concurrent block, the structural join at the block’s end, and compile-time data-race freedom from a marking discipline over the activation tree - is the subject of the data-races article and is not restated here. What this report has to say is how little of the memory model changes when tasks run on several cores, and why.

The principle is partition, do not share. Each task has its own activation tree, its own regions, and its own result-region state, so the common allocation and release paths take no lock at all.

   task A (core 1)                    task B (core 2)
   ┌───────────────────────┐          ┌───────────────────────┐
   │ activation regions    │          │ activation regions    │
   │ result region + marks │          │ result region + marks │
   │ region list           │          │ region list           │
   └───────────────────────┘          └───────────────────────┘
        no lock                            no lock

   shared, each under one small lock, reached only by programs that
   use them:
   ┌────────────────────────────────────────────────────────────┐
   │ the fixed arena's byte budget · the early-dispose registry │
   │ the program-lifetime region                                │
   └────────────────────────────────────────────────────────────┘

Figure 20 - partition per task. The common paths never meet; the three things that cannot be partitioned each take one lock held inside a single primitive.

Three things cannot be partitioned and each takes one small lock held only inside a single primitive: the fixed arena’s byte budget, which every core draws from; the registry that lets an early dispose find a cell’s owner from any core; and the program-lifetime region, whose cells any task may allocate and release. Two of the three are gated so that a program which never uses them never reaches the lock, and none of it exists in a single-core build, whose generated code is byte-identical to what it was before multicore existed.

A task’s inputs, and a generator’s, are plain values by rule: a value whose every byte is the value itself. A string, a dynamic array and a pointer are not — their bytes live in a cell the value only points at — so a task parameter, a generator parameter and a stream element of any of those types are refused at compile time (5318, 5370, 5375); what is admitted is copied into the task’s own frame at schedule. This is what lets the argument road of Section 8 share a string’s bytes: no admitted callee can outlive its caller’s statement, because no string ever crosses into one.

10. The guarantees, stated

10.1 What a guarantee means here

A guarantee in this report is a specification plus a commitment.

The specification says what a conforming Mica compiler does: which programs it refuses, which checks it plants, and what a program that compiles may therefore rely on. The table below is that specification.

The commitment says what happens when the compiler and the specification disagree: a program that violates a stated guarantee is a compiler defect of the highest class — reported at the top of the queue, fixed with priority, and pinned by a regression test in the corpus so that it cannot return. It is never answered by quietly narrowing the claim.

This is the meaning the word carries in every language that guarantees something about memory or types without a machine-checked proof of its entire implementation. Rust keeps a dedicated label for soundness defects in safe code and has been fixing them since before its 1.0 release; Java’s type system carries a deliberate unsoundness in array covariance; Ada’s SPARK subset proves properties with a toolchain that has defects of its own; and even CompCert, whose optimizer carries a machine-checked correctness proof, had defects found by random testing in the parts the proof did not cover. None of them withdrew a guarantee on that account, and none of them should have. A guarantee states what the language promises and what its maintainers owe — not a claim that no defect will ever be found.

What backs the commitment is evidence, and the evidence is public. Every merge runs the whole corpus three times over — more than twelve thousand declared runs per gate — across both architectures, both memory classes, both text encodings, and the single- and multi-core runtimes, and a gate that executes fewer runs than its recorded count fails on that difference alone. Beyond the corpus, the model is attacked deliberately: programs are written whose purpose is to violate a stated guarantee, and each one that the compiler accepts is a defect under the commitment above. The most recent such sweep, in September 2026, wrote 258 of them; 87 were refused with diagnostics naming the consequence, and of those that were not, twelve were closed the same day — the rule they exposed is stated in the table’s first rows — five were caught by the checked tier exactly as the table says unprovable cases are, and one remains open and is named in the list of what is not guaranteed below. That is the process this report describes, running.

10.2 The table

The table lists each property, the construct that establishes it, and the moment at which it is established. “Compile time” means the program does not build; “every tier” means a runtime check that release builds keep; “checked tier” means the develop-and-test build.

What is not guaranteed, said out loud:

• Bounded memory in every loop. A variable overwritten in a loop holds one cell when the rebump rule applies and grows otherwise, bounded by its owner’s life. The bound is always known - the owner - and never silent, but a global overwritten among other globals in a long loop grows until process exit. The remedy is to declare the accumulator in the loop’s scope, or to build with a builder.
• Reclaim before the owner ends. A region gives nothing back until its owner does. A very long activation that allocates steadily holds its memory for its whole life; the design answer is the same - a statement scope, a named owner, or an explicit cell.
• Zero copies. The value model copies at lifetime boundaries. A program that stores every temporary pays a copy per store, deliberately visible.
• Cross-task sharing without marks. Sharing between tasks is spelled synchronized, and unmarked sharing is refused; there is no unsafe door.
• A compile-time refusal of every store through a pointer into storage that outlives what is stored. The escape rule refuses a store whose destination it can name - a global, a variable of an enclosing activation, a container those root in, the pointee of a global pointer. A store written through a pointer parameter (p.field := q) reaches whatever the caller’s p happens to point at, and which storage that is depends on the pointer’s value rather than on the program’s text, so the rule does not judge it: refusing every such store would reject the ordinary doubly-linked structure, whose two cells belong to one owner and die together. This is the same unprovable half that use-after-release has, and it has the same answer: the checked tier reports the stale read at its line, as the table above states; the release tier does not.

11. Costs and measurements

11.1 The cost model

11.2 What the test corpus pins

The compiler’s test corpus contains programs that hold a fixed memory budget across hundreds of thousands of rounds, and that fail loudly - by arena exhaustion at a named line - if any round retains anything. Three of them describe the model directly:

• Fifty thousand rounds each of a global overwritten with the same string, a global overwritten with alternating longer and shorter strings, and a procedure that copies two strings into its locals, all inside a one-megabyte arena. The first two rounds settle on one cell each through the rebump rule; the third gives its activation’s region back on every return.
• Two hundred thousand rounds of every shape a materialized string can stand in - a bare call argument, a kept call result, the five expression windows, a loop over a temporary, a forwarded result, an ordinal-returning function, a record result with a string field, a deferred materialization, and two tasks materializing at once - each flat in a one-megabyte arena, on both encodings, both memory classes, and the multicore runtime.
• Twenty thousand returned arrays of fifty elements, in a sixty-four-kilobyte arena sixteen times smaller than the default, together with the shapes that would read a released result back if the window rule released one moment too early.

11.3 A whole program

The program that motivated the string rule is a byte-pair tokenizer: it cuts a text into pieces with a regular expression and encodes each piece, and over a twenty-two-million-character corpus it cuts 5.7 million pieces. Before the rule, every piece that was handed to the encoding procedure was kept for the whole run, because an argument may in principle be stored by its callee and the compiler could not prove otherwise; the program’s memory grew by roughly 140 megabytes across the encode loop from pieces alone. After the rule, each piece lives for one statement, and the elimination measurement - the same program with the encode step removed, and with the output list removed - shows no growth attributable to the pieces at all. The growth that remains has two named owners, neither of them a string: the output list of token identifiers, which doubles its backing as it grows and cannot rebump when other program-lifetime allocations sit above it, and a per-match retention inside the regular-expression engine’s cursor, which is bounded by the activation that drives the cut and is the subject of its own work item. These measurements were taken on a development machine and serve to attribute, not to benchmark; the release’s documented-machine run carries the published numbers.

12. Related work

The activation-owned region is the oldest idea here. Sequential allocation with a stack discipline is the first storage scheme in Knuth’s treatment of dynamic storage [2], and Hanson’s arenas [3] made “allocate by lifetime, free all at once” a systems-programming idiom. Region-based memory management was formalized by Tofte and Talpin [4], who inferred regions and their lifetimes from a program’s structure through an extended type system; Cyclone [5] brought regions to a C-like language with explicit region annotations. Mica’s regions need neither the inference nor the annotations, because the value model removes the aliasing that makes region inference hard: a value is in one place, and that place’s owner is the region. Ada’s secondary stack [6], on which its implementations return values of a size the caller cannot know, is the direct precedent of the result region, down to the choice of the statement as the release boundary. Storage pools and arenas, in Ada and in the systems languages that expose them as libraries, are the precedent of the fixed-arena class, and the exact-fit list inside it follows the allocator survey’s guidance for repeating request sizes [7]. The named owner - new T until Owner - has its own ancestors, and naming them is part of the claim. The ML Kit’s region calculus lets an expression allocate at ρ into an enclosing region [4], and Cyclone’s rnew(r, ...) allocates into an outer region through its handle [5]; both need a region-typed handle or an inferred region variable at every such site. Ada 2012’s subpools let a program allocate into a named subpool and release it whole [6]. Apache’s pool hierarchy and the arena libraries of several systems languages offer the same discipline as a library, with the pool passed by hand. Mica states the same relation with the enclosing routine’s name alone

• no handle, no region parameter, no lifetime annotation - because lexical nesting fixes the owner; and, unlike the library forms, the obligation analysis knows the construct, so a cell bound to an owner is proven not to leak rather than assumed. The price is the one the whole model pays: an owner is a routine or the program, never an object made at run time and handed around. Obligation tracking for explicit cells belongs to the family of typestate analyses [8]; Mica’s version is deliberately confined to the explicit cell, where it can be complete, and never asked to reason about values, where the region does the work. The escape analyses of the compiler literature [9] are the road not taken for text: an earlier design bound a string temporary to its activation only when a proof showed it never escaped, and the report’s Section 8 describes what replaced the proof - a copy at every store, which needs no proof at all. The reader who wants the concurrency side’s precedents will find them in the data-races article.

13. Conclusion

Mica’s memory model is three rules and a mechanism for each. Values are copied, so a value is in one place. Places belong to owners - an activation, a named activation, or the program - and an owner’s end is its memory’s end, implemented by regions that allocate by bumping and release by truncation. Explicit cells are obligations the compiler follows to the end of every path. Values cross activations through a result region that the calling statement marks and releases. Text obeys the same store rule as every other value, and its temporaries live exactly one statement. What the compiler cannot decide it checks on a tier built for the purpose, and what it will not guarantee it says. None of this requires an annotation from the programmer, and all of it survives the move from a host’s heap to a fixed arena and from one core to many.

Glossary

• heap memory - memory a program takes while it runs, as opposed to the fixed-size storage of an activation; the general name, whatever the memory class it comes from.
• memory class - the build-time choice of where heap memory comes from: the hosted-heap class (the operating system’s heap) or the fixed-arena class (one static byte array).
• arena - the one static byte array a fixed-arena program carries in place of an operating-system heap. In this report never a synonym for region.
• block - one large piece of heap memory a region carves its cells from.
• cell - one unit of storage with an address: a variable’s storage in an activation or in the program’s own storage, or one allocation carved from a region. It is the thing a pointer names and the unit every lifetime rule is stated over. An explicit cell is one made with new, whose release the code must spell; every other cell returns with its owner.
• activation - one call in progress: its parameters, locals, and the memory it owns. Ends at the return.
• static link - the pointer from a nested routine’s frame to its enclosing routine’s frame, through which it reaches the enclosing cells.
• statement scope - the extent of a variable declared inside a statement list; a loop body’s scope ends at every back edge.
• owner - the activation, named activation, or program that reclaims an allocation when it ends.
• region - an owner’s chain of blocks, allocated by bumping and released whole at the owner’s end.
• cleanup list - an owner’s registration list of deferred statements, owned cells, and its region, drained newest-first at the owner’s exit.
• rebump - resizing a region’s newest cell in place when the variable that holds it is overwritten.
• obligation - the debt an explicit new creates and one of four constructs must discharge on every path; the obligation analysis is the compile-time check that every path does.
• borrowed - a pointer that may read and write a cell but may never release it or become its owner.
• result region - the per-task region a function’s returned value is written into, marked and released by the calling statement.
• window - the interval between a statement’s mark and its release; the life of every temporary the statement materializes.
• materialize - to make a new string: concatenation, ToString, and the string-returning verbs.
• view - a stringpart: a window over a string’s characters with no storage of its own, walled so it cannot outlive its source.
• builder - a stringbuffer: growable text storage read out by ToString.
• checked tier - the develop-and-test build on which every explicit cell carries state and every use of it is checked.

References

1. A. V. Aho, M. S. Lam, R. Sethi, J. D. Ullman. Compilers: Principles, Techniques, and Tools, 2nd edition. Addison-Wesley, 2006. Chapter 7 (run-time environments: activation trees, static links) and chapter 9 (data-flow analysis).
2. D. E. Knuth. The Art of Computer Programming, Volume 1: Fundamental Algorithms, 3rd edition. Addison-Wesley, 1997. Section 2.2.2 (sequential allocation) and section 2.5 (dynamic storage allocation).
3. D. R. Hanson. “Fast allocation and deallocation of memory based on object lifetimes.” Software: Practice and Experience 20(1), 1990.
4. M. Tofte, J.-P. Talpin. “Region-based memory management.” Information and Computation 132(2), 1997.
5. D. Grossman, G. Morrisett, T. Jim, M. Hicks, Y. Wang, J. Cheney. “Region-based memory management in Cyclone.” PLDI, 2002.
6. ISO/IEC 8652, Ada Reference Manual, section 13.11 (storage management) and section 13.11.4 (storage subpools, Ada 2012); and the secondary stack as implemented for functions returning values of unknown size, described in the GNAT documentation.
7. P. R. Wilson, M. S. Johnstone, M. Neely, D. Boles. “Dynamic storage allocation: a survey and critical review.” International Workshop on Memory Management, 1995.
8. R. E. Strom, S. Yemini. “Typestate: a programming language concept for enhancing software reliability.” IEEE Transactions on Software Engineering 12(1), 1986.
9. Y. G. Park, B. Goldberg. “Escape analysis on lists.” PLDI, 1992; and B. Blanchet. “Escape analysis for object-oriented languages.” OOPSLA, 1999.
10. N. Wirth. Compilerbau, 4th edition. B.G. Teubner Stuttgart, 1986.