Bare metal: device nodes, freestanding builds, and layout claims

kola was built for a stack with no operating system under it: a hypervisor, a filesystem, a router on a MIPS board. A C ABI and a bare-metal target are therefore part of the language's reason to exist. This chapter covers the two directions that pulls in. One is reaching a device through an OS, with Dev, the userspace char-device capability. The other is shipping where there is no OS at all: kola build --freestanding, a static arena instead of malloc, and an object whose list of undefined symbols tells you what the program can still fail at. Between them sits layout_assert, which lets you state a struct's C layout and have the C compiler check it.

Granted MMIO and RAM windows are covered in Hardware: granted windows and typed device access, and the Cpu intrinsics and SMP atomics in The machine: CPU, ordering and atomics. This chapter refers to them where they meet.

Dev: a device node is a peer, not a window

On Linux and other Unix systems, a driver usually shows itself to ordinary programs as a device node: a special file such as /dev/widget. A program opens it like a file, which gives it a file descriptor (a small integer the kernel uses to identify the open handle). It then talks to the driver with ioctl calls, each a numbered request with a small buffer of arguments, and may ask for mmap, which maps a page of the driver's memory straight into the program's address space. Suppose a userspace daemon needs to talk to a kernel module through /dev/widget. kola already has a capability for hardware, Mmio (memory-mapped I/O: device registers that the CPU reads and writes as if they were memory), which hands out three kinds of window (MmioWindow, RamWindow, IoWindow). It would be easy to add a fourth. kola does not, for two reasons.

The first is what a capability is for: answering an audit question. If Mmio also covered opening device nodes, a manifest line reading Mmio could no longer tell a bare-metal driver touching UART registers apart from a daemon that opens nodes and issues ioctls. A reviewer would learn something false from it in both directions.

The second is the nature of the thing. A window is a granted address range. Nothing can fail at grant time and there is nobody on the other side. A device node has a lifecycle and a protocol: open can fail, an ioctl is a request a driver may refuse, and that driver has its own state machine. That is much closer to a network connection than to a range of memory. The mapped page is the one part that resembles a window, and it arrives through the protocol. Fs is wrong for a similar reason: /dev/widget is an absolute path outside every sandbox root, and ioctl and mmap are not file operations.

So sys.dev: Dev is its own capability. It is an authority token, so it may be dropped on any path. A Device is a linear handle, meaning it must be used up exactly once on every path through the program (here, by close), because it owns a file descriptor and the rules from Resources and linearity apply to it unchanged.

The basic surface

impl Dev {
    // A grant lookup: an unknown name is None, never an error.
    fn open(self: &Dev, name: &[u8]) -> Option[Device] !{io}
    // The mount door: a Result, because a missing mount and a refused mint
    // are different failures with different repairs.
    fn mint(self: &Dev, name: &[u8]) -> Result[Device, (DevErr, OsErr)] !{io}
}

impl Device {                                  // linear: it owns an fd
    fn ioctl_read(self: &mut Device, code: u32, out: &mut [u8])
        -> Result[usize, (DevErr, OsErr)] !{io}
    fn map_ro(self: &mut Device) -> Result[RamWindowRo, (DevErr, OsErr)] !{io}
    fn close(self: Device) !{io}               // consumes
}

Like every operation that reaches the OS, a fallible device op answers Result[T, (DevErr, OsErr)]: you branch on the DevErr and print the OsErr (with use std::os;, os.name() gives its canonical name).

open answers None for an unknown name, and also for a granted node that is not there. From the program's point of view those are the same fact: it does not have this device.
ioctl_read issues one read-direction ioctl. The allowlist belongs to the grant, not to the program: a code that is not on it is Err((DevErr::Denied, _)), checked before the device is touched. The runtime also checks what the code itself declares. A declared size larger than out, or a code whose direction is write-only, is refused with Denied before the syscall, because the allowlist picks the code but the program picks the buffer.
map_ro takes one read-only mapping of the granted length, held for the life of the handle. A second call is AlreadyMapped.

The DevErr variants are split by what the caller should do next. Unavailable means the thing behind the node is not live (ENODEV, ENXIO); a gateway uses it to decide whether to serve at all. IoFailed is transient: your state stands, retry. WouldBlock means nothing yet: your state stands, poll. Stale means your state is invalid and retrying can never succeed; discard the position and re-establish. ESTALE and EIO look alike as numbers, but treating one as the other turns a retry into a false acknowledgement of durability. The remaining variants (Denied, AlreadyMapped, Busy, Interrupted, ReadOnly, Invalid, NoSpace) mean what their names say.

mint is a second way to get a Device: out of a granted mount rather than a node. The operator binds --dev-mint vol0=/mnt/data:mint=0x80384b01:map=4096, a mount path plus the one ioctl code that turns a path descriptor into a handle, and sys.dev.mint(b"vol0") performs open, ioctl and close inside the runtime. The intermediate path descriptor is never a kola value, so the program cannot hold it and pin the mount. The minted Device has the same operations. The mint verb is bound to the grant and never available on a handle: an ioctl that returns an arbitrary descriptor would launder authority past the audit, so the compiler refuses it.

fn launder(d: &mut Device) !{io} {
    let x = d.mint(0x1234u32);
}

$ kola check launder.kl
error[card §7]: `mint` is bound to the GRANT, never free on a `Device` handle
  --> launder.kl:2:13

The help line that follows points at the --dev-mint grant as the repair. A name is one kind of grant or the other: open does not see a mount and mint does not see a node.

map_ro returns the ordinary read-only window

A device often publishes its status in a shared page that the driver may be rewriting while you read it. The usual protocol is a seqlock: the writer bumps a sequence number to an odd value before it writes and to an even value after, and a reader copies the data, then checks that the number was even and unchanged; if not, it retries. A device that publishes a status page therefore needs a seqlock reader, and the obvious design is a device-specific window type with its own reader. kola does not have one. RamWindow has a read-only twin, RamWindowRo, which you can make from any RAM window by attenuation, that is, by deriving a weaker capability from one you hold (w.ro(), no grant needed), and map_ro returns exactly that type. The seqlock reader over a device's status page is therefore the same snapshot used over a network card's descriptor ring (the shared queue in which the card and the driver exchange buffer addresses).

RamWindowRo is RamWindow without its write half. It has the read* ops, copy_out, .len and snapshot; write*, copy_in, zero and the DMA ops do not exist on it. A device reader that tries to write does not get past the checker:

fn poke(w: &RamWindowRo) !{io}
    req w.len >= 8usize
{
    w.write32(0usize, 1u32);
}

$ kola check poke.kl
error[card §7]: `RamWindowRo` is the READ-ONLY half of a RAM window — `write32` writes, and the write half does not exist on this type
  --> poke.kl:4:5

Grants and models

A node is granted the way a filesystem root is: the operator binds a name to a path, the program asks for the name, and the path never appears in the program.

kola run gw.kl \
    --device widget=/dev/widget:map=32:ioctl=0x80384b01 \
    --sim-dev widget=gw

# the same grant as environment variables, for a unit file or a container
KOLA_DEVICE_widget=/dev/widget:map=32:ioctl=0x80384b01
KOLA_SIM_DEV_widget=gw

map=LEN is the mappable length. ioctl=CODE may be repeated, and the list is the allowlist. Taken together over a shipped image, the grants say exactly which device nodes the program opens and which ioctl codes it may issue.

The --sim-dev binding decides which world the program runs against. With a model bound, the device is that model, under run and test alike. Without one, kola run and kola run --native open the real device: a real open, a real allowlisted ioctl, a real mmap. Under kola test a grant without a model is refused at startup, because a real ioctl would read the host:

$ kola test --interp t.kl --device widget=/dev/widget:map=32:ioctl=0x80384b01
error[card §7]: device `widget` is granted but has no model binding — a TEST backs a device node with a SimDevice model, because a real ioctl would read the host

A plain memory window needs no model, since plain memory is its own model. A device does, because ioctl and mmap semantics are defined by the device. The model is a set of pure functions over a state struct you define, one per operation, named after the prefix you bind:

p_new() -> M
p_attach(m: &mut M, now: u64) -> bool: did the node open? false makes open answer None.
p_ioctl(m: &mut M, code: u32, out: &mut [u8], now: u64) -> Result[usize, DevErr]
p_map(m: &mut M, now: u64) -> Result[(), DevErr]: did the mapping succeed?
p_page(m: &mut M, off: usize, dst: &mut [u8], now: u64): every read of the mapped page pulls through this.
p_mint(m: &mut M, code: u32, now: u64) -> Result[(), DevErr], for a mint grant only. The compiler refuses a mint grant whose model lacks it and a node grant whose model has it.

All of them are !{}. Writer, stream and TUN grants add callbacks of their own, listed in STD-CARD.

Three rules shape these models. now is a parameter, never a Clock inside the model, so determinism belongs to the caller. A model names its outcome as a DevErr and never returns an errno, because a model is portable kola and errno values differ by host (ESTALE is 116 on Linux and 70 on macOS); the executor adds OsErr::Other. And every operation that can fail has its own model function. An operation with no model function is one that cannot fail in simulation, which is why p_map exists: without it, a device the model had already declared gone could still hand out a fresh mapping.

A gateway, end to end

Here is the whole shape in one file: a model that publishes a status page, and a gateway that checks it before serving. The model answers with an odd sequence word on the first page pull, which means a publish is in progress, so the seqlock read has to retry once.

use std::log;

// ---- the model: pure fns over your own state struct
struct Gw { pulls: u64, probes: u64 }

fn gw_new() -> Gw !{} { Gw { pulls: 0, probes: 0 } }

// Did the node open? `false` makes `sys.dev.open` answer `None`.
fn gw_attach(m: &mut Gw, now: u64) -> bool !{} { true }

// The liveness probe: live on the first call, gone after that.
fn gw_ioctl(m: &mut Gw, code: u32, out: &mut [u8], now: u64) -> Result[usize, DevErr] !{} {
    m.probes = m.probes + 1;
    if m.probes > 1 { return Err(DevErr::Unavailable); }
    for i in 0..out.len { out[i] = 1u8; }
    Ok(out.len)
}

// Did the mapping succeed?
fn gw_map(m: &mut Gw, now: u64) -> Result[(), DevErr] !{} {
    if m.probes > 1 { Err(DevErr::Unavailable) } else { Ok(()) }
}

// The page as little-endian 8-byte words: 0 seq, 8 magic | mounted << 32, 16 fenced.
// The sequence word is odd on the first pull (a publish in progress), even after.
fn gw_word(pulls: u64, base: usize) -> u64 !{} {
    if base == 0 {
        if pulls == 1 { 1 } else { 2 }
    } else if base == 8 {
        0x4b4f5246u64 | (1u64 << 32)
    } else {
        0
    }
}

fn gw_page(m: &mut Gw, off: usize, dst: &mut [u8], now: u64) !{} {
    m.pulls = m.pulls + 1;
    for i in 0..dst.len {
        let a = off + i;
        let w = gw_word(m.pulls, a - a % 8);
        dst[i] = wrap[u8](w >> widen[u64]((a % 8) * 8));
    }
}

// ---- the gateway
fn read_status(ro: &RamWindowRo, dst: &mut [u8]) -> bool !{io}
    req ro.len >= 32usize
    req dst.len == 12usize
{
    ro.snapshot(0usize, 8usize, dst)
}

fn le32(b: &[u8], i: usize) -> u32 !{}
    req i + 4 <= b.len
{
    widen[u32](b[i]) | (widen[u32](b[i + 1]) << 8) | (widen[u32](b[i + 2]) << 16) | (widen[u32](b[i + 3]) << 24)
}

fn main(sys: Sys) -> u8 !{io, log} {
    let mut dev = match sys.dev.open(b"widget") {
        None => { log::info("no widget node: serving nothing"); return 1; }
        Some(d) => d,
    };
    let mut junk = [0u8; 8];
    match dev.ioctl_read(0xdeadu32, &mut junk) {
        Err((DevErr::Denied, _)) => log::info("undeclared code: Denied"),
        _ => log::error("an undeclared code reached the device"),
    }
    let mut probe = [0u8; 8];
    match dev.ioctl_read(0x80384b01u32, &mut probe) {
        Ok(n) => log::info(f"attach probe n={n}"),
        Err(_) => { log::info("mount is gone"); dev.close(); return 2; }
    }
    match dev.map_ro() {
        Err(_) => { log::info("map_ro failed"); dev.close(); 3 }
        Ok(ro) => {
            let mut hdr = [0u8; 12];
            let ok = read_status(&ro, &mut hdr);
            let magic = le32(&hdr, 0);
            let mounted = le32(&hdr, 4);
            let fenced = le32(&hdr, 8);
            log::info(f"ok={ok} magic={magic} mounted={mounted} fenced={fenced}");
            dev.close();
            0
        }
    }
}

$ kola run gw.kl --device widget=/dev/widget:map=32:ioctl=0x80384b01 --sim-dev widget=gw
[info] undeclared code: Denied
[info] attach probe n=8
[info] ok=true magic=1263489606 mounted=1 fenced=0

$ kola run --native gw.kl --device widget=/dev/widget:map=32:ioctl=0x80384b01 --sim-dev widget=gw
[info] undeclared code: Denied
[info] attach probe n=8
[info] ok=true magic=1263489606 mounted=1 fenced=0

$ kola run gw.kl                       # no grant at all
[info] no widget node: serving nothing

The two runs are a real comparison. The C backend compiles the model functions into the native program and calls them directly, so both executors run the same state machine. Keep in mind what such a comparison can and cannot show. If a bug sits on both sides, for example both executors skipping the retry, the outputs still match. The reference program in the repository (golden/dev-widget.kl) catches that by publishing the model's own pull counter in the page and comparing it against a fixed value. A model that counts its own calls is a cheap way to make a differential test see behaviour, not only values. More generally, a simulated device proves the driver's logic: attach order, gating policy, retry discipline. Only a run against a real /dev node proves the ioctl encoding, the real mapping and the real memory ordering.

Because grants are command-line flags, a test file run with no flags can only exercise the pure model functions directly. The driver itself needs a run that supplies the grants. If you write a device driver, expect that split.

The mount door looks the same, with the sixth model function:

use std::log;
use std::os;

struct Vol { minted: bool }

fn vol_new() -> Vol !{} { Vol { minted: false } }
fn vol_attach(m: &mut Vol, now: u64) -> bool !{} { true }

// The sixth fn, for a mint grant: did the filesystem hand over a handle?
fn vol_mint(m: &mut Vol, code: u32, now: u64) -> Result[(), DevErr] !{} {
    if code != 0x80384b01u32 { return Err(DevErr::Denied); }
    m.minted = true;
    Ok(())
}

fn vol_ioctl(m: &mut Vol, code: u32, out: &mut [u8], now: u64) -> Result[usize, DevErr] !{} {
    if !m.minted { return Err(DevErr::Unavailable); }
    for i in 0..out.len { out[i] = 7u8; }
    Ok(out.len)
}

fn vol_map(m: &mut Vol, now: u64) -> Result[(), DevErr] !{} {
    if m.minted { Ok(()) } else { Err(DevErr::Unavailable) }
}

fn vol_page(m: &mut Vol, off: usize, dst: &mut [u8], now: u64) !{} {
    for i in 0..dst.len { dst[i] = 0u8; }
}

fn main(sys: Sys) -> u8 !{io, log} {
    match sys.dev.mint(b"vol0") {
        Ok(d) => {
            let mut d = d;
            let mut out = [0u8; 4];
            match d.ioctl_read(0x80384b01u32, &mut out) {
                Ok(n) => log::info(f"minted handle answers {n} byte(s), first={out[0]}"),
                Err(_) => log::info("ioctl refused"),
            }
            d.close();
            0
        }
        Err((_, os)) => { log::error(f"mint refused: {os.name()}"); 1 }
    }
}

$ kola run mint.kl --dev-mint vol0=/mnt/data:mint=0x80384b01:map=4096:ioctl=0x80384b01 --sim-dev vol0=vol
[info] minted handle answers 4 byte(s), first=7

A match arm cannot bind a mut name, which is why the Ok(d) arm rebinds it with let mut d = d;.

What the prover sees

The two reqs on read_status do real work. Both of snapshot's builtin bounds, the payload's and the sequence word's, discharge from them, so the function carries no runtime check (see Contracts, traps and tests):

$ kola report checks gw.kl
...
fn read_status
  proven   ro.snapshot(8usize, ..)  [proved #8 + dst.len <= ro.len from req+guards]
  proven   ro.snapshot(seq 0usize, ..)  [proved #0 + #4 <= ro.len from req+guards]
...

The verified IR is the internal form of the program the prover analyses; not every construct can be expressed in it yet. The Dev operations themselves are not in it, and neither are Mmio::window and Mmio::ram. So the function that performs the grant lookup is not analysed, while the driver functions that take a &RamWindowRo are. A gateway naturally has that shape: attach once in main, then read in helpers. If you want kola check --require-analyzed to pass on a function, keep the attach sequence out of it.

The manifest side

A pack that opens device nodes declares the names, and the declaration composes through [deps] the same way granted filesystem roots do:

[pack]
name = "devgw"
version = "0.1.0"

[caps]
allowed = ["Dev", "Sys", "log"]
devices = ["widget"]

$ kola audit .
audit: caps within budget — pack `devgw` (used=["Dev", "Sys"] ⊆ allowed=["Dev", "Sys", "log (effect)"])
audit: devices — declares ["widget"], opens ["widget"]
audit ok: 0 violation(s) — every budget checked in this run is within its declared limits

Drop the devices line and the audit names the device and the manifest key:

error[pack budget]: device name `widget` requested via `Dev::open`/`Dev::mint`/`Dev::open_class` but not declared in [caps] devices = [] — ...

Sys in allowed does not cover Dev. allowed lists what a pack may take out of the root bundle, so a pack that opens a node through sys.dev must list Dev, while a library that receives an already-open Device as a parameter needs nothing, just as one handed a Conn does. Manifest details are in Packages. Device grants are hosted only: a freestanding image has no /dev, and a freestanding build refuses every device construct.

layout_assert: claiming a layout

Hardware descriptors, wire headers and ABI structs have a layout fixed by someone else. A kernel project once kept ten hand-written layout self-checks because kola could not state a struct's size; when the Rust code that cross-checked them was removed, half of them were asserting a layout nothing verified. layout_assert exists so that such a claim is checked by the build.

// A descriptor the hardware also reads: its layout is not ours to choose.
pub struct Desc {
    addr: u64,
    len: u32,
    flags: u16,
    next: u16,
}

layout_assert[Desc](16, 8);

pub fn desc_is_chained(d: &Desc) -> bool !{} {
    d.flags & 1u16 == 1u16
}

A struct's layout is its size, its alignment (the address multiple it must start at) and the offset of each field, including any padding the C compiler inserts. layout_assert[T](SIZE, ALIGN); is a module-level item, not a statement. That matters: a build emits only the reachable functions and drops test items, so a claim inside a function body would quietly stop being checked once that function was no longer called. As an item it is emitted once, unconditionally, next to the definitions it describes, even for a struct no function uses.

kola has no size_of. The size is never computed in the language. You claim it, and the C backend emits _Static_assert(sizeof(T) == SIZE) (a C11 compile-time assertion: the compiler stops with an error if the condition is false) and _Static_assert(_Alignof(T) == ALIGN), so the judge is the target's own C compiler rather than a model of it inside kola. If you need the size as a value, to size a buffer, this feature does not provide it.

A wrong claim fails the build and names the type and the number:

$ kola build --native ring.kl        # with layout_assert[Desc](24, 8);
build/ring.c:808:1: error: static assertion failed: "kola layout_assert[Desc]: claimed sizeof == 24"
error[build]: cc failed: exit status: 1

A claim that cannot hold on any C implementation is refused earlier, by kola check:

$ kola check ring.kl                 # with layout_assert[Desc](12, 8);
error[card §9]: layout_assert[Desc](12, 8) can never hold: a C object's size is always a multiple of its alignment (the trailing padding that makes an array of it work)
  --> ring.kl:9:1
   = help: round the size up to 16, or check the alignment claim

Only the C backend verifies a claim: kola build, kola run --native, kola test --native. The interpreter treats it as a checked no-op, since it has no C layout, and kola build --cross ignores it. A green interpreted kola test tells you nothing about a layout claim.

Every struct the C backend emits already carries internal layout checks, which confirm that the C compiler agrees with kola's own layout model. layout_assert checks something different: that the layout is the number you claim from an external specification. kola and cc can agree perfectly on a layout the hardware does not accept.

What may be claimed: a plain struct or enum you declared, a fixed array, a tuple, or a scalar. A reference, slice, Vec, capability, resource or generic instantiation is refused. The size and alignment must be integer literals or module consts; real layout tables are usually const tables, and a named const reads better at the claim site.

Shipping with no OS: kola build --freestanding

The default C backend is hosted. It uses libc for what libc is for: malloc and free back regions, fprintf and exit implement traps, memcpy and memset move bytes, clock_gettime backs Clock. None of that exists on bare metal.

A freestanding build includes only the compiler-provided headers (<stdint.h>, <stddef.h>, <stdbool.h>), backs regions with a static arena, lowers every trap (a failed contract, an overflow, an out-of-bounds index) to a call to k_panic, which the platform supplies, provides its own memcpy and memset, and turns each OS-dependent backing into an external hook that is referenced only if the program uses it. --freestanding produces an object, never an executable: a bare-metal image is laid out by your linker script, so --link is refused here.

Read the undefined-symbol list

An object file lists the symbols (named functions and variables) it defines and the ones it uses but does not define; the linker must find each undefined one somewhere else when it builds the final image. nm -u prints that second list. Build two small functions freestanding and ask nm what each still needs:

// pure.kl: every obligation discharges
pub fn checksum(xs: &[u8]) -> u64 !{} {
    let mut h = 0xcbf29ce484222325u64;
    for b in xs {
        h = (h ^ widen[u64](b)) *% 0x100000001b3u64;
    }
    h
}

// checked.kl: `+` traps on overflow, and nothing here rules overflow out
pub fn total_len(a: u32, b: u32) -> u32 !{} {
    a + b
}

$ kola build --freestanding pure.kl
build ok (freestanding): 1 native fn(s), 1 exported item(s) (1 fn, 0 const, 0 type) → build/pure.o
  checksum
$ nm -u build/pure.o
                                   (nothing)

$ kola build --freestanding checked.kl
build ok (freestanding): 1 native fn(s), 1 exported item(s) (1 fn, 0 const, 0 type) → build/checked.o
  total_len
$ nm -u build/checked.o
                 U k_panic

checksum walks the slice with for and multiplies with the wrapping operator, so nothing in it can trap and the object references nothing at all. total_len uses checked addition, and the prover cannot rule out overflow from an empty contract. That one residual check is what puts k_panic in the undefined set. The undefined-symbol list is a short summary of what the program can still fail at, which is why a bare-metal project should assert it in its build rather than eyeball it. Assert it as a subset of the allowed hooks, not as a count.

The hooks, and when each appears:

Symbol	Referenced when
`void k_panic(const char *msg)`	a trap edge survives the prover
`uint64_t k_now_ns(void)`	the program reads `clock.now` or `now_boot`, or the unit is built with `-DKOLA_MAIN`
`int64_t k_now_wall_us(void)`	the program reads `now_wall`
`void k_io_write(const char *s)`	the unit is built with `-DKOLA_LOG_HOOK` and the program logs

k_panic is where a contract, bounds or overflow violation lands, deterministically, as a trap does under the interpreter. It must not return (the runtime hangs after it as a safeguard). kola cannot write it for you, because "halt this machine" is the machine owner's decision: log and hang, fault the guest, or reset the board.

Logging is opt-in. Without -DKOLA_LOG_HOOK a log write is dropped and k_io_write is not referenced. With it, the hook receives one formatted [level] message line at a time. Interpolated lines work freestanding, since kola.h carries its own formatter:

$ kola build --freestanding logbare.kl                       # log::info(f"tick {n}")
$ nm -u build/logbare.o
                 U k_panic
$ KOLA_CC="cc -DKOLA_LOG_HOOK" kola build --freestanding logbare.kl
$ nm -u build/logbare.o
                 U k_io_write
                 U k_panic

The k_panic here comes from the formatting code, which can trap; a plain log::info("tick") adds nothing.

If you compile the generated C yourself rather than through kola build --freestanding, the undefined set can change in ways that say nothing about your program: at -O0 an unused clock helper stays alive, and without -fno-stack-protector the compiler adds stack-protector symbols. A build check on the symbol list should use the object kola build --freestanding produced.

No C compiler at all: --cross

Where there is no C compiler, kola build --cross --target <arch> uses kola's own backend and writes an object with no cc and no linker involved. Targets are x86_64, aarch64, riscv64, riscv32, mips64el, mips32el, armv7m, loongarch64 and wasm32; a full triple such as riscv64-linux-gnu also works.

$ kola build --cross --target mips32 --format elf -o ring-mips32.o ring.kl
build ok: 1 native fn(s), 1 skipped → ring-mips32.o (mips32el/elf, 716 bytes)
  skipped `desc_is_chained`: slot `d`: `&struct#0` is outside native-mips32

$ file ring-mips32.o
ring-mips32.o: ELF 32-bit LSB relocatable, MIPS, MIPS32 rel2 version 1 (SYSV), not stripped

The own backend reaches less of the language than the C backend, and where it cannot emit a function it says so and names the reason. Plain --target <triple> without --cross is something else: it passes the triple to the same C compiler.

The C backend is the production build path wherever a C compiler exists. The own backend covers the places without one, and on x86-64 and AArch64 it already links executables for Linux, macOS and Windows: kola build --link tries it first and falls back to cc, with a note, for a program it refuses. Under the hood describes the backends in more detail.

The arena: measuring the heap you have to budget

With no OS there is no malloc and no brk. A freestanding program gets one bump arena per image: a fixed block of memory reserved when the image is linked, from which allocations are handed out by moving a pointer forward ("bumping" it). It is sized by -DKOLA_HEAP_BYTES (16 MiB by default), and the regions from Memory: regions and references carve their slabs from it. -DKOLA_REGION_DEFAULT sets the size of each region's first slab (1 MiB by default), which matters on a small target. Both must be the same on every translation unit of one image.

Reading the watermark

A C program is compiled one translation unit (a .c file plus everything it includes) at a time, and the units are then linked together. The runtime exports two functions a host translation unit can call: k_heap_used_bytes(), the bare-allocation ledger, and k_heap_total_bytes(), the linked pool size. Take a module with one permanent allocation and one per-request function:

// pool.kl
// Permanent state: `heap` is never closed, so what it takes from the arena stays taken.
pub fn stash(n: u64) -> &heap mut Vec[u64] !{alloc(heap)} {
    let v: &heap mut Vec[u64] = alloc in heap mut Vec::new();
    for i in 0..n { v.push(i); }
    v
}

// One request: everything transient lives in a region that closes before
// the fn returns, so the arena rewinds behind it.
pub fn serve(n: u64) -> usize !{} {
    let mut used = 0usize;
    region q {
        let v: &q mut Vec[u64] = alloc in q mut Vec::new();
        for i in 0..n { v.push(i); }
        used = v.len;
    }
    used
}

Exported functions are named k_<module>__<fn> in the generated header (see Embedding kola in a C program):

/* host.c: an ordinary C translation unit beside the kola one */
#define KOLA_FREESTANDING 1
#include "pool.kh"
#include <stdio.h>
#include <stdlib.h>

void k_panic(const char *m) { fprintf(stderr, "k_panic: %s\n", m); exit(7); }

int main(void) {
    printf("start:            used=%6zu of %zu\n",
           k_heap_used_bytes(), k_heap_total_bytes());
    (void)k_pool__stash(1000ull);                         /* permanent, in heap   */
    printf("after stash:      used=%6zu\n", k_heap_used_bytes());
    for (int i = 0; i < 100; i++) k_pool__serve(500ull);  /* transient, region q  */
    printf("after 100 serves: used=%6zu\n", k_heap_used_bytes());
    return 0;
}

$ kola build --freestanding pool.kl
$ cd build
$ cc -c -O2 -ffreestanding -DKOLA_HEAP_BYTES=262144u -DKOLA_REGION_DEFAULT=4096u pool.c -o pool_bare.o
$ cc -O2 -DKOLA_HEAP_BYTES=262144u -DKOLA_REGION_DEFAULT=4096u -I. ../host.c pool_bare.o -o host
$ ./host
start:            used=     0 of 262144
after stash:      used= 12480
after 100 serves: used= 12480

used counts region slabs and growth chunks taken from the arena, not the bytes live inside a region. It is the number KOLA_HEAP_BYTES has to cover. It goes down as well as up, so sample its peak under load rather than taking one reading.

Reclaim on close

A hundred calls to serve cost no permanent bytes. A closing region counts its own allocations, and close rewinds the arena if and only if the ledger advanced by exactly that count, which proves every byte above the region's mark belongs to it.

Now keep the per-request state in heap by mistake, a one-word change in a type, and the same service dies:

/* leak.c: the same service, with per-request state left in heap */
int main(void) {
    for (int i = 0; ; i++) {
        if ((i % 20) == 0) {
            printf("request %4d: used=%7zu of %zu\n",
                   i, k_heap_used_bytes(), k_heap_total_bytes());
            fflush(stdout);
        }
        (void)k_pool__stash(100ull);
    }
}

$ ./leak
request    0: used=      0 of 262144
request   20: used=  28960 of 262144
request   40: used=  61824 of 262144
request   60: used= 127456 of 262144
...
request  120: used= 258624 of 262144
...
request  220: used= 258624 of 262144
k_panic: bare heap exhausted

Some consequences of the rewind rule:

Arena sizing is peak-concurrent, not cumulative. Nested or sequential regions cost their maximum live size, plus one slab per interleave event.
An interleave event is an allocation by someone else inside a region's window (between its start mark and its close), such as a program-lifetime cache that grows in the middle of a request. Rewinding over it would hand live cache bytes to the next region, so that window is not reclaimed. What leaks is the event, not the request, and events are rare: a cache that grows geometrically interleaves a logarithmic number of times over the life of the process.
A budgeted region (region r from m) refunds the Mem credits it charged when it closes, on every exit path. Arena bytes and budget credits are separate ledgers that answer different questions.

For a service that must survive unbounded requests, there are three idioms, in order of preference. Use a per-request region { } closed before return, and keep program-lifetime state in heap or an outer region. Have library entry points take caller-provided scratch, so that a warmed scratch Vec allocates nothing per call. Or, for a resident state machine that can persist itself, close its long-lived region and restore it into a fresh one. The last is a policy decision only the program can make, because the runtime cannot know which states are restorable.

One pool per image

The arena is one array per linked image, not one per translation unit. Every translation unit that includes kola.h emits a definition of it, marked weak (a weak symbol is one the linker may discard in favour of another definition of the same name), and it lives in a link-once section (.gnu.linkonce.b.k_heap on ELF), so the linker keeps exactly one copy and nothing is asked of your cc line. A hand-written linker script is the exception: a .bss rule that lists input sections explicitly needs *(.gnu.linkonce.b.*), or the pool becomes an orphan section placed wherever the linker decides. Whether a given linker discards the losing copies is a per-linker question; it has been checked on GNU ld and LLD, not on gold or mold.

You can check the linked image itself, with no kola involved. It should contain exactly one defined k_heap, weak; its st_size should equal the pool you intend; and the linked value of k_heap_bytes should equal the same number. Checking that every object was compiled with the same -DKOLA_HEAP_BYTES is useful but cannot see what the linker kept.

An image that never allocates can say so. -DKOLA_HEAP_BYTES=0 on its own is refused at compile time, because a zero-sized definition could win the link and starve a unit that does allocate. Paired with -DKOLA_NO_HEAP it is accepted and means two things at once: nothing is reserved, and every allocation traps by name:

$ cc -c -ffreestanding -DKOLA_NO_HEAP -DKOLA_HEAP_BYTES=0 ...
# at run time, on any allocation:
k_panic: bare allocation in an image built -DKOLA_NO_HEAP: this image declares that it never allocates from the bare pool, and something just did. Either the allocation is a defect, or the declaration is wrong — drop -DKOLA_NO_HEAP and pass the image's real pool size to EVERY TU.

The message is deliberately not "bare heap exhausted": a pool that was never reserved did not run out. -DKOLA_NO_HEAP with a nonzero size is a contradiction and is refused at compile time, which catches a build script that grew a real pool while an old flag stayed on its command line.