seL4 for SpacemiT K3

The QSOE 0.3 notes say the K3 is QSOE/N only. That was true of the release set and, for the three days before it, false of the lab: on the evening of 14 September seL4 16.0.0 booted to user space on the SpacemiT K3 — 16 harts, at the first attempt — and by the small hours of the 16th QSOE/L was logged in on it, over the serial line and on the screen, with the NVMe, the USB keyboard and the network attached and, once up, nothing from the kernel on the console at all.

The kernel is k3sel4, version 16.0.0-qsoe-k3-0.2. This post is about what it took, because seL4 16.0.0 could not have booted on this board: the SoC has none of the things the RISC-V kernel assumes, and one thing it does not expect.

seL4 16.0.0 assumes	the K3 has	k3sel4 does
a PLIC	no PLIC anywhere: an S-mode APLIC in MSI delivery mode feeding 16 IMSIC interrup files (the RISC-V AIA)	a driver for both, behind the kernel’s six-function interrupt-controller contract
the SBI v0.1 legacy calls, for everything	a vendor OpenSBI, and a project rule that the legacy extensions are out of bounds	sbi.h rewritten on TIME, IPI, RFENCE, DBCN and SRST; the binary audited for the fingerprint
an elfloader carrying the root task inside the image	mr-bml 1.0 and Multiboot3	a boot stub entered directly, the userland cpio as a module
a DMA-coherent bus	a non-coherent one, with Zicbom	uncached frames through Svpbmt; cache maintenance opened to U-mode
a version file only the manual reads	—	a version derived from the git tag, in the image, on the console and in the boot record

An overlay, not a fork

k3sel4 is not a seL4 tree with changes in it. It is a directory, k3/, laid out like the seL4 tree — 21 files, ~6000 lines of code — and a Makefile that extracts the pristine 16.0.0 tag with git archive, copies k3/ over it and builds. 10 of the files are new and add the platform: the AIA driver, the boot stub, a device tree trimmed to what seL4’s hardware_gen reads. 11 files replace the corresponding upstream ones. make overlay-audit lists every overlay file that shadows an upstream one and refuses a list that differs from the documented one; when seL4 moves on, the work is eleven diffs regenerated, not a rebase.

make check then inspects the binary: the generated device map, the interrupt space, the driver’s state linked in, the version string, and the a7 load feeding every ecall in the image — a li a7,N with N in 0..8 is the fingerprint of a legacy SBI call, and there are none.

No PLIC

The K3’s interrupts are an APLIC in MSI mode — a wired source, when it fires, writes a message into the interrupt file of the hart it is aimed at — and seL4 16.0.0 carries no driver for an APLIC or an IMSIC. What it does carry is a small, clean contract: six static inline functions in one header, selected by the platform, and the architecture code never looks past them. So the driver is a 323-line header, and the design fits in a paragraph. The kernel’s interrupt number is the IMSIC identity, 1 to 511. A wired APLIC source binds to the identity of its own number, so that seL4_IRQControl_GetTrigger() marks an interrupt as a wired source and a plain seL4_IRQControl_Get() means an identity a device will write directly, with the APLIC left alone. Every hart enables every identity in its own file once, at init, so the kernel never writes another hart’s CSRs; a claim is one CSR swap of stopei, which returns the highest pending identity and clears it; a level-sensitive wired source is re-armed on acknowledge. The IMSIC’s 4 MiB is named a kernel device for one reason only — so that its pages are withheld from the device untypeds user space gets. Nobody but the APLIC and a device that trusted software programmed may raise an identity.

The second evening produced the line the design existed for: devb-nvme: interrupts on (AIA EID=384 vector=416 hart=5), the first message-signaled interrupt ever delivered on seL4 by this driver — a device writing its own hart’s file, no APLIC in the path. It also produced a correction. Upstream aims a wired source at the hart that executes the invocation, which is always the root task’s, and nothing on RISC-V ever moves it, so every device trap on the board landed on hart 0 and the thread that serviced it was woken across harts. ARM has GetTriggerCore for this. Here it is one more word on the existing invocation, the core the interrupt thread runs on; a kernel that does not know the word ignores it and behaves as before.

Modern SBI, and nothing else

seL4 talks to its firmware exclusively through the SBI v0.1 “legacy” extensions — timer, console, IPI, remote fences, shutdown, ids 0 to 8 — which QSOE does not permit, whether or not the firmware would still answer them: the project’s firmware floor is OpenSBI 1.6 and its rule is modern extensions only, no probes, no fallbacks. It turned out to be the cheapest change in the tree. Every kernel call site goes through the functions in one header, so the replacement keeps their names and signatures and implements them on TIME, IPI, RFENCE, DBCN and SRST; the legacy clear_ipi becomes a local csrc sip; not one .c file changes. The other legacy speaker in the chain was the elfloader, and the elfloader is gone.

No elfloader

mr-bml enters the kernel by its multiboot3 command directly, with the userland cpio as a module3. The stub behind the Multiboot3 note does what the elfloader used to — finds the root task in the cpio, places it above the kernel, builds the one-page Sv39 table seL4 expects to be running under, starts the other harts through SBI HSM and enters _start with the eight arguments the elfloader passed — and three things the elfloader never did. It honors the loader’s memory map, so every range the firmware keeps (a video controller’s handoff block, runtime services) is carved out of RAM and offered to the root task as device memory rather than reused under it. It leaves the modules where they are, as device untypeds, so the root task maps the cpio instead of carrying a copy of it inside its own image. And it chooses harts rather than counting them: the device tree’s status says which the loader withheld, and the video controller’s handoff block says which one its character generator is running on — the K3 has no engine behind its display, the text console on the monitor is a borrowed hart — so with the screen kept alive the console reads mb3: 15 core(s) on harts 0,2,3,…,15 and the kernel is built for 15 harts.

What the stub learns it hands to the root task in a record next to the device tree: the modules, the command line, which hart runs each seL4 core, the kernel’s version, and — since last night — the date. seL4 keeps no wall clock and the K3’s RTC block counts from zero at every reset; the date that survives a power cut lives in the platform’s management processor, reachable over SBI MPXY from S-mode, which the root task is not. So the stub asks once, before the memory map is carved, and records the answer with the time CSR of the same instant; the root task advances the pair by the ticks since, and nothing in it has to be privileged. The record is append-only and its header’s length is its only version; its limits were set once, generously, before anything freezes. The MBI walk follows Multiboot3 1.0 — every tag two 64-bit words, type then size — so mr-bml 1.0 goes onto the board with this kernel.

Three things the board taught

The first boot was clean. What followed was not free, and the three real findings are worth more than the port.

Six spurious interrupts per boot. A debug-build seL4 prints Spurious interrupt! when it takes a trap it has no record for, and on the K3 it did so six times per boot, always on the first user instruction of a freshly woken thread. The real cause is upstream’s: the RISC-V trap path consumes an IPI in getActiveIRQ() — clears the pending bit and reads the record — before it takes the kernel lock. While the hart then waits for the lock, its holder may send it another reschedule; that one’s record merges with the one already read, as the design allows, but its notification arrives on its own, after the first was cleared, and is taken on the first instruction the woken thread runs. A software interrupt without a record stands for a reschedule at most, so that is what it is reported as now: harmless when nothing changed, and exactly right when a merged kick would otherwise have been lost. Upstream’s assertion on that path, that no remote call is pending without a record, does not hold either — the sender raises the flag before it writes the record. An instrumented boot settled every case in one pass.

A network that linked up and carried nothing. The DesignWare MAC came up, registered, and the harvest stopped dead after two frames while transmit errors climbed. Its descriptors are 16 bytes, four to a cache block, and both the device and the CPU write them, so on a non-coherent SoC the ring must be uncached — no sequence of cache maintenance can be correct for a line two parties are writing. The driver asks for exactly that whenever a cache-block size exists; QSOE/N honors it through Svpbmt; seL4 16.0.0 has no page-based memory types at all, so the ring came back cached. The fix is seL4_RISCV_Uncached, a two-bit pbmt field in the PTE and PBMT = NC on the frame — and one more thing, easy to miss: the frame must be flushed before it is mapped, because zeroing it had left dirty lines that would later land on the device’s descriptors. Nothing of this was ever seen on the Unmatched or the VisionFive 2. Their buses are coherent.

reboot reboots. Stock seL4 can only stop a machine: halt is a shutdown, and on a board that leaves a power cycle between the user and the next boot. A U-mode task cannot ask the firmware itself — its ecall lands in the kernel — so the root task gets a debug syscall for it, handled on the architecture side before the unknown-syscall path the way x86 handles VMEnter: name the caller, hand the machine to the firmware for a cold reset. It is registered last, so every upstream syscall keeps the number 16.0.0 gave it, and QSOE/L uses it only when the boot record says the kernel is this one.

Next

The kernel is done in the sense that matters: the whole of QSOE/L runs on it, on the board, with no kernel noise. What ships is a separate question. 0.3 went out with the K3 as QSOE/N only: its release set was fixed before this kernel was three days old. QSOE/L on the K3 — both kernels on all three boards, which is the shape 1.0 asks for — arrives with the next release; the taskman side of it already runs on the board.

The overlay is at gitlab.com/sel4-frontier/k3sel4; make alone fetches the 16.0.0 tag, applies the overlay and builds kernel.elf, and make check tells you what you got. seL4 16.0.0 is at github.com/seL4/seL4; mr-bml 1.0 ships with QSOE 0.3.