The machine: Cpu, ordering, and atomics

Most kola code runs inside an operating-system process and reaches the world through system calls. This chapter is about the layer underneath: code that switches interrupts off, writes a CPU's control registers, flushes a cache, or shares memory with another CPU core without a lock. That is the work of kernels, hypervisors and device drivers, and kola supports it through one capability (Cpu), one effect row (hw) and a small family of atomic operations.

The hardware windows chapter covers how a program reaches device registers and shared memory without a pointer, including seqlocks and DMA cache maintenance. Bare metal covers device nodes and freestanding builds. This chapter takes windows as given.

The hw effect

Effects say what kind of thing a function does. The hw marks a privileged or ordering-sensitive machine operation. "Privileged" means an instruction the CPU only allows in kernel mode, such as switching interrupts off. "Ordering-sensitive" means an operation whose point is when its effect becomes visible to other cores or devices, such as a memory barrier.

The compiler treats hw like io: it never removes or reorders such an operation, and it is forbidden in constant-time functions. It is a separate row so that a reviewer can see which functions touch the machine itself, as opposed to which talk to the operating system. Leave it out and the checker names the operation:

fn mask(cpu: &Cpu) !{io} {
    cpu.irq_disable();
}

error[card §6]: `mask` performs `hw` (cpu irq_disable) but does not declare it
  --> row.kl:2:5
   = help: add `hw` to the effect clause, or hand the work to a caller that has it

An atomic operation inside a ct fn is refused like any other call to a non-ct function:

error[card §6b]: [ct fn `leaky`] ct fn calls non-ct fn `load32_relaxed` — a `ct` fn may only call other `ct` fns or the `widen`/`narrow`/`wrap` builtins

The Cpu capability

A window is granted by name, because "which device?" has many possible answers and only the operator who starts the program can choose. "May this code run privileged CPU instructions?" has one answer, so Cpu is a single authority token on the root set, like Clock or Rng. There is no flag, no lookup and no Option: sys.cpu is always there, and a test gets sim.cpu from its Sim bundle.

Every Cpu operation takes a shared &Cpu. The simulated CPU keeps real state (an interrupt flag, register files) and updates it through that shared reference, which keeps functions taking &Cpu inside the verified subset so that the bounds and req obligations around them still prove.

Under the interpreter and in hosted native builds (ordinary programs under an operating system: kola run --native, kola test --native), the operations run against the same simulated CPU, so the two executors agree. A hosted process has no interrupt table to load; a model of one is what both give you. That means cpuid answers what the model says, not what your machine says. A freestanding build (kola build --freestanding, code that runs directly on the hardware with no operating system underneath) lowers each operation to the real instruction for the target architecture.

Interrupts

An interrupt is the hardware stopping whatever the CPU is doing to run a handler: a timer tick, a packet arriving, a key press. Kernel code that updates shared state often has to switch interrupts off briefly, so a handler cannot run in the middle and see half-finished work. That stretch is a critical section.

There are four operations: irq_disable(), irq_enable(), irq_save() -> u64 and irq_restore(flags: u64). irq_save disables interrupts and returns the state from before (1 means they were enabled). That is why it exists beside irq_disable. A critical section that ends with irq_enable() is wrong if its caller already had interrupts off, because it switches them back on behind the caller's back. save and restore put back exactly what was there, so critical sections can nest.

use std::log;

// Mask interrupts, do the work, put back exactly the state that was there.
fn critical(cpu: &Cpu) !{hw, log} {
    let prior = cpu.irq_save();
    log::info(f"critical section entered, prior={prior}");
    cpu.irq_restore(prior);
}

fn main(mut sys: Sys) -> u8 !{hw, log} {
    critical(&sys.cpu);        // a reset CPU starts masked: prior = 0
    sys.cpu.irq_enable();
    critical(&sys.cpu);        // now prior = 1, and restore leaves them on
    let after = sys.cpu.irq_save();
    log::info(f"after both sections, interrupts were on={after}");
    0
}

$ kola run --log stderr crit.kl
[info] critical section entered, prior=0
[info] critical section entered, prior=1
[info] after both sections, interrupts were on=1

The first prior=0 is the simulated CPU's own state: like a real CPU after reset, it starts with interrupts masked.

Halting, waiting and spinning

A CPU with nothing to do should stop and wait for something to happen instead of burning power. kola has three operations for that, hlt(), wfi() (wait for interrupt) and wfe() (wait for event), and one for the opposite case, spin_hint(), which tells the CPU that the code is in a busy loop waiting for another core. Under the interpreter all four do nothing, since the simulator does not model interrupts arriving. In a freestanding build they map to these instructions:

x86 has no wait-for-event instruction. The obvious substitute, pause, does not park the CPU, so a kernel idle loop written as loop { cpu.wfe(); } would spin at full power on x86 and sleep elsewhere. Rather than let one operation mean two things depending on the target, kola refuses wfe on x86. Code generation emits each Cpu operation in expression position, where a C _Static_assert cannot go, so the refusal is an undeclared identifier whose name is the diagnostic:

pub fn park(cpu: &Cpu) !{hw} { cpu.wfe(); }

fn main(mut sys: Sys) -> u8 !{hw} { park(&sys.cpu); 0 }

$ kola build --freestanding wait.kl -o out        # on an x86-64 host
out/kola.h:9800:5: error: ‘k_cpu_wfe_UNAVAILABLE_ON_x86_64__use_wfi_to_park_or_spin_hint_to_spin’ undeclared (first use in this function)
error[build]: cc failed: exit status: 1

The identifier names both repairs: wfi to park, spin_hint to spin. The same C compiles for aarch64 and mips, which have a real wait-for-event.

Here is a loop that uses spin_hint: a bounded attempt to take a spinlock, a lock that a waiting core acquires by retrying in a loop rather than by sleeping. The atomic operations it uses are explained further down.

// A bounded compare-and-swap acquire: the shape of every SMP spinlock.
pub fn try_acquire(cpu: &Cpu, cells: &[u32], i: usize, budget: u32) -> bool !{hw}
    req i < cells.len
{
    let mut tries = 0u32;
    while tries < budget {
        if Atomic::cas32_acquire(cells, i, 0u32, 1u32) == 0u32 {
            return true;
        }
        cpu.spin_hint();
        tries = tries + 1;
    }
    false
}

pub fn release(cells: &[u32], i: usize) !{hw}
    req i < cells.len
{
    Atomic::store32_release(cells, i, 0u32);
}

test the_lock_is_taken_then_released(mut sim: Sim) {
    let cells: [u32; 1] = [0u32];
    assert try_acquire(&sim.cpu, &cells, 0, 64);
    // held: a second acquirer spins out its budget and gives up
    assert !try_acquire(&sim.cpu, &cells, 0, 8);
    release(&cells, 0);
    assert try_acquire(&sim.cpu, &cells, 0, 64);
}

$ kola test spin.kl
spin.kl: test the_lock_is_taken_then_released ... ok
1 passed, 0 failed (interpreted, JIT backend)
native tests: 1 ran, 0 fail(s)

$ kola report checks spin.kl
  proven   Atomic::cas32_acquire(cells, i)  [proved i < cells.len from req+guards]
  proven   tries + 1u32  [sum bounded by width]
  proven   Atomic::store32_release(cells, i)  [proved i < cells.len from req+guards]

Compiled freestanding, the hint is pause on x86-64 and yield on aarch64. On mips it is nothing at all: mips has no spin hint, and emitting its wait instead would park a core that is supposed to be watching for the lock.

Privileged registers

CPUs keep their configuration in special registers that ordinary code cannot touch: whether paging is on, where the interrupt table lives, which features are enabled. Each architecture names them differently, and kola keeps each architecture's own shape:

• aarch64: sysreg_read(enc) -> u64 and sysreg_write(enc, v). enc is the system register's encoding and must be a compile-time constant, because the instruction (mrs/msr) carries the register number inside the instruction word.

• x86 MSRs (model-specific registers): rdmsr(id) -> u64 and wrmsr(id, v). Here id may be a run-time value, because rdmsr reads the index from a register.

• x86 control registers: cr_read(n) -> u64 and cr_write(n, v). n is a constant, one of 0, 2, 3, 4 or 8. A reserved number traps rather than reading 0, because a control register that silently reads 0 looks like "paging is off" to boot code.

• mips CP0: cp0_read(reg, sel) -> u64 and cp0_write(reg, sel, v), with reg and sel constant.

The constant requirement is a property of code generation, so kola check accepts a run-time selector and the freestanding build refuses it:

pub fn read_dynamic(cpu: &Cpu, enc: u64) -> u64 !{hw} {
    cpu.sysreg_read(enc)
}

$ kola build --freestanding sysreg.kl -o out
codegen: native codegen: `sysreg_read(...)` in `read_dynamic`: the register selector must be a compile-time constant (it is baked into the instruction encoding) — pass a literal or a `const`, not a runtime value (design-kernel-lowlevel.md §2.1b)

x86 also has descriptor tables, the in-memory tables that describe segments and interrupt handlers. lgdt(base, limit), lidt(base, limit) and ltr(sel) load them; sgdt() and sidt() return (base, limit) and str() the task register. The reads return a tuple because each is one instruction that fills several registers; two separate operations would run it twice. cpuid(leaf, sub) returns the four result registers. lgdt_win(w), lidt_win(w) and cr3_write_win(w) take a RamWindow instead of a raw address: the runtime reads the base out of the window, so the address never appears in kola source, and the limit is computed as len - 1.

In the simulator, one keyed register file backs all of these. A register nobody wrote reads 0:

// One keyed register file backs all three surfaces; unwritten reads 0.
test the_register_files_round_trip(mut sim: Sim) {
    // aarch64: SCTLR_EL1 (S3_0_C1_C0_0) has encoding 0xc080, a constant
    assert sim.cpu.sysreg_read(0xc080) == 0;
    sim.cpu.sysreg_write(0xc080, 0x1234);
    assert sim.cpu.sysreg_read(0xc080) == 0x1234;

    // x86: IA32_EFER is MSR 0xC0000080; the index may be a runtime value
    sim.cpu.wrmsr(0xC0000080, 0x500);
    assert sim.cpu.rdmsr(0xC0000080) == 0x500;

    // x86 control registers: the number is a constant, one of 0/2/3/4/8
    sim.cpu.cr_write(4, 0x20);
    assert sim.cpu.cr_read(4) == 0x20;

    // mips: CP0 is keyed on (reg, sel); another sel is independent
    sim.cpu.cp0_write(10, 0, 0xABCD);
    assert sim.cpu.cp0_read(10, 0) == 0xABCD;
    assert sim.cpu.cp0_read(10, 1) == 0;
}

test descriptor_tables_and_cpuid(mut sim: Sim) {
    sim.cpu.lgdt(0x8000, 0x37);
    let (base, limit) = sim.cpu.sgdt();
    assert base == 0x8000;
    assert limit == 0x37;
    let (a, b, c, d) = sim.cpu.cpuid(0x4000_0000, 0);
    assert a == 0 && b == 0 && c == 0 && d == 0;   // an unqueried leaf answers all zero
}

On the wrong architecture a register operation is refused by name in the freestanding build, never compiled to a silent no-op.

Virtualization

A hypervisor runs whole operating systems as guests. On Intel CPUs the hardware support is called VMX: the hypervisor enters a special mode (vmxon), and describes each virtual CPU in a memory structure called the VMCS (virtual machine control structure), which holds the guest's registers, the reasons it may exit back to the hypervisor, and so on. AMD's equivalent is SVM, with a structure called the VMCB.

kola reaches VMCS fields through one pair of operations, vmread(enc) -> u64 and vmwrite(enc, v), rather than through a hundred and fifty named ones. The field encodings are constants in std::machine::vmcs (GUEST_RIP, VM_EXIT_REASON, HOST_RIP, ...). When the encoding is a constant, its validity is checked at compile time:

pub fn bad(cpu: &Cpu) -> u64 !{hw} {
    cpu.vmread(0x7000)
}

error[card §7]: `vmread`: 0x7000 is not a valid Intel VMCS field encoding — a well-formed encoding sets no bit outside 0x6FFF (bit 12 and bits 15-31 are reserved MBZ)
   = help: use a field from the std::machine::vmcs table (GUEST_RIP, VM_EXIT_REASON, …), or a real Intel SDM Vol 3 App-B encoding — this constant could only ever fault the instruction

An encoding computed at run time (a loop that saves a list of fields, say) is checked at run time instead.

Around that pair is the rest of the lifecycle: for VMX vmxon, vmxoff, vmclear, vmptrld, vmptrst, invept and invvpid; for SVM vmsave, vmload, stgi, clgi, vmmcall and invlpga. All are x86 only, !{hw}, and take &Cpu. The instruction set is closed, so kola provides the whole family rather than the subset one program happened to need. invept and invvpid flush cached address translations for the guest (EPT is the guest's second level of page tables, VPID a tag on its entries in the TLB, the CPU's cache of address translations).

use std::machine::vmcs;

// Per-CPU Intel VMX bring-up: enter VMX root mode, load a VMCS,
// set the guest's start address, flush EPT and VPID entries, leave.
fn vmx_bringup(cpu: &Cpu, vmxon_pa: u64, vmcs_pa: u64, eptp: u64) !{hw} {
    cpu.vmxon(vmxon_pa);
    cpu.vmclear(vmcs_pa);
    cpu.vmptrld(vmcs_pa);
    cpu.vmwrite(vmcs::GUEST_RIP, 0xffff_0000);
    cpu.invept(1, eptp);           // type 1: single-context EPT flush
    cpu.invvpid(2, 1, 0);          // type 2: single-context VPID flush
    cpu.vmxoff();
}

test the_lifecycle_leaves_the_vmcs_fields_alone(mut sim: Sim) {
    vmx_bringup(&sim.cpu, 0x1000, 0x2000, 0x3000);
    assert sim.cpu.vmread(vmcs::GUEST_RIP) == 0xffff_0000;
    assert sim.cpu.invept_single(0x3000);
    assert sim.cpu.invept_count() == 1;
}

In the simulator the lifecycle operations are no-ops or small flag changes (VMX root on and off, a current-VMCS pointer, the global interrupt flag). The VMCS field file is the interesting state, and the test checks that the lifecycle leaves it alone. invept_single(eptp) -> bool is a convenience beside the raw invept: single-context, with the instruction's failure bit returned as a value. invept_count() counts flushes so a test can assert "N page-table changes produced N flushes". It works in both simulated executors and is refused in a freestanding build, where a count of zero would make such an assertion pass without meaning anything.

The instructions that actually enter the guest (vmrun, vmlaunch, vmresume) are not in kola. Entering a guest needs the hypervisor's own register save and restore wrapped around the instruction, which no generic operation can provide, so that step lives in code outside kola. Everything that prepares and tears down virtualization is in kola.

Caches, TLBs and fences

A CPU keeps recently used memory in caches, and recently used address translations in the TLB (translation lookaside buffer). Most of the time this is invisible. It stops being invisible when something other than the CPU reads memory (a DMA engine), when page tables change, or when the CPU writes instructions it will execute. The maintenance operations on Cpu handle those cases: tlb_flush_all(), tlb_flush_page(va), dcache_clean(va), dcache_flush(va), icache_invalidate(va).

A fence (or memory barrier) is an instruction that stops the CPU from reordering memory operations across it. Modern CPUs reorder loads and stores for speed; a fence is how you say "everything before this must be visible before anything after it". fence() orders memory between cores; fence_sys() is the whole-system barrier that also covers devices. All of these are no-ops in the simulator, and they are freestanding operations.

You need fewer explicit fences than you might expect. An access through an MmioWindow is already ordered as the device sees it, so "write a descriptor into a RamWindow, then write the doorbell register" needs no barrier between the two. The DMA cache operations for a range of memory, dma_writeback and dma_invalidate, live on RamWindow because they apply to a range, not to the CPU; see the hardware windows chapter.

Atomics

When two cores share memory, an ordinary read-modify-write such as x = x + 1 is not safe: both cores may read the same old value, and one increment is lost. An atomic operation does the whole read-modify-write as one indivisible step that no other core can interrupt. Atomics are the building blocks of locks, counters and lock-free queues.

kola has 18 atomic operations, all !{hw}, spelled Atomic::<op>(cells, i, ...). The first argument is a shared slice (&[u32] or &[u64]) and the second an index into it. There is never a reference to a single cell:

• The slice is shared, not &mut, because an atomic is exactly the kind of write that is safe through a shared reference. That is what separates it from a plain write.

• kola has no way to read through a reference to a single integer, so a cell is named by slice and index. A useful consequence: a misaligned atomic cannot be written at all, since indexing a u32 slice always lands on a 4-byte boundary.

Both the width and the ordering are in the operation's name. Ordering says what other memory operations are guaranteed to be visible around the atomic. Relaxed guarantees only that the operation itself is atomic. Acquire (on a load) means nothing after it may be moved before it, which is what you want when taking a lock. Release (on a store) means nothing before it may be moved after it, which is what you want when giving a lock back, so the other core sees your writes before it sees the lock free.

• load: load32_relaxed, load32_acquire, load64_relaxed, load64_acquire

• store: store32_relaxed, store32_release, store64_relaxed, store64_release

• read-modify-write, each returning the previous value: add32_relaxed, add64_relaxed, or32_relaxed, or64_relaxed, and32_relaxed, and64_relaxed, swap32_relaxed, swap64_relaxed

• compare-and-swap: cas32_acquire, cas64_acquire, taking (cells, i, expected, new)

Compare-and-swap (CAS) writes new only if the cell currently holds expected. kola's CAS returns the value it observed, not a bool. If it equals expected, you won. If not, you already have the current value and don't need a second load, which could be stale by the time it runs.

pub fn bump(cells: &[u64], i: usize) -> u64 !{hw}
    req i < cells.len
{
    Atomic::add64_relaxed(cells, i, 1u64)   // returns the previous value
}

pub fn try_latch(cells: &[u32], i: usize) -> bool !{hw}
    req i < cells.len
{
    Atomic::cas32_acquire(cells, i, 0u32, 1u32) == 0u32
}

test the_latch_wins_exactly_once {
    let cells: [u32; 1] = [0u32];
    assert try_latch(&cells, 0);
    assert !try_latch(&cells, 0);
}

test cas_reports_what_was_really_there {
    let cells: [u32; 1] = [0u32];
    let won = Atomic::cas32_acquire(&cells, 0, 0u32, 7u32);
    assert won == 0u32;
    let lost = Atomic::cas32_acquire(&cells, 0, 0u32, 9u32);
    assert lost == 7u32;               // the value that was there, not the guess
    assert Atomic::load32_relaxed(&cells, 0) == 7u32;
}

test add_returns_the_previous_value {
    let cells: [u64; 1] = [0u64];
    assert bump(&cells, 0) == 0u64;
    assert bump(&cells, 0) == 1u64;
    assert Atomic::load64_relaxed(&cells, 0) == 2u64;
}

$ kola test lock.kl
lock.kl: test the_latch_wins_exactly_once ... ok
lock.kl: test cas_reports_what_was_really_there ... ok
lock.kl: test add_returns_the_previous_value ... ok
3 passed, 0 failed (interpreted, JIT backend)
native tests: 3 ran, 0 fail(s)

The set is small on purpose. There is no sequentially consistent ordering (the strongest, slowest kind) and no "weak" CAS that may fail spuriously; the operation handles that retry itself.

Atomics over a window

The cells argument may also be a RamWindow, or its atomic-only attenuation AtomicWindow (w.atomic()), so the same operations reach memory shared with another core or a device. With a window the index is still a cell index, not a byte offset, so that Atomic::add32(x, i, v) means the same thing whatever x is; the bound is w.len / 4 for 32-bit cells.

test atomics_over_a_window(mut sim: Sim) {
    match sim.mmio.ram(b"roster") {
        Some(w) => {
            let a = w.atomic();
            let prev = Atomic::add32_relaxed(&a, 1, 5u32);   // cell 1 = bytes 4..8
            assert prev == 0u32;
            assert w.read32(4) == 5u32;
        }
        None => { assert false; }
    }
}

This test needs a grant: kola test aw.kl --ram-window roster=0x0:0x40.

What the compiler emits

kola does not write assembly for atomics. It emits the C compiler's __atomic builtins, which need no header (so they work in a freestanding build) and choose the right instruction for each architecture. It does not use C11's <stdatomic.h>: a freestanding build may not have it, and an _Atomic type could change the layout of memory that another core reads as plain bytes.

On mips, for example, the 32-bit CAS compiles to a load-linked/store-conditional pair. ll loads a value and starts watching the address; sc stores only if nobody else wrote the address in between, and reports whether it succeeded:

	ll	$1, 0($4)
	...
	sc	$2, 0($4)
	...
	sync

A 32-bit target such as 32-bit mips has no single instruction for a 64-bit atomic. The compiler would call a helper library instead, and a freestanding image cannot link one. So the 64-bit operations are refused there at compile time, with the repair in the identifier:

pub fn bump(cells: &[u64], i: usize) -> u64 !{hw}
    req i < cells.len
{
    Atomic::add64_relaxed(cells, i, 1u64)
}

$ kola build --freestanding w64.kl -o out
$ clang --target=mipsel-linux-gnu -ffreestanding -DKOLA_FREESTANDING -Iout -c out/w64.c
out/w64.c:799:12: error: use of undeclared identifier 'k_atomic64_UNAVAILABLE_ON_ILP32__use_the_32_bit_ops'
  799 |     return K_ATOMIC64(__atomic_fetch_add(((uint64_t*)((cells).ptr) + (/*IR:discharged*/(i))), ...

The 32-bit operations still compile for that target. The same error line also shows what req i < cells.len bought: the index reaches the C code marked /*IR:discharged*/, with no bounds check, because the bound was proven.

What the simulator cannot tell you

The interpreter runs one thread at a time, so it is an oracle for values and for nothing about ordering or coherence. A release store runs there as a plain store, a fence does nothing, and a compare-and-swap is a read followed by a write with nothing that could interfere in between. Every agreement between kola run and kola run --native in this chapter is a statement about which numbers came back.

Three things fill the gap:

• Read the generated assembly. pause against yield against nothing is invisible to any test of values. The wfe problem above could only be seen in the instructions.

• Run on the target hardware, with more than one core where ordering matters. A multi-core spinlock test on the real chip is the evidence that the atomics are right; passing hosted tests are not.

• Remember that comparing two executors cannot find a bug they share. If both executors get a check wrong in the same way, they agree, and only an assertion about the expected value fails.

A measurement in this area means something only if it says which machine produced it. x86 orders stores more strictly than ARM, so code that is wrong on ARM can pass every test on an x86 laptop.