Kernel code

Nova is designed to run inside an operating system kernel as well as in user programs. Its kernel support is developed against CosmoOS, a kernel written in C, where Nova code runs as kernel components and as loadable modules on x86-64 and AArch64. Nothing in it is specific to CosmoOS: the same mechanisms fit any C kernel or firmware.

The freestanding profile

--profile freestanding (or profile = "freestanding" in a package's manifest) compiles for an environment without a C library or an operating system:

• there is no main: the entry points are @export functions that the environment calls;
• everything that needs a hosted runtime is unavailable, and naming it is an error: Console, files, sockets, SystemHeap and the collections built on it;
• memory comes from an allocator the environment provides, written in Nova over the kernel's C functions;
• --no-float (or float = false) rejects floating point, for code compiled without FP registers.

novac build --emit obj then writes one relocatable object, with only the undefined symbols the environment provides, ready for the kernel's own build to link.

/// A CRC-32C over `n` bytes at `data`, for C callers.
/// Safety: `data` points to `n` readable bytes, as the C prototype's contract says.
@export("crc32c_sum")
unsafe fn crc32c(data: *u8, n: usize) -> u32 {
    return checksum(Slice.fromRaw(data, n));
}

fn checksum(bytes: Slice<u8>) -> u32 {
    var crc: u32 = 0xFFFFFFFF;
    for (b in bytes) {
        crc = crc ^ (b as u32);
        for (bit in 0..8) {
            let mask = if ((crc & 1) != 0) 0x82F63B78u32 else 0u32;
            crc = (crc >> 1) ^ mask;
        }
    }
    return crc ^ 0xFFFFFFFF;
}

The unsafe part is confined to the boundary: the exported function turns C's pointer and length into a slice under a stated contract, and everything behind it is safe, checked Nova.

Context effects

Kernel code runs in contexts with rules: while a spin lock is held it must not sleep; in an interrupt handler it must not sleep or allocate. Nova checks these rules at compile time, across function calls:

• an operation's effects are sleep (it may block) and alloc (it may allocate), inferred for every function from what it does and calls, its destructors included;
• @effects(…) declares what a C function may do, or bounds what a Nova function may do;
• @context(atomic) on a function forbids sleep in it; @context(irq) forbids sleep and alloc;
• @context(atomic) on a struct makes holding one an atomic context: a spin-lock guard.

@header("kernel/sched.h")
extern "C" {
    @effects(sleep)
    fn cosmo_sleep_ms(ms: u32);
}

/// Holding a spin-lock guard makes the code that runs meanwhile atomic: it must not sleep.
@context(atomic)
struct SpinGuard { cpu: u32; drop {} }

/// Safety: cosmo_sleep_ms has no preconditions; it may sleep.
fn backOff() { unsafe { cosmo_sleep_ms(1); } }

fn update(counter: borrow mut u64) {
    let guard = SpinGuard { cpu: 0 };
    counter += 1;
    backOff(); // sleeps while the guard is held
}

main.nova:17:5: error[N0295]: a 'SpinGuard' is live here, which makes this an atomic context (type-system.md §32.3), but this may sleep: it calls 'backOff', which calls 'cosmo_sleep_ms', declared @effects(sleep)
   |
17 |     backOff(); // sleeps while the guard is held
   |     ^^^^^^^^^^

This proves that Nova code does nothing its context forbids, given that the @effects of C functions are declared correctly. It does not prove the absence of deadlocks or lock-order inversions: the kernel's own lockdep stays the check for those.

Hardware registers

lib/core provides Volatile<T>, a cell read and written only by volatile accesses, and MmioPtr<T>, the address of memory-mapped registers. Making an MmioPtr is the one unsafe step; register access through it is safe.

@repr(C)
struct UartRegs {
    data: Volatile<u32>;
    status: Volatile<u32>;
}

struct Uart {
    regs: MmioPtr<UartRegs>;

    /// Safety: `base` is the mapped address of a UART that no other `Uart` aliases.
    public unsafe fn attach(base: usize) -> Uart => Uart { regs: MmioPtr<UartRegs>.at(base) };

    public fn putByte(borrow mut this, b: u8) {
        while ((this.regs.get().status.read() & 0x20) != 0) {
            Cpu.spinHint();
        }
        this.regs.getMut().data.write(b as u32);
    }
}

Kernel allocators, locks and objects

The CosmoOS integration (in the repository's integrations/cosmoos/) builds the rest from these pieces, in Nova:

• KernelHeap, an allocator over kmalloc/kfree, so Box.createIn(KernelHeap {}, value) allocates kernel memory and returns Err when the kernel has none;
• SpinLock<T>, IrqSpinLock<T> and Mutex<T> that hold the data they protect: the data is reachable only through a guard, the guard unlocks when it is destroyed, and a spin guard is an atomic context;
• KRef<T>, a reference-counted kernel object whose final release may sleep, so dropping one under a spin lock does not compile;
• C kernel state (lists, locks, kernel objects) embedded by value in Nova structs, built in place and never moved;
• a loadable module whose state, init and teardown are Nova.

How these were built and tested inside CosmoOS, including a stress test under lockdep, is in the CosmoOS reports and the profiles.

Next

The novac command.