docs / specification / Specification

5 — Ownership & the Borrow Checker

This chapter defines Cajeta’s ownership model — the owned and borrow states — and the static analysis that enforces it. Every heap value has one responsible owner. A plain = produces a borrow, a # on the source surrenders the title, and #= is a passthrough that hands along whatever title its source holds. All enforcement is at compile time, with no ownership annotations in the type system and no reference counting on the owned path.

5.1 Ownership States

A binding to a title-bearing value is in one of two states. The state is inferred, and it is never written in source.

The title is the ownership stake in a value, the right and the obligation to drop it. A borrow is a reference without the title.

One resolution operates beside the two states without adding a third. An escaping borrow of an immutable leaf buffer — a String produced by substring is the canonical case — resolves into a copy, or into a shared stake in the backing buffer. A stake is a property of the buffer, not of the binding. A runtime count co-owns the buffer, and the last stake frees it. The binding itself is a borrow. Stakes are specified in Arrays, Views, Slices & Records §12.

5.2 The Borrow Operator

= with a plain right side borrows. The title stays where it was, and the original owner drops the value when its scope ends. Three cases produce a borrow.

• A local from a local. T b = a makes b a borrow of a.
• A field or element read. T b = h.c makes b a borrow rooted at h with path c. Element reads borrow the same way.
• A plain call argument. f(a) lends a to the callee for the call. The caller keeps the title (§5.5).

Example 5.2-1. A local borrowing a local.

public final class C {
    public static int32 run() {
        int8[] a = heap int8[4];
        a[0] = (int8) 7;
        int8[] b = a;           // borrow — the title stays with a
        return (int32) b[0];    // 7
    }
}

Example 5.2-2. A field read, rooted at the holder.

public class Cell { public int32 v; public Cell(int32 v) { this.v = v; } }
public class Holder { public Cell c; public Holder() { this.c = heap Cell(7); } }
public final class C {
    public static int32 run() {
        Holder h = heap Holder();
        Cell b = h.c;           // borrow rooted at h, path c
        return b.v;             // 7
    }
}

Example 5.2-3. A plain argument lends. The caller still owns the buffer after the call.

public final class C {
    public static int32 peek(int8[] p) { return (int32) p[0]; }
    public static int32 run() {
        int8[] a = heap int8[4];
        a[0] = (int8) 7;
        int32 n = C.peek(a);
        return n + (int32) a[0];    // 14
    }
}

A borrow must not outlive its source. The compiler tracks each owner’s declaration site and scope end, and each borrow’s source. A borrow that may outlive its source is a compile-time error at the use site.

A borrow tracks its path from the named root, not only the variable it was read from. After String n = person.address.city, the borrow n is rooted at person with path address.city. Reassigning any link along that path — person.address #= x — invalidates everything derived from the link, and a subsequent use of n is a compile-time error.

Two further rules protect borrows.

• Anonymous owners. An owned temporary is a call receiver that nothing names and that holds a title. It is the result of a call declared #T, or a heap X(...) creator, used as the receiver of a further call. The temporary drops at the end of its statement. In the condition of an if, while, do or for, it drops right after the condition is evaluated, so a loop condition drops its temporary on every pass. A plain class, String, array or interface result that reaches the temporary through plain calls may be used within the statement. It may be passed as an argument, read or compared. Binding it to a local with = or #=, storing it in a field, or returning it is a compile-time error, CAJETA_ERROR_BORROW_OF_TEMPORARY, because the borrow would dangle. The check walks back through plain intermediate calls, so Doc.parse(t).self().title() is caught too. A #T result and a primitive result always pass. Binding the temporary itself to a name resolves the error, and so does calling a method that returns an owned copy.
• Alias mutation. A live borrow into a value blocks mutation of, or through, that value’s path. Iteration is a borrow construct, so mutating a collection inside its own for-each body is a compile-time error.

Example 5.2-4. A rejected program. title() returns a plain borrow that reaches the Doc temporary, and the local would outlive it.

public class Doc {
    String head;
    public Doc(String text) { this.head = "title: " + text; }
    public static #Doc parse(String text) { return heap Doc(text); }
    public String title() { return this.head; }
}
public final class C {
    public static int32 run() {
        String s = Doc.parse("intro").title();   // CAJETA_ERROR_BORROW_OF_TEMPORARY
        return (int32) s.byteLength();
    }
}

Example 5.2-5. The accepted shapes. The borrow is used inside its statement, the temporary is bound to a name, or the call returns an owned copy.

public class Doc {
    String head;
    public Doc(String text) { this.head = "title: " + text; }
    public static #Doc parse(String text) { return heap Doc(text); }
    public String title() { return this.head; }
    public #String titleCopy() { return "" + this.head; }
}
public final class C {
    public static int32 run() {
        int32 n = (int32) Doc.parse("intro").title().byteLength();   // used inside the statement
        Doc d #= Doc.parse("intro");
        String s = d.title();                                         // d owns the Doc to the block end
        String c #= Doc.parse("intro").titleCopy();                   // an owned copy
        return n + (int32) s.byteLength() + (int32) c.byteLength();   // 36
    }
}

Discussion. This is the full-expression rule of C++ and the check behind Rust’s E0716. Dropping the temporary at the end of the enclosing block would let the borrow live longer. It would also cost a drop-entry push and pop on every run of the block.

Discussion. An escaping borrow whose source is an eligible immutable leaf buffer does not error. It resolves into a copy or a shared stake (Arrays, Views, Slices & Records §12). The error-and-# discipline described in this chapter is the rule for identity objects and mutable values. At script top level, bindings live in the session scope, and a top-level borrow of a session binding is CAJETA_ERROR_SESSION_BORROW_ESCAPE (Script Units §18).

5.3 Transfers

A transfer moves the title from one binding to another. There is no transfer operator. The # prefix marks the surrender at the source, and it is written wherever the value is handed on.

• A store. a = #b gives a the title b held.
• A call argument. f(#b) gives the callee the title (§5.5).
• A return. return #b hands the title back to the caller (§5.5.2).

A signature can also require a transfer. A parameter declared #T accepts only a surrendered argument (§5.5.1), and a return declared #T promises the caller a title (§5.5.2).

After a transfer, the source is demoted to a borrow of the same instance. A previously owning variable remains valid, and reading through it stays legal. When it drops from scope it does not free the memory it once owned. That obligation traveled with the title, and only the new owner’s drop fires the destructor. Transferring it again is a compile-time error (§5.6).

A fresh heap T(...) expression in transfer position promotes implicitly, with no # written. The temporary is an unnamed owner with no prior identity (Allocation §4).

Example 5.3-1. A transfer at a store, then a read through the demoted source.

public final class C {
    public static int32 run() {
        int8[] a = heap int8[4];
        a[0] = (int8) 7;
        int8[] b = #a;          // b holds the title, a is demoted to a borrow
        return (int32) a[0];    // 7
    }
}

Example 5.3-2. A transfer at a call argument. The buffer’s title reaches the Sink, which outlives the call.

public final class Sink {
    int8[] held;
    public Sink(#int8[] b) { this.held #= b; }
    public int32 first() { return (int32) this.held[0]; }
}
public final class C {
    public static int32 run() {
        int8[] a = heap int8[4];
        a[0] = (int8) 7;
        Sink s = heap Sink(#a);
        return s.first();       // 7 — the buffer now belongs to s
    }
}

Example 5.3-3. A transfer at a return, through a #T signature. The result is received with #= (§5.5.2).

public final class C {
    public static #int8[] make() {
        int8[] out = heap int8[2];
        out[0] = (int8) 7;
        return #out;
    }
    public static int32 run() {
        int8[] q #= C.make();
        return (int32) q[0];    // 7
    }
}

Example 5.3-4. A rejected program. b is a borrow, so it holds no title to surrender (§5.6).

public final class C {
    public static int32 run() {
        int8[] a = heap int8[4];
        a[0] = (int8) 7;
        int8[] b = a;
        int8[] c = #b;          // CAJETA_ERROR_MOVE_OF_BORROW
        return (int32) c[0];
    }
}

Discussion. Transfer of stack-allocated values is TBD. The transfer machinery is being consolidated, and the semantics of # applied to a stack instance will be specified when that work lands. What holds today is that a #-return of a stack local is CAJETA_ERROR_STACK_RETURN_ESCAPES, and a plain return of a stack value copies into a caller-allocated slot (Allocation §4). Other stack-transfer shapes are unspecified here until the consolidation completes.

5.4 The Passthrough Operator

#= is a passthrough. It hands along whatever title its source actually holds — a transfer when the source owns, a borrow when it does not. #= is a single token, so an ownership store cannot be half-written. When the source owns, the store is a transfer and the source is demoted (§5.3). When the source is a borrow, the destination borrows and nothing is demoted.

A source holds no title in two ways, and #= forwards a borrow from either. A name that never owned — an alias, a field read, the result of a plain call — is one. A name demoted by an earlier transfer is the other. Neither has a title to give, so the destination borrows, nothing is demoted a second time, and the owner still drops the value exactly once. #= therefore never raises CAJETA_ERROR_MOVE_OF_BORROW. That diagnostic belongs to #v (§5.6), which asserts that its source holds a title to surrender.

The destination may be a local binding, a field, or an element. A field or element store records the arrived mode in the slot’s own ownership bit. A #T result is received the same way (§5.5.2), and a formal forwards its arrived mode through #= (§5.5).

Example 5.4-1. A passthrough into a local. The source owns, so the title moves.

public final class C {
    public static int32 run() {
        int8[] a = heap int8[4];
        a[0] = (int8) 7;
        int8[] b #= a;
        return (int32) b[0];    // 7
    }
}

Example 5.4-2. A passthrough into a field. The constructor’s parameter is a must-own edge, so the field records an owned slot.

public final class Sink {
    int8[] held;
    public Sink(#int8[] b) { this.held #= b; }
    public int32 first() { return (int32) this.held[0]; }
}
public final class C {
    public static int32 run() {
        int8[] a = heap int8[4];
        a[0] = (int8) 7;
        Sink s = heap Sink(#a);
        return s.first();       // 7
    }
}

Example 5.4-3. A passthrough into an element. The slot records the arrived mode.

public class Cell { public int32 v; public Cell(int32 v) { this.v = v; } }
public final class C {
    public static int32 run() {
        Cell[] arr = heap Cell[2];
        Cell c = heap Cell(7);
        arr[0] #= c;
        return arr[0].v;        // 7
    }
}

5.5 Calls and Mode Forwarding

The call site decides ownership. f(x) lends and f(#x) transfers. The callee is told what it got — every class-typed parameter and return carries a hidden per-call ownership flag, whose encoding is the Runtime & ABI companion’s concern — so a formal is a runtime owner, neither statically a borrow nor statically an owner, but whichever the caller made it. Its drop entry is armed from the flag on entry. A local initialized from a call arms from the return flag the same way.

Three consequences follow.

1. A surrendered argument the callee never consumes drops in the callee, on whatever exit the callee takes, including a throw.
2. A lent argument leaves the callee’s drop entry disarmed, and the caller still owns it.
3. #p on a formal — at a store, a forward, or a return — consumes the formal and passes the arrived mode on. A forwarding chain threads the original caller’s decision all the way down. A value lent into outer and forwarded with # to inner arrives at inner still lent, and nobody frees it.

This is what makes mode-forwarding wrappers expressible, and it is why the move-of-borrow check (§5.6) deliberately excludes plain formals.

Example 5.5-1. A mode-forwarding wrapper. keep forwards whichever mode arrived, and run transfers, so the buffer’s title reaches the Sink.

public final class Sink {
    int8[] held;
    public Sink(#int8[] b) { this.held #= b; }
    public int32 first() { return (int32) this.held[0]; }
}
public final class C {
    public static int32 keep(int8[] p) {
        Sink s = heap Sink(#p);   // forwards the arrived mode
        return s.first();
    }
    public static int32 run() {
        int8[] a = heap int8[4];
        a[0] = (int8) 7;
        return C.keep(#a);        // 7 — the caller surrendered the title
    }
}

5.5.1 Must-own parameters

A parameter type may be spelled #T. This is an opt-in must-own edge for a method that cannot function with a borrow, because it stores the value somewhere that outlives the call and has no way to cope with the caller keeping the title. Passing a plain argument at such an edge is a compile-time error. A #T formal owns its argument and frees it at return, so the store that keeps it is still spelled #= (§5.7).

Example 5.5-2. A #T parameter, satisfied by a transfer.

public final class C {
    public static int32 take(#int8[] p) { return (int32) p[0]; }
    public static int32 run() {
        int8[] a = heap int8[4];
        a[0] = (int8) 7;
        return C.take(#a);        // 7
    }
}

Example 5.5-3. A rejected program. A plain argument at a #T parameter.

public final class C {
    public static int32 f(#int8[] p) { return (int32) p[0]; }
}

int8[] a = heap int8[4];
a[0] = (int8) 5;
System.stdout.println(C.f(a));    // CAJETA_ERROR_TRANSFER_REQUIRED

Transfer mode is not part of a signature — dispatch erases # — so two declarations that differ only in mode collide. Declaring both f(Cell c) and f(#Cell c) is CAJETA_ERROR_TRANSFER_MODE_OVERLOAD. A plain formal already accepts both a lend and a transfer.

5.5.2 Returns

A plain return x hands back whatever title x held. A lent value stays lent, and an owned one transfers. return #x hands back the title.

A method may declare its return type #T, promising the caller a title. A #T result must be received with #=, which is what makes the acquisition visible at the call site without opening the callee. Binding it with a plain = is a compile-time error. A plain-T result binds with a plain = and carries whatever mode the callee’s frame held.

Example 5.5-4. A rejected program. A #T result bound with =.

public final class C {
    public static #int8[] make() {
        int8[] out = heap int8[2];
        out[0] = (int8) 3;
        return #out;
    }
}

int8[] q = C.make();    // CAJETA_ERROR_OWNED_RESULT_NEEDS_TRANSFER
System.stdout.println(q[0]);

The receiving local’s type never carries the marker. #Point q = … is a compile-time error (CAJETA_ERROR_TYPE_TRANSFER_RETIRED), because a local’s role comes from its initializer.

Discussion. Nothing in user code reads the per-call flag positionally, and the retired Cajeta.moveMask() accessor is rejected with CAJETA_ERROR_MOVEMASK_RETIRED. Code that branches on a formal’s arrived mode calls Cajeta.owned(formal). Ownership is never inferred from the body. A lend at a local’s last use is often a transfer the author did not spell, and the compiler advises (§5.10) rather than guesses, because the guess is wrong exactly where it matters — a value handed to a spawned task outlives the frame that appears finished with it.

5.5.3 Borrow-only parameters

A parameter type may be spelled ^T. The callee receives a borrow on every call, so a ^T formal carries no runtime ownership flag. A call site may pass a name, a field read or another borrow. Passing #x, a fresh heap value, an owned #T result or a + String is a compile-time error, CAJETA_ERROR_TRANSFER_INTO_BORROW_PARAM, because nothing would own the value after the call. Inside the callee, #p on a ^T formal is CAJETA_ERROR_MOVE_OF_BORROW. A plain argument or a #= store passes the formal on as a borrow.

An override must spell the same ^ marks as the method it overrides (CAJETA_ERROR_BORROW_MARK_MISMATCH), and a call through an interface or a virtual call is checked against the declared signature. ^ on a primitive or value-type formal is CAJETA_ERROR_BORROW_MARK_ON_VALUE, and on a varargs formal it is CAJETA_ERROR_BORROW_MARK_ON_VARARGS. ^ never marks a type-parameter declaration (class C<^K> is an error). A formal typed by a type parameter may be spelled ^K key, and the mark has no effect where K is instantiated with a primitive.

Example 5.5-5. A borrow-only formal kept in a field.

public class Cell { public int32 v; public Cell(int32 v) { this.v = v; } }
public final class Watcher {
    Cell seen;
    public Watcher(^Cell c) { this.seen = c; }      // the field borrows
    public int32 read() { return this.seen.v; }
}
public final class C {
    public static int32 run() {
        Cell c = heap Cell(7);
        Watcher w = heap Watcher(c);   // a lend; heap Watcher(#c) is rejected
        return w.read();               // 7
    }
}

5.6 Restrictions on Transfer

This section governs #, the transfer spelling. # asserts that its source holds a title to surrender, so the restriction is a single rule: you cannot transfer from a borrow. Applying # to a value the compiler can prove holds no title is a compile-time error, CAJETA_ERROR_MOVE_OF_BORROW.

A transferred source becomes a borrow, so a second transfer is the same rule seen twice, not a separate one:

T a = heap T();
T b = #a;      // valid   -- a holds the title, b takes it
T c = #a;      // rejected -- a is a borrow now

Lending reaches the same place by the other road. T b = a lends, so #b is a transfer from a borrow and is rejected for the identical reason.

What the compiler can PROVE holds no title is the limit of the rule. A local bound to a plain (non-#) call is not provably a borrow, because a plain return is runtime-conditional (§5.5.2) — it may well arrive carrying a title. T b = lend(a); T c = #b; therefore compiles, and whether it is correct is decided at run time.

None of this reaches #=. A passthrough asserts nothing and claims nothing, so from a titleless source it simply forwards a borrow (§5.4). b #= a followed by c #= a is a transfer followed by a borrow, and it compiles.

Plain formals are excluded deliberately. Their mode is a runtime fact fixed at the call site (§5.5), and rejecting #p statically would outlaw every mode-forwarding wrapper.

Example 5.6-1. A transfer from a borrow is rejected.

public class T { public int32 v; public T(int32 v) { this.v = v; } }
public final class C {
    public static int32 run() {
        T a = heap T(7);
        T b = #a;
        T c = #a;           // CAJETA_ERROR_MOVE_OF_BORROW
        return c.v;
    }
}

Example 5.6-2. The same shape spelled #= is legal. b takes the title, and c borrows what a has left.

public final class C {
    public static int32 run() {
        int8[] a = heap int8[4];
        a[0] = (int8) 7;
        int8[] b #= a;
        int8[] c #= a;
        return (int32) c[0];    // 7
    }
}

Discussion. At script top level the transfer check does not yet fire. The two transfers of Example 5.6-1, written as loose statements, compile today. The gap is recorded as disabled pinning tests in test/jit/SessionBindingTests.cpp, and this section governs once they pass.

5.7 Escapes and Retention

A plain store of a name and a plain argument lend. The rules below keep a lend from outliving its source, within the limit stated at the end of this section.

Keeping a value in a field. A store into a field, an element or a static outlives the call that makes it. The compiler checks each such store against the form of its source.

The same table governs an element store (this.items[i] = v) and a nested path (this.head.prev = v). A primitive or value-type source carries no title and may be stored with =. Spelling the formal #T does not make = safe, because a #T formal owns its argument and frees it at return. Each message names the spelling that fixes the store.

= never moves. An owned local stored with = is rejected even when no later statement reads it, so String w #= s.substring(1, 9); this.v = w; is an error and this.v #= w; is the fix.

Strings follow every rule in this section. A #= of an owned window moves the window and its shared stake on the root. A lent window stored with #= resolves to a copy up to 256 bytes, or to a shared stake on the root above that. Frame-arena bytes always copy when they escape. A String = into a field is a plain borrow and makes no copy. To keep your own String past its source, write this.v #= o.v.clone(). A String array slot follows the same rule: each slot carries its own title, so a[i] = s borrows and a[i] #= s takes the title or resolves a lent source.

Holders. A store into a field or element of a local, the holder, follows the same table when the holder escapes. A holder escapes when it is returned, passed with #, stored with #=, or stored into a field, an element, a static, or another holder that escapes or is not the frame’s own. A holder bound from a parameter, a field read or a call is not the frame’s own, so a store into it is always checked. A holder declared in an outer block that keeps an owned local declared in an inner block outlives that local, so the store is checked too. A holder bound in the frame that stays local is exempt.

Example 5.7-1. A kept formal stored with = is rejected.

public final class Holder {
    int8[] f;
    public Holder() { this.f = heap int8[1]; }
    public void set(int8[] v) {
        this.f = v;           // CAJETA_ERROR_KEEP_NEEDS_SHARP_STORE
    }
}

Example 5.7-2. The two correct spellings. set lets the caller choose, and watch only ever borrows.

public final class Keeper {
    int8[] f;
    int8[] g;
    public Keeper() { this.f = heap int8[1]; this.g = heap int8[1]; }
    public void set(int8[] v) { this.f #= v; }       // set(a) lends, set(#a) transfers
    public void watch(^int8[] v) { this.g = v; }     // a borrow on every call
}

Example 5.7-3. An escaping holder that keeps an owned local with = is rejected under the holder rule. h.c #= s gives the holder the title.

public class Cell { public int32 v; public Cell(int32 v) { this.v = v; } }
public class Holder {
    public Cell c;
    public Holder() { this.c = heap Cell(0); }
}
public final class C {
    public static #Holder build() {
        Holder h = heap Holder();
        Cell s = heap Cell(5);
        h.c = s;              // CAJETA_ERROR_KEEP_NEEDS_SHARP_STORE: h escapes
        return #h;
    }
}

Dangling lend. When a method lends one of its own owned locals to a holder local through a call that retains it, and then returns the holder, the return is a compile-time error, CAJETA_ERROR_DANGLING_LEND. The holder would leave holding a pointer to a local that is about to drop. The check is intra-procedural and single-hop. It fires only when the callee actually retains, because a method that merely reads its argument cannot strand anything. The fix is to say what was meant. h.keep(#s) gives the holder the title.

Example 5.7-4. A dangling lend through a retaining call is rejected.

public class Cell { public int32 v; public Cell(int32 v) { this.v = v; } }
public class Holder {
    public Cell c;
    public Holder() { this.c = heap Cell(0); }
    public void keep(Cell v) { this.c #= v; }
}
public final class C {
    public static #Holder build() {
        Holder h = heap Holder();
        Cell s = heap Cell(5);
        h.keep(s);            // lend, the title stays with s
        return #h;            // CAJETA_ERROR_DANGLING_LEND: s drops at }
    }
}

Not checked. A caller that lends x to a holder that outlives x in any other way is not caught. The lend may reach the holder through a ^T formal, or through a retaining call whose holder is not returned by the method that owns x. Catching it needs lifetime information the language does not track. When the holder must outlive the value, transfer it with #x.

A sibling field alias is not checked either. this.a = this.b stores a legal borrow of a field read. Replacing this.b afterwards frees the value this.a points at, and the compiler does not track that.

5.8 Field Ownership and the Live-Set Claim

A field’s ownership status is resolved at drop time, not at declaration. p.field #= x and p.field = heap T(...) make the field an owner. p.field = y, where y is a borrow, stores the borrow, and the field aliases y’s source.

Every heap allocation is registered in a global live set. When an owner drops, the synthesized drop body offers each owned-shape field to its drop dispatcher, and the dispatcher makes an atomic claim — remove-if-present — on the field’s address. The first claimant frees the value and runs its destructor. Every later claimant for the same address, whether the owning local’s own drop or another field aliasing it, finds it gone and does nothing. The claim is what keeps aliased fields from double-freeing without reference counts.

Discussion. A use after free through an aliased field whose source has already dropped is the programmer’s responsibility in v1. A static lifetime tracker for that case is planned but not implemented.

5.9 Drops Under Transfer

Transfer moves the obligation to drop. When # passes a title, the source’s drop entry is deactivated and the destination’s is armed. Each instance’s destructor runs exactly once, when the drop chain reaches whichever entry ends up owning it. Drop entries fire at the closing brace of the declaring lexical block, in reverse declaration order, on both the normal and the exceptional path (Allocation §4). Destructor declaration and dispatch are specified in Classes §8.

5.10 Advisories

Lending a local at its final use is suspect. Nothing in the scope reads it again, so the lend is usually a transfer the author did not spell. The compiler reports CAJETA_WARN_LAST_USE_TRANSFER with a # fixit and continues. A later read of the local suppresses the warning. So does a use inside a loop, and so does spelling #x.

Source: docs/specification/05-ownership-borrow-checker.md · 17 min · 3799 words