Hardware: granted windows and typed device access

kola has no pointer type. There is no raw address you can dereference and no cast from an integer to a memory location (SPEC-CARD §12). Yet kola drives real hardware, and hardware is reached through addresses. A network card or a serial port exposes its controls as registers that appear at fixed physical addresses: reading or writing one of those addresses talks to the device instead of to RAM. This is called memory-mapped I/O, or MMIO. Devices also share ordinary memory with the CPU. With DMA (direct memory access) a device reads and writes RAM on its own, for example a network card picking up outgoing packets from a ring of descriptors the driver filled in. kola reaches both through one construct, the window, and this chapter is about it.

A window is a length and an opaque base. The program never learns the address. It computes offsets, and the same prover that discharges array bounds (Contracts, traps, and tests) checks each offset against the window's length. In exchange for the pointer you get a driver whose memory accesses can be proven in range at compile time. That matters more in a kernel than anywhere else, because a trap in a kernel is not something a caller can catch.

Grants

If you have read the filesystem chapter, you know the pattern. The sandbox is closed by default, and the way out is a grant: the operator binds a name to a piece of the outside world, the program asks for that name, and the manifest lists the names a pack may ask for. --fs-root db=/var/lib/thing grants a directory. Windows apply the same idea to physical memory.

The capability is sys.mmio: Mmio, part of the root set handed to main. It mints windows by name, and every lookup answers Option:

sys.mmio.window(b"uart0")    // -> Option[MmioWindow]  device registers
sys.mmio.ram(b"ring0")       // -> Option[RamWindow]   memory shared with hardware
sys.mmio.io_window(b"com1")  // -> Option[IoWindow]    x86 port I/O

A name nobody granted is None, not an error, so a program can notice that a grant is missing and carry on. Here is a complete program:

use std::log;

fn main(sys: Sys) -> u8 !{io, log} {
    match sys.mmio.ram(b"ring0") {
        Some(w) => {
            log::info(f"ring0 granted, len={w.len}");
            w.write32(0, 0xC0FFEEu32);
            let back = w.read32(0);
            log::info(f"read back {back}");
            0
        }
        None => { log::error("no ring0 grant"); 2 }
    }
}

$ kola run grant.kl --ram-window ring0=0x1000:0x100 --log stderr
[info] ring0 granted, len=256
[info] read back 12648430

$ kola run grant.kl --log stderr
[error] no ring0 grant

RamWindow is ordinary memory shared with hardware. MmioWindow is a block of device registers. IoWindow is for x86 port I/O, an older second address space that x86 CPUs reach with the special in and out instructions instead of normal loads and stores. Each window kind has a flag and an environment twin:

The value is base:len (port:len for port I/O, with the port at most 0xFFFF). The length is required, because it becomes the window's .len. On a hosted run (an ordinary program under an operating system) the base is ignored. In a freestanding build, which runs directly on the hardware with no operating system underneath, it is the real physical address.

Grants in tests

A test that probes for a window gets None unless the run grants one, so write drivers in two halves. The model half (the device's behaviour, a state machine, an encoder) is pure kola that you can test with no grant at all. The driver half takes a window and is tested by a run that supplies the flags. Inside a test the bundle is sim, and kola test accepts the same grant flags:

fn poke(w: &RamWindow) -> u32 !{io}
    req w.len >= 8
{
    w.write32(0, 42u32);
    w.read32(0)
}

test a_granted_window_inside_a_test(mut sim: Sim) {
    match sim.mmio.ram(b"scratch") {
        Some(w) => { let v = poke(&w); assert v == 42u32; }
        None => { assert false; }
    }
}

$ kola test tw.kl --ram-window scratch=0x0:0x40
tw.kl: test a_granted_window_inside_a_test ... ok
...
$ kola test --interp tw.kl
tw.kl: test a_granted_window_inside_a_test ... FAILED (seed 1802464353)
error[card §8]: assertion failed

Grants in the manifest

A pack declares the window names it may ask for, one list per kind: mmio_windows, ram_windows, io_windows (see Packages). A probe for an undeclared name fails the audit:

[caps]
allowed = ["Sys", "Mmio", "log"]
ram_windows = ["ring0"]

$ kola audit ringdrv          # with ram_windows = []
error[pack budget]: granted window `ring0` probed via Mmio::ram / Mmio::bind_ram but not declared in [caps] ram_windows = [] — the audit signal is "wants ring0", so the name must be on the manifest (design-kernel-lowlevel.md §1.8).
audit: FAILED (1 violation(s)) — see the `error[...]` line(s) above; `kola audit` exits 1

$ kola audit ringdrv          # with the name declared
audit: caps within budget — pack `ringdrv` (used=["Mmio", "Sys"] ⊆ allowed=["Sys", "Mmio", "log (effect)"])
audit: ram windows — declares ["ring0"], probes ["ring0"]
audit ok: 0 violation(s) — every budget checked in this run is within its declared limits

Offsets and proofs

Every window operation carries builtin contracts that you do not write and cannot switch off:

• off + size <= self.len: the access lies inside the window.

• off % size == 0: natural alignment, for every access wider than a byte. A 4-byte access must start at an offset divisible by 4; many CPUs and devices fault or misbehave otherwise. The byte-granular bulk operations (copy_in, copy_out, zero) carry only the bound.

These are ordinary contracts, discharged by the ordinary prover, so the ordinary technique works: state what you need about the window in a req on your driver function, and the obligations inside the body follow from it. Here is a descriptor ring over a 256-byte window. A descriptor is a small fixed-size record telling a device where a buffer is and how long it is; a ring is an array of them that the driver fills at one end (the tail) and the device consumes at the other (the head).

use std::log;

const RING_BYTES: usize = 256;   // the granted length this driver needs
const HEAD: usize  = 0x00;       // consumer index (u32)
const TAIL: usize  = 0x04;       // producer index (u32)
const MAGIC: usize = 0x08;       // layout tag (u64)
const DESC_BASE: usize = 0x10;   // first descriptor slot
const DESC_SIZE: usize = 16;
const SLOTS: usize = 15;         // 0x10 + 15 * 16 = 256

fn ring_init(w: &RamWindow) !{io}
    req w.len >= RING_BYTES
{
    w.zero(0, RING_BYTES);
    w.write64(MAGIC, 0x6b6f6c6172696e67u64);
    w.write32(HEAD, 0u32);
    w.write32(TAIL, 0u32);
}

// Where slot `i` starts. The `ens` lets a caller's copy bound discharge.
fn slot_off(i: usize) -> usize !{}
    req i < SLOTS
    ens ret + DESC_SIZE <= RING_BYTES
{
    DESC_BASE + i * DESC_SIZE
}

fn ring_push(w: &RamWindow, slot: usize, desc: &[u8], tail: u32) !{io}
    req slot < SLOTS, desc.len == DESC_SIZE, w.len >= RING_BYTES
{
    let off = slot_off(slot);
    w.copy_in(off, desc);
    w.write32(TAIL, tail);
}

fn main(sys: Sys) -> u8 !{io, log} {
    match sys.mmio.ram(b"ring0") {
        Some(w) => {
            if w.len < RING_BYTES { log::error("ring0 is too small"); return 1; }
            ring_init(&w);
            let d = [0xEFu8, 0xBE, 0xAD, 0xDE, 0, 0, 0, 0, 64, 0, 0, 0, 1, 0, 0, 0];
            ring_push(&w, 14, &d, 1u32);
            let tail = w.read32(TAIL);
            let mut back = [0u8; 16];
            w.copy_out(0xF0, &mut back);
            log::info(f"tail={tail} b0={back[0]} b12={back[12]}");
            0
        }
        None => { log::error("no ring0 grant"); 1 }
    }
}

Writing the register map as named constants is more than style. A constant offset folds at compile time, so both its bound and its alignment are decided there. The one guard in main (if w.len < RING_BYTES) gives the prover the fact that every req below needs.

kola report checks lists every obligation in the file and how it was settled:

$ kola report checks ringdrv.kl
fn ring_init
  proven   w.zero(0usize, ..)  [proved #0 + #256 <= w.len from req+guards]
  proven   w.write64(8usize, ..)  [proved #8 + 8 <= w.len from req+guards]
  proven   w.write64(8usize, ..) align  [8 % 8 == 0 (const offset)]
  ...
fn slot_off
  proven   16usize + (i * 16usize [novf: product bounded by width])  [sum bounded by width]
  proven   i * 16usize  [product bounded by width]
  proven   ens at tail  [ens discharged at this exit]
fn ring_push
  proven   req slot_off(slot)  [req discharged at this call site]
  proven   w.copy_in(off, ..)  [proved off + desc.len <= w.len from req+guards]
  ...
fn main
  proven   req ring_init(w)  [req discharged at this call site]
  proven   req ring_push(w, 14usize, &d, 1u32)  [req discharged at this call site]
  proven   w.copy_out(240usize, ..)  [proved #240 + #16 <= w.len from req+guards]
  ...
13 mmio site(s): 13 proven at compile time, 0 runtime

In application code an unproven bound is acceptable: it becomes a runtime check, and if it fails the program traps with a diagnostic. In a kernel nobody receives that trap. A driver whose report shows a runtime window site has a crash in it that no test has found yet, so for kernel code the target is zero runtime sites. If a function never reaches the verified IR, the report says so and names the reason, so a clean count over the analyzed functions is never mistaken for a clean count over the program. The report reflects the prover of the compiler you run, so re-run it rather than quote it.

The proof reaches the generated code. In a freestanding build, a proven access is a bare call with a discharge marker, and the same operation with nothing to prove from carries a bounds test and a trap:

// req off + FRAME <= w.len
({ KRamWindow kt1 = (*(w)); size_t kt2 = (size_t)(off); size_t kt3 = (size_t)(k_dma__FRAME);
   /*IR:ram-bounds*/ k_dma_writeback((void *)(kt1.base + kt2), kt3); (void)0; });

// no req
({ KRamWindow kt1 = (*(w)); size_t kt2 = (size_t)(off); size_t kt3 = (size_t)(n);
   if (kt2 > kt1.len || kt1.len - kt2 < kt3)
       k_trap("ram dma_writeback out of range: off + len > window len (card §7)");
   k_dma_writeback((void *)(kt1.base + kt2), kt3); (void)0; });

This is also what "opaque base" means: the address appears only as kt1.base + kt2, assembled at the point of use from a base no kola expression can name and an offset kola computed and proved.

When a bound or an alignment cannot be proven, you get a runtime check. A constant misaligned offset is not a compile error; it is an obligation that fails when it runs:

use std::log;

fn read_status(w: &RamWindow) -> u32 !{io}
    req w.len >= 0x20
{
    w.read32(0x06)     // 6 % 4 != 0: an unaligned word access
}

fn main(sys: Sys) -> u8 !{io, log} {
    match sys.mmio.ram(b"regs") {
        Some(w) => {
            if w.len < 0x20 { return 2; }
            let s = read_status(&w);
            log::info(f"status={s}");
            0
        }
        None => { log::error("no grant"); 1 }
    }
}

$ kola report checks misrun.kl
fn read_status
  proven   w.read32(6usize)  [proved #6 + 4 <= w.len from req+guards]
  RUNTIME  w.read32(6usize) align
...
$ kola run misrun.kl --ram-window regs=0x0:0x40 --log stderr
trap: error[card §7]: ram read32 misaligned: off 0x6 % 4 != 0 on window `regs`
  --> misrun.kl:6:5
   = help: a RAM-window word access must be naturally aligned: the op's builtin contract is `off % N == 0`

The window kinds

One capability mints several window types. Each difference between them reflects what the hardware behind the window does.

MmioWindow has eight operations, read8/16/32/64 and write8/16/32/64, and nothing else. Every access is volatile: the compiler may not merge, repeat or drop one, as it might with ordinary memory, because reading a register can have side effects (taking the next byte out of a receive queue, or clearing a status bit). Accesses are also ordered as the device sees them. CPUs normally reorder memory operations for speed, and a barrier is an instruction that forbids that. An MmioWindow access needs none: a write lands after every earlier store and a read happens before every later load. So writing a descriptor into a RamWindow and then writing the doorbell register (the register that tells the device "new work is ready") is safe as written.

RamWindow has the same eight operations with the same contracts, plus a byte-granular bulk family: copy_in(off, src), copy_out(off, dst) and zero(off, n). Copying a descriptor into a slot is one memory copy, not sixteen byte writes. Because it is ordinary memory, its plain operations are on the io row. Two of its families are on hw; they are described below.

IoWindow has six operations, not eight. x86 in and out go up to 32 bits, so the type has no 64-bit pair, and asking for one is a compile error that explains why:

fn probe(w: &IoWindow) -> u64 !{hw}
    req w.len >= 8
{
    w.read64(0)
}

error[card §7]: `IoWindow` has no `read64`: x86 port I/O is 8/16/32-bit only
  --> io64.kl:4:5
   = help: an I/O-space window lowers to in/out (inb/inw/inl, outb/outw/outl) — there is no 64-bit port op. Use read32/write32, or split the access; for a 64-bit MMIO register use `sys.mmio.window` (a memory window has read64) (design-kernel-lowlevel.md §2.3)

In a freestanding build an IoWindow lowers to in/out on x86 and is refused on every other architecture.

Narrowing a RAM window

A RamWindow has two attenuations. Both are !{}, need no grant and cost nothing at run time, because narrowing authority you already hold is always safe. It is the same move as Dir to DirRo in the filesystem chapter.

w.ro() gives a RamWindowRo, which carries read8/16/32/64, copy_out, .len and one operation of its own, snapshot (below). The write operations, copy_in, zero and the DMA operations do not exist on the type, so a reader that writes does not compile:

// Attenuation is free: no grant, no effect, no capability argument.
fn narrow_it(w: &RamWindow) -> RamWindowRo !{} {
    w.ro()
}

fn bump(ro: &RamWindowRo) !{io}
    req ro.len >= 8
{
    let s = ro.read32(0);
    ro.write32(0, s + 1u32);
}

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
  --> rowrite.kl:5:5
   = help: `w.ro()` ATTENUATES a `RamWindow`: the result carries `read8/16/32/64`, `copy_out`, `.len` and `snapshot`, and nothing that mutates ...

w.atomic() gives an AtomicWindow, which carries .len and nothing else. Its cells can be reached only by passing it as the cells argument of an Atomic:: operation (The machine). Code that holds an AtomicWindow cannot touch those cells any other way. That rules out a classic bug: a cell written atomically by one core and with a plain store by another, which works on some machines and is not correct on any memory model. atomic() does not consume the original window, so the guarantee lives in the parameter type of the code you hand the AtomicWindow to.

Windows a kernel creates itself

Two more operations create a RamWindow, both meant for kernels rather than for grants. Mmio::reserve(name, size, align) asks the compiler to emit storage that kola owns, reachable only through the returned window; the name and both sizes must be constants. Mmio::bind_ram(name, base, len) creates a window over an address the program learns at run time, such as a PCI BAR or a framebuffer base from the boot protocol, and bind_window/bind_io_window do the same for the device kinds. The name must still be declared in the pack's per-kind list (ram_windows, mmio_windows, io_windows); an undeclared name answers None.

reserve and bind_ram work in hosted builds too: the address is ignored and a zeroed buffer of the requested length is used, which is a faithful model of plain memory. bind_window and bind_io_window are freestanding only. A device register does not read back what was written, so a buffer standing in for one would make a write-then-read test pass on the host and fail on the hardware.

Seqlocks

RamWindowRo has one operation of its own: snapshot(seq_off, off, &mut dst) -> bool, a seqlock read. A writer on another core makes a sequence word odd, stores the data, and makes the word even again. The reader copies the data while the word is even and unchanged across the copy; otherwise it retries. The point is to avoid a torn read, a copy that mixes bytes from two different writes, without making the writer wait for readers. NIC descriptor rings publish this way, and so do kernel modules that expose state to userspace.

The write side is one operation on the full window, publish(seq_off, off, &src) -> bool:

use std::log;

const SEQ: usize = 0x40;   // the sequence word (u32)
const DATA: usize = 0x00;  // the payload it guards

// The reader holds only the read-only twin.
fn read_epoch(ro: &RamWindowRo, dst: &mut [u8]) -> bool !{io}
    req ro.len >= 0x80, dst.len == 8
{
    ro.snapshot(SEQ, DATA, dst)
}

// The writer: one op owns both ordering edges.
fn publish_epoch(w: &RamWindow, src: &[u8]) -> bool !{io, hw}
    req w.len >= 0x80, src.len == 8
{
    w.publish(SEQ, DATA, src)
}

fn main(sys: Sys) -> u8 !{io, hw, log} {
    match sys.mmio.ram(b"hdr") {
        Some(w) => {
            if w.len < 0x80 { return 2; }
            let payload = [0xEFu8, 0xBE, 0xAD, 0xDE, 0, 0, 0, 0];
            let published = publish_epoch(&w, &payload);
            let ro = w.ro();
            let mut buf = [0u8; 8];
            let ok = read_epoch(&ro, &mut buf);
            log::info(f"published={published} ok={ok} b0={buf[0]}");

            w.write32(SEQ, 3u32);              // an odd word: a publish in flight
            let mut buf2 = [0u8; 8];
            let ok2 = read_epoch(&ro, &mut buf2);
            let again = publish_epoch(&w, &payload);
            log::info(f"mid-publish ok={ok2} b0={buf2[0]} publish={again}");
            0
        }
        None => { log::error("no hdr grant"); 1 }
    }
}

$ kola run seq.kl --ram-window hdr=0x0:0x80 --log stderr
[info] published=true ok=true b0=239
[info] mid-publish ok=false b0=0 publish=false

kola run --native prints the same two lines. Look at the second line. With the sequence word odd, the reader refused and buf2 is still zeros: dst is written only on success, so a torn snapshot is never produced at all, not even with a warning. The number of retries is not a parameter, because the right bound depends on the writer's critical section rather than on the caller. publish is symmetric: if the word is already odd it answers false and writes nothing, so two publishers cannot interleave into a torn page.

Inside the runtime, publish reads the even sequence word, stores it odd, issues a store-store fence (a barrier that keeps the odd-word store from being reordered after the data stores), copies src.len bytes to off, and release-stores the word even. It carries the same two contracts as snapshot (off + src.len <= self.len and seq_off + 4 <= self.len). It is on the hw row because only the effect row can say "with ordering another core depends on". The payload is copied, because an operation that owns both ordering edges must own what happens between them, and kola has no closures through which to hand the runtime a critical section.

Device models

A window grants physical memory, and a hosted process has none. What backs a window when you run on a laptop depends on its kind.

A RamWindow needs nothing, because plain memory is already a good model of plain memory: write a byte and you read it back. That is why the ring driver ran with a grant and no model, and why kola run and kola run --native produce the same bytes for it.

An MmioWindow or IoWindow needs a model, because a register is not memory. A read-only register ignores writes; a status register clears itself when read; a counter answers with the time. A register's behaviour is a function, so the model is three functions over a state type you declare:

fn p_new() -> M !{}
fn p_read(m: &mut M, off: usize, width: usize, now: u64) -> u64 !{}
fn p_write(m: &mut M, off: usize, width: usize, val: u64, now: u64) !{}

width is in bytes (1, 2, 4 or 8). now is the clock of the bundle: virtual under Sim, the wall clock under Sys. You bind the three by their shared prefix: --sim-mmio timer0=tm uses tm_new, tm_read and tm_write (mod::tm looks them up in module mod). Here is a timer with a read-only counter and a status flag that clears on read, together with a driver for it:

use std::log;

const T_CTRL: usize  = 0x00;  // read-write: enable bit
const T_COUNT: usize = 0x08;  // read-only: the running count
const T_STAT: usize  = 0x10;  // pending flag, clears on read

// The model: three pure fns over a state struct of your own.
struct TimerModel { ctrl: u64, base: u64, fired: bool }

fn tm_new() -> TimerModel !{} {
    TimerModel { ctrl: 0, base: 0, fired: false }
}

fn tm_read(m: &mut TimerModel, off: usize, width: usize, now: u64) -> u64 !{} {
    if off == T_CTRL { return m.ctrl; }
    if off == T_COUNT {
        if m.ctrl == 0 { return 0; }
        return now - m.base;
    }
    if off == T_STAT {
        let s = if m.fired { 1u64 } else { 0u64 };
        m.fired = false;           // clears on read
        return s;
    }
    0
}

fn tm_write(m: &mut TimerModel, off: usize, width: usize, val: u64, now: u64) !{} {
    if off == T_CTRL {
        m.ctrl = val & 1;
        m.base = now;
        m.fired = true;            // arming raises the pending flag
    }
    // T_COUNT and T_STAT are read-only: a write to them is ignored.
}

// The driver: written against the window, unaware of the model.
fn timer_arm(w: &MmioWindow) -> u64 !{hw}
    req w.len >= 0x18
{
    w.write64(T_CTRL, 1u64);
    w.write64(T_COUNT, 999u64);    // read-only register: ignored
    let c = w.read64(T_COUNT);
    let s0 = w.read64(T_STAT);     // 1: pending
    let s1 = w.read64(T_STAT);     // 0: cleared by the first read
    let mut acc = (s0 << 8) | s1;
    if c != 999 { acc = acc | (1u64 << 16); }
    acc
}

fn main(sys: Sys) -> u8 !{io, hw, log} {
    match sys.mmio.window(b"timer0") {
        Some(w) => {
            if w.len < 0x18 { return 2; }
            let acc = timer_arm(&w);
            log::info(f"acc={acc}");
            0
        }
        None => { log::error("no timer0 grant"); 1 }
    }
}

test status_clears_on_read {
    let mut m = tm_new();
    tm_write(&mut m, T_CTRL, 8, 1, 0);
    let first = tm_read(&mut m, T_STAT, 8, 0);
    let second = tm_read(&mut m, T_STAT, 8, 0);
    assert first == 1;
    assert second == 0;
}

test the_count_register_ignores_writes {
    let mut m = tm_new();
    tm_write(&mut m, T_CTRL, 8, 1, 100);
    tm_write(&mut m, T_COUNT, 8, 999, 100);
    let c = tm_read(&mut m, T_COUNT, 8, 140);
    assert c == 40;
}

$ kola test timer.kl
timer.kl: test status_clears_on_read ... ok
timer.kl: test the_count_register_ignores_writes ... ok
...
$ kola run timer.kl --mmio-window timer0=0x0900_0000:0x18 --sim-mmio timer0=tm --log stderr
[info] acc=65792

The tests exercise the model directly, with no grant and no flags. Each register read is bound with let before the assert, because an assert expression may not change state and a clears-on-read register does. Under kola run --native the model is compiled into the program, so the native build gives the same answer.

The model binding is required for these two kinds, and the check happens at startup, before your program runs. Both mistakes are refused with the missing flag spelled out:

$ kola run timer.kl --mmio-window timer0=0x0:0x18
error[card §7]: mmio window `timer0` is granted but has no model binding — hosted runs back windows with a SimMmio model
  = help: add --sim-mmio timer0=<prefix> (or KOLA_SIM_MMIO_timer0=<prefix>): the prefix names three program fns `<p>_new`/`<p>_read`/`<p>_write` (design-kernel-lowlevel.md §1.3); `mod::<p>` resolves them in module `mod`

$ kola run timer.kl --sim-mmio timer0=tm
error[card §7]: mmio model `timer0` is bound but the window was never granted — a binding backs a GRANT, it does not create one
  = help: add --mmio-window timer0=0x0:LEN (len is REQUIRED and sizes the window's `.len`; the base is ignored under hosted run/test — design-kernel-lowlevel.md §1.2)

Effect rows: io for memory, hw for the machine

Effects and capabilities introduced the effect rows. hw marks a privileged or ordering-sensitive machine operation, and it is separate from io because "this code talks to the operating system" and "this code performs a privileged machine operation" are different questions for a reviewer. hw is enforced like io: it is forbidden in ct functions and never elided or reordered.

One Mmio capability mints windows on both rows, because memory shared with hardware is ordinary memory while a device register access is a privileged operation. So RamWindow's word and bulk operations are io; its DMA cache pair, its release stores and publish are hw; everything on MmioWindow and IoWindow is hw. The rows are checked:

fn probe(w: &MmioWindow) -> u32 !{io}
    req w.len >= 8
{
    w.read32(0)
}

error[card §6]: `probe` performs `hw` (mmio read) but does not declare it
  --> rowmiss.kl:4:5
   = help: add `hw` to the effect clause, or hand the work to a caller that has it

The CPU keeps recently used memory in a cache, and on many chips a DMA engine reads RAM directly without looking in that cache. So before a device reads a buffer the CPU wrote, the dirty cache lines must be written back to RAM, and after a device writes a buffer, the CPU's stale cached copy must be thrown away. The DMA cache pair does exactly that: dma_writeback(off, n) writes a range out of the data cache, and dma_invalidate(off, n) discards the cached copy so the CPU sees what the engine wrote. Both carry the bulk family's bound. They are freestanding only, and the hosted native build says why:

const FRAME: usize = 64;

// Flush one frame out of the data cache before the DMA engine reads it.
fn tx_frame(w: &RamWindow, off: usize) !{hw}
    req off + FRAME <= w.len
{
    w.dma_writeback(off, FRAME);
}

fn main(sys: Sys) -> u8 !{io, hw} {
    match sys.mmio.ram(b"ring0") {
        Some(w) => {
            if w.len < FRAME { return 2; }
            tx_frame(&w, 0);
            0
        }
        None => 1,
    }
}

$ kola run --native dma.kl --ram-window ring0=0x0:0x1000
codegen: native codegen: `w.dma_writeback(...)` in `tx_frame` has no HOSTED native lowering (design-hot-datapath.md §2.1b: a hosted process has no cache to maintain) — interpret it (`kola run|test`), or build `--freestanding`, where the per-arch KOLA_HOT_DMA table lowers it ...

$ kola build --freestanding dma.kl -o out
build ok (freestanding): 2 native fn(s), 0 exported item(s) (0 fn, 0 const, 0 type) → out/dma.o

Under the interpreter the cache operations do nothing, which is accurate: a hosted process has nothing to flush. The values are the same; the effect the operation exists for cannot be observed there.

Where simulation stops

The interpreter is an oracle for values and nothing else. It tells you that your descriptor encoding is right, that your offsets are in range, that your state machine moves correctly. It cannot tell you that a barrier is in the right place, that a cache line was flushed, or that two cores agree. A comparison between two executors that share the same blind spot cannot tell you either. The interpreter is single-threaded, so a release store, a fence and a plain store all look the same to it.

A real example shows the gap. Caches work in fixed-size blocks called lines, so a writeback loop steps through a range one line at a time. On MIPS, the DMA cache operations take the line size from a CP0 configuration register. The runtime once read the wrong register select. The value it got made the writeback loop step too far and run once per window, so the second cache line of each frame was never flushed and the DMA engine sent stale bytes: frames on the wire were cut off at exactly byte 32. Every hosted run passed, and the cross-assembly passed too, because a wrong register select assembles cleanly. Only running on the real chip showed it.

So claims about ordering, caches and coherence are settled by reading the generated assembly and by running on the target hardware. The window gives up the pointer and gets a proof of every offset in return; the simulator gives up the machine and tells you plainly where that leaves you. Both trades are worth making if you know where each one stops.