Chapter 3 — Memory & the Heap

Mica 5.0.0 Technical Portrait · Chapter 3 of 9 · reading guide

This is the chapter 5.0.0 was built around. A systems language is eventually judged by how it handles the heap, and there are only three known ways to do it, each paying a different price:

Mica takes a fourth path, and it is the reason this release matters:

Heap lifetimes are scheduled and proven by the compiler — the same way a modern backend schedules and proves register lifetimes — not discovered by a runtime and not extracted from the programmer through annotations.

No garbage collector. No borrow checker. No lifetime syntax. The same SSA, liveness, and escape machinery the backend already needs (Chapter 5) is turned on lifetimes instead of registers. This chapter covers both halves: how the compiler proves lifetimes, and how those lifetimes are served at runtime.

◈ The surfaces

The heap has a small, readable vocabulary. Every allocation has exactly one owner at every moment.

buffer := new int64;              { allocate; owned by the current function }
dispose buffer;                   { end this object's life }

defer dispose buffer;             { run dispose on every exit edge of this function }

pixels := new Frame until Render; { allocate AND bind to an enclosing function 'Render' }
cache  := new Atlas until program;{ bind to the lifetime of the whole process }

• new T — allocate a cell; the owner is the allocating function. Reclaimed when that function returns. The tightest possible lifetime.
• dispose p — end the object’s life. (A semantic event the compiler checks; when the bytes physically return is the allocator’s business — those are deliberately separate.)
• defer stmt — run a statement on every exit edge of its function, in last-registered-first order. A scope guard that lowers to ordinary code — no runtime structure, no frames (Go’s open-coded defer, adopted wholesale).
• new T until F — a single atomic allocate-and-own construct binding the cell to an enclosing function F. It is deliberately not sugar for allocate-then-register, which is the window bug that forced C++ to invent make_unique.
• until program — process lifetime; drained at exit (it works inside libraries, via the C runtime’s at-exit registration).

until F is the pivotal idea. It “lifts a cleanup out of the current frame and binds it to an ancestor” — and that ancestor is a region you can name.

◈ Owners and the contract

The whole model rests on one rule:

A program compiles only if every allocation’s obligation is discharged on every control-flow path.

An obligation is the duty created by every new. There are exactly three ways to discharge one — a closed set, by design (a new discharge channel is a deliberate language change, never something the analysis silently infers):

1. A dominating dispose — you free it on every path that reaches the exit.
2. Registration — defer dispose p, or an until form, hands the cleanup to an owner whose exit drain becomes the guaranteed backstop.
3. Transfer — you return the pointer; the caller receives the obligation.

If none of those happens on some path, the obligation is undischarged at that exit, and that is a compile-time error. The canonical failing program is four lines:

procedure Build();
var
    buffer : pointer int64;
begin
    buffer := new int64;     { allocation — creates an obligation }
    value buffer := 42;
end;                         { the exit releases nothing → does NOT compile }

Any one of four edits fixes it, and each produces a different, named outcome:

dispose buffer;                     { → manual-verified }
defer dispose buffer;               { → manual-verified, discharged on the exit edge }
buffer := new int64 until Build;    { → owner-bound }
Build := buffer;                    { return it → transferred }

◈ The four lifetime classes

Every allocation site is classified into exactly one of four classes — there is no “unknown”:

That last class is the honest core of the design. Where a pointer’s flow exceeds what the analysis can track precisely — it is address-taken, stored into an aggregate, shared across the static link, passed to a call, or cast — the site degrades to manual-unverified rather than the compiler guessing. The guarantee there is safety against silent failure, not absolute omission:

A leak of a fully-tracked allocation is inexpressible. Where tracking runs out, the discipline becomes a transparent, narrated manual one — the compiler tells you, in source order, exactly which sites it could not prove and why.

This is the resolution of region-based memory management’s historic weakness — opacity. Mica descends from Tofte and Talpin’s region calculus and the MLKit compiler, whose inference was sound but invisible; programmers could not see or correct its decisions. Mica makes every region a function the programmer names and sees, and makes every decision inspectable in the memory narration the compiler emits.

◈ The obligation analysis — SSA thinking, applied to lifetimes

The proof engine is a dedicated dataflow pass in the obligation package, run in every compilation mode. Formally it is “the same dataflow framework as classical liveness, dualized to a forward may-analysis over allocation values” — it tracks, for every name, the set of allocation sites it may hold plus a purity bit (true when the name provably holds exactly one tracked allocation on every path). An obligation is discharged only when the carrier it acts on is pure and single-site; any ambiguity degrades rather than guesses. A site still undischarged at a function’s exit, never degraded, is a reported leak.

It earned the right to be a hard error the safe way. The contract was staged: introduced first as a warning, then promoted to an error under an explicit compiler token, then made the default once the entire corpus and all examples compiled clean. Because the test harness fails any execution test on a warning, every run during the warning phase already rehearsed the final state — so the flip to a hard error was a one-line change in diagnostic severity, with zero churn.

The analysis carries the full machinery underneath: formal transfer functions, the soundness insights (a store through a pointer is not a redefinition of the pointer; an uncomputed predecessor is bottom, not empty), the leak predicate, and a direct relationship to SSA.

◈ Steering — the answer to opacity

When the default isn’t what you want, you correct it in source with one of four levers, and the memory narration confirms the result:

{ 1 · DEFAULT — owned by this function, reclaimed when it returns }
pixels := new Frame;
dispose pixels;                        { → manual-verified, plug-in: hosted-malloc }

{ 2 · STEER OUTWARD — "this must outlive me; it belongs to my caller Session" }
pixels := new Frame until Session;     { → owner-bound, plug-in: region }

{ 3 · STEER TO PROCESS LIFETIME — a cache as long-lived as the program }
cache := new Atlas until program;      { → owner 'program' }

{ 4 · STEER ACROSS THE CALL — hand the obligation to the caller }
function Make() : pointer Frame;
begin
    Make := new Frame;                 { → transferred }
end;

The compiler emits a memory narration — one line per memory-relevant site, in source order, naming the owner, the proven class, and the allocator it scheduled:

allocation line 28 col 14 in 'Inner':  new int64 (8 bytes), owner 'Worker', class owner-bound,       plug-in region
allocation line 34 col 10 in 'Worker': new int64 (8 bytes), owner 'Worker', class manual-unverified, plug-in hosted-malloc
defer      line 35 col  5 in 'Worker': cleanup runs on the exits of 'Worker'
allocation line 45 col 10 in 'program body': new int64 (8 bytes), owner 'program', class owner-bound, plug-in region

◈ How lifetimes are served — the plug-in seam

Proving a lifetime is one half; serving it is the other. Mica’s intermediate code never names malloc. It emits allocator intrinsics, and the compiler chooses which allocator serves each site from the lifetime class it proved:

Allocator selection is instruction selection.

Three allocators live behind one fixed symbol contract:

defer, owners, and regions all ride one runtime data structure — a per-owner singly-linked list, drained last-in-first-out at the owner’s exit, where each node is tagged as an owned cell, a deferred-cleanup marker, or a whole region. That is what keeps the runtime small enough to read in one sitting.

And it is a genuine plug-in. The deployment class (hosted vs fixed-arena) is a per-program link decision, never a source change, because code generation is byte-identical across classes. A third-party archive that honours the heap symbol contract links and runs with no change to the compiler — the seam, the single runtime data structure that backs defer, owners, and regions alike, and the three allocators all sit behind one fixed interface.

And it is fast. On an allocation-heavy workload the compiler-scheduled region allocator spends materially fewer instructions than per-cell allocation — and on amd64 it drops to 0.80× of gcc -O2’s retired-instruction count. The region out-counts glibc malloc/free on the workload it targets. The full benchmark story is Chapter 7.

◈ What is honest about this

The papers are candid, and so is this chapter. None of the following is a soundness hole — they are precision and ergonomics gaps with a plan for each:

• Containers are designed, the runtime half is in progress. Storing an owning pointer into a struct field or array element currently degrades to manual-unverified. The container rule — an owner-bound container absorbing its elements’ obligations, released in one typed drain — is being wired now (self-referential types and obligation absorption already work; the typed drain that releases the elements is the near-term next step).
• The precision floor is conservative. Address-taken, stored-into-aggregate, shared-across-static-link, passed-to-call, and cast all degrade. Real leaks behind those escapes are narrated, not yet caught. The trackable set widens incrementally, with measurement.
• The inbound half of transfer is not yet wired. A returned pointer is classified transferred, but the caller does not yet pick it up as a fresh obligation — so a returned pointer the caller silently drops can still leak in pure Mica today.
• No compiler-inserted dispose yet. The planned “static-GC clause” will insert a dispose at a single post-dominating point — never in a loop, never across an unproven alias. Today you resolve it with one keyword.
• Use-after-free is a runtime guarantee, not yet compile-time. Rust proves it in its safe fragment; Mica’s nil/dispose guards catch it at runtime in checked builds, and a compile-time post-dispose check is on the roadmap.

The stated position is deliberate: conservatism costs a keyword, never a miscompilation, and never a rejected correct program. A mechanized soundness proof of the tracked core — “the direct answer to where is your RustBelt” — is planned.

Where to next

You’ve seen what Mica compiles and how it manages memory. Now we open the hood and follow a program through the machine — from source text to a flat intermediate representation.

→ Chapter 4 — The Pipeline · back to the reading guide