Resources and linearity

Some values stand for something outside your program's memory. A file descriptor is the small integer the operating system gives you for an open file or socket; the OS keeps a table entry for it until you close it, and a process that keeps opening files without closing them eventually runs out. A lock must be released, or every other thread waiting for it hangs. A database transaction must be committed or rolled back. All of these come with an obligation. In C that obligation lives in a comment. In C++ and Rust a destructor, a function the compiler calls automatically when a value goes out of scope, discharges it invisibly. kola does neither. Such values are declared as linear resources, and the compiler requires every resource to be consumed exactly once on every execution path. Forgetting to close something is a compile error. There are no implicit destructors: cleanup is an ordinary function call that you can see in the source.

How a resource differs from a struct

The syntax differs by one word, resource struct instead of struct. The rules for handling the value are what change:

For data, let b = a; makes a second copy and both stay usable. For a resource, the same line transfers ownership: the value is now called b, and any later use of a is a compile error. A copy cannot exist, because two owners of one file would close it twice. The same move happens at every by-value position, not only in let: a function argument, a struct field in a literal, Some(v), a returned value, a message sent on a channel.

A first resource

The running example is a write-ahead log, a file a database appends records to before applying them, so that it can recover after a crash. Ours must be sealed when you are done with it. Hover over the highlighted parts:

use std::log;

resource struct Wal { entries: u32 }

impl Wal {
    pub fn open() -> Wal !{} {
        Wal { entries: 0 }
    }

    pub fn append(self: &mut Wal) !{} {
        self.entries = self.entries + 1;
    }

    pub fn seal(self: Wal) !{log} {
        log::info(f"sealed after {self.entries} entries");
        let Wal { entries: _ } = self;
    }
}

fn main() -> u8 !{log} {
    let mut wal = Wal::open();
    wal.append();
    wal.append();
    log::info(f"entries so far: {wal.entries}");
    wal.append();
    wal.seal();
    0
}

seal takes no capability argument: a handle carries its own reach. Logging needs nothing either, since log is an effect rather than a resource (see Effects and capabilities).

Delete wal.seal(); and the compiler points at the declaration:

error[card §2]: resource `wal` is not consumed on this path
  --> wal.kl:21:5
    |
 21 |     let mut wal = Wal::open();
    |     ^^^
    = help: no implicit destructors: move it on, return it, destructure it, or pass it to a consuming fn

Destructuring

In let Wal { entries: _ } = self; the left side is a pattern with the shape of a Wal; entries: _ discards that field, and entries: n would keep it. Once the pattern matches, the resource is gone. This is the body of a destructor, written out where you can see it.

Every field must be named; there is no .. for "the rest". When you add a field to a struct later, the compiler then points at every destructuring site that needs a decision about it. Here a consuming commit takes a transaction apart, discards one field and returns the other:

resource struct Txn { id: u64, writes: u32 }

impl Txn {
    pub fn begin(id: u64) -> Txn !{} { Txn { id: id, writes: 0 } }
    pub fn record(self: &mut Txn) !{} { self.writes = self.writes +% 1; }
    pub fn commit(self: Txn) -> u32 !{} {
        let Txn { id: _, writes: w } = self;
        w
    }
}

test destructure_binds_a_field {
    let mut t = Txn::begin(42);
    t.record();
    t.record();
    t.record();
    let n = t.commit();           // consumes t, returns the write count
    assert n == 3;
}

Leave out a field and the pattern is refused:

error[card §2]: struct pattern misses field `id`
  --> txn.kl:6:9
   |
 6 |         let Txn { writes: w } = self;
   |         ^^^
   = help: destructuring consumes the whole value; name every field (use `_`)

There are four ways to consume a resource: pass it to a consuming function (wal.seal()), return it, move it on (let archived = wal; or into a struct, a channel, another function), or destructure it. One of them must happen exactly once on every path through the function, including early returns and every match arm. The compiler rejects both the forgotten case and the doubled one.

? is an early return

"Every path" includes paths you did not write out. The ? operator (see Contracts, traps, and tests) is a hidden return Err(...), so a resource that is live at a ? would be lost on the error branch. The checker reports it and says where the resource was declared:

error[card §2]: `?` returns early on Err while resource `w` is live — the Err path would leak it
  --> ingest.kl:10:13
    |
 10 |     let v = step(b)?;
    |             ^^^^^^^^
    = help: consume `w` before the `?`, or handle the Result with an explicit `match`
    = note: `w` was declared here (ingest.kl:9:5)

Either finish with the resource before the fallible call, or write the match out, which makes you say what happens to the resource on each side:

use std::log;

resource struct Wal { entries: u32 }

impl Wal {
    pub fn open() -> Wal !{} { Wal { entries: 0 } }
    pub fn append(self: &mut Wal) !{} { self.entries = self.entries + 1; }
    pub fn seal(self: Wal) !{log} {
        log::info(f"sealed after {self.entries} entries");
        let Wal { entries: _ } = self;
    }
    pub fn discard(self: Wal) !{} { let Wal { entries: _ } = self; }
}

enum ParseErr { Short }

fn parse_len(b: &[u8]) -> Result[u32, ParseErr] !{} {
    if b.len == 0 { return Err(ParseErr::Short); }
    Ok(widen[u32](b[0]))
}

fn ingest(b: &[u8]) -> Result[u32, ParseErr] !{log} {
    let n = parse_len(b)?;       // no resource is live yet: fine
    let mut w = Wal::open();
    w.append();
    match parse_len(b) {         // a `?` here would be refused: `w` is live
        Ok(v) => { w.seal(); Ok(n +% v) }
        Err(e) => { w.discard(); Err(e) }
    }
}

test question_mark_and_linearity {
    let good = ingest(&b"\x05");
    assert good == Ok(10u32);
    let bad = ingest(&b"");
    assert bad == Err(ParseErr::Short);
}

lend: a view you can store

Ordinary access needs nothing special: reading a field (wal.entries) or calling a method (wal.append()) borrows the resource for that expression or call. lend is for the case where you need a region reference &r Wal, typically to store views of several resources in a region data structure or to pass one to a function that keeps references. let v: &r Wal = lend wal in r; freezes wal until the region closes. Until then wal can be neither modified nor consumed:

error[card §4]: `a` is frozen by a `lend` until its region closes
  --> lend.kl:11:9
    |
 11 |         a.append();
    |         ^

The view is read-only; there is no lend mut. When the region closes, the freeze lifts and the owner can be modified and consumed again. Lending the same resource into the same region twice is allowed. A lend never counts as consuming the resource, so the obligation is still there when the region closes.

Here views of two logs are collected in a region vector. Call-scoped references would not work, because the vector stores them:

resource struct Wal { entries: u32 }

impl Wal {
    pub fn open() -> Wal !{} { Wal { entries: 0 } }
    pub fn append(self: &mut Wal) !{} { self.entries = self.entries + 1; }
    pub fn discard(self: Wal) !{} { let Wal { entries: _ } = self; }
}

test lend_into_a_structure {
    let mut a = Wal::open();
    a.append();
    let mut b = Wal::open();
    b.append();
    b.append();

    region r {
        let views: &r mut Vec[&r Wal] = alloc in r mut Vec::new();
        views.push(lend a in r);     // a and b are frozen from here
        views.push(lend b in r);

        let mut total: u32 = 0;
        for i in 0..views.len {
            total = total +% views[i].entries;
        }
        assert total == 3;
    }
    a.discard();                     // the region is closed: a is usable again
    b.discard();
}

Shadowing a live resource

Rebinding a name with a second let is legal for data, as in Rust. A live resource cannot be hidden that way, since that would leak it with one innocent-looking line:

resource struct Wal { entries: u32 }

impl Wal {
    pub fn open() -> Wal !{} { Wal { entries: 0 } }
    pub fn discard(self: Wal) !{} { let Wal { entries: _ } = self; }
}

test shadowing_a_live_resource {
    let wal = Wal::open();
    let wal = Wal::open();   // the first Wal is still live
    wal.discard();
}

The compiler reports resource `wal` is not consumed on this path at the first let. Consume the first value, then reuse the name.

Optional resources

A resource often sits in a slot that is sometimes empty: a worker you have not started yet, a connection that may or may not be open. The slot is an Option, and linearity tracks what it holds. An Option holding None owes nothing at an exit, and assigning into it drops nothing, so filling an empty slot is ordinary code. Some(resource) carries the obligation, and a match discharges it on both arms. Overwriting a slot that really does hold a resource is still refused, and so is a loop that refills a slot on every pass without emptying it first, which would leak one resource per iteration.

To move a value out of a slot you can write to (a &mut Option[T], a field of a &mut struct, an element of a &mut Vec), use take(), which returns the value and leaves None behind:

resource struct Wal { entries: u32 }

impl Wal {
    pub fn open() -> Wal !{} { Wal { entries: 0 } }
    pub fn discard(self: Wal) !{} { let Wal { entries: _ } = self; }
}

// Empty the slot if it holds something, leaving None behind.
fn retire(slot: &mut Option[Wal]) -> bool !{} {
    match slot.take() {
        Some(w) => { w.discard(); true }
        None => false,
    }
}

test an_empty_slot_owes_nothing {
    let mut slot: Option[Wal] = None;     // holds nothing, owes nothing
    slot = Some(Wal::open());             // now it owes one consumption
    let retired = retire(&mut slot);
    assert retired;
    match slot {                          // the checker does not know slot is
        Some(w) => { w.discard(); }       // None now, so the exit still matches
        None => {}
    }
}

Invariants

An invariant is a condition that holds for every value of a type for as long as the value exists: a counter never exceeds 100, a ring's head stays below its size. Without language support such conditions live in comments, and every function either trusts them or checks them again. A resource struct declares them as the last item of its body:

resource struct Counter { n: u32, inv n <= 100 }

impl Counter {
    pub fn bump(self: &mut Counter) !{} {
        self.n = self.n + 1;
    }
    pub fn done(self: Counter) -> u32 !{} {
        let Counter { n } = self;
        n
    }
}

test invariant_holds {
    let mut c = Counter { n: 0 };
    c.bump();
    c.bump();
    let total = c.done();    // bind first: an assert may not consume or mutate
    assert total == 2;
}

Constructing Counter { n: 200 } traps at the construction site with inv violated on `Counter`. Any function that receives a Counter can therefore rely on n <= 100 without checking, because no other Counter can exist. Invariants follow the same rules as other contracts: proven at compile time where possible, checked at run time otherwise.

Resources and domain

A trap is kola's response to a broken assumption, such as an overflow, an index out of bounds or a failed contract: execution stops at that point, with no unwinding. A trap normally ends the whole process. A domain limits it to one block, domain d { work(); } recover(t: Trap) { ... }, so a server can lose a request instead of the server. Traps belong to Contracts, traps, and tests; they appear here because a domain interacts with linearity.

A trap leaves the block from the middle. A resource that was live at that moment would have no consumption on that path, and the compiler could no longer promise "exactly once". So a linear value may be neither declared nor used inside a domain's body or its recover arm. Authority tokens (below) are exempt, since dropping one loses nothing. If a resource is still live inside a callee when the trap fires, the trap is fatal and no domain catches it.

error[card §3]: `w`: a linear resource may not live inside a `domain` — a trap would strand it
  --> worker.kl:9:9
   |
 9 |         let w = Wal::open();
   |         ^^^
   = help: domains compute over data; move this resource outside the domain, or consume it before entering

The shape that works keeps the resource outside, and the domain computes over plain data:

use std::log;

fn checked_div(a: u32, b: u32) -> u32 !{log} {
    let mut out: u32 = 0;
    domain d {
        out = a / b;             // traps when b == 0
    } recover(t: Trap) {
        let k = t.kind;          // Bounds, Arith, Req, Ens, Inv, Assert, ...
        let site = t.site;       // "module:line"
        log::warn(f"recovered {k} at {site}");
        out = 0;
    }
    out
}

test domain_bounds_the_trap {
    assert checked_div(10, 2) == 5;
    assert checked_div(10, 0) == 0;    // trapped, recovered, still running
}

Which built-in values must be consumed

Linearity is not only for types you declare. The whole capability system is built on it (see Effects and capabilities), and so is every OS handle the standard library gives you. Not all of them carry the same obligation, and the difference follows one rule: whether the value owns something.

• Authority tokens can be dropped. Clock, Rng, Fs, Dir, DirRo, Dial, Listen, Stdout, Stdin, Args, Env, Tty, Ping, Proc, Mmio and its windows, Cpu, Dev, Window, and Sys itself. There is no quantity to reconcile and nothing to release, so dropping one loses nothing and the runtime reclaims it. A token still moves rather than copies; to give a worker its own, you attenuate it (clock.split(), dir.ro()).

• Mem must be returned. It is the one metered quantity. sys.mem.split(n) carves off a memory budget and sys.mem.absorb(sub) gives it back; dropping it in between would lose that budget for the rest of the program. Forget the absorb and you get the familiar resource `small` is not consumed on this path at compile time.

• Linear handles must be closed. They hold a real OS object or key material, so dropping one leaks something. These are the ones you will meet most: File, Tmp, Sealed, FsNode (files); Listener, Conn, UdpSock, Poller (network); Thread, Tx, Rx (threads and channels); Child, ChildIn, ChildOut (processes); Device (a device node); Secret (dropping it would leave key material unwiped); RawMode (dropping it would leave the terminal in raw mode). The GUI and packet-socket handles follow the same rule.

A capability is strict because it owns something, not because it is powerful. Clock is broad authority and costs nothing to drop; a single File is narrow authority and must be closed. For the same reason the names of built-in linear handles are reserved: struct Thread { ... } or struct Conn { ... } is refused, because spawn hands you a Thread without your ever writing the type name, and a look-alike type could slip a live handle out of linearity. The one exception to "consume everything yourself" is the root bundle: whatever is left in sys when main returns (or in sim when a test ends) is reclaimed by the runtime.

The normative reference is SPEC-CARD §2 and §7 (kola help spec-card).