User mode and PMP
sysp proves tasks keep to their own memory. The hardware enforces it as well: tasks run in RISC-V user mode, where Physical Memory Protection lets each one touch only its own stack, its own heap, the shared code and constants, and its device if it holds one. Calls into the kernel are traps.
Two privilege modes
RISC-V has machine mode (everything allowed), supervisor mode (for kernels that use the MMU) and user mode. sysk uses no MMU and only two modes: the kernel's scheduler and channels, and the boot and trap assembly, run in machine mode; tasks run in user mode, together with the library code they run on their own memory (the heap allocator, closing a receiving end) and a few assembly helpers (the gate stubs, the heap's block views, and since sysk 023 the loads and stores load8, load32, store8 and store32 a driver reaches its device's registers with). Machine mode can reach everything; user mode can reach only the address ranges PMP gives it, and cannot touch control registers at all. Breaking either rule traps into machine mode, and sysk stops: sysk: task fault, status 3.
Why both proofs and hardware? The proofs hold if the compiler, the assembly and every task are right. PMP catches what they assume away in code that runs in a task, such as a compiler bug in a task's code or a store in assembly that sysp never sees. It does not guard the kernel: the entries are not locked, so machine mode is not bound by them. Nor does it bind a device that reads and writes memory itself, the disk (sysk 023): PMP checks the CPU's accesses, so what the disk may touch is proven instead (Storage). The tests include a task that writes to kernel memory through assembly, and one that writes to the UART without holding it. Both must fault.
What each task may touch
PMP has numbered entries, each covering an address range with read, write and execute permissions. On an access from user mode, the lowest-numbered entry that matches decides; if none matches, the access faults. sysk sets the addresses of entries 0 to 2 once at boot; at every switch it loads the addresses of 3 to 7 and the permissions of all eight (pmpcfg0) from pmp_regions. Pick a task, then try an access.
| Entry | Mode | Range | Allows | What it is | Set by |
|---|
Entries 0, 3 and 5 are off: in TOR mode ("top of range") an entry covers from the previous entry's address up to its own, so each pair of addresses makes one range. Entry 7 is NAPOT, one naturally aligned power-of-two range, which is why a device's page must be aligned to its size; since sysk 023 every page is 4096 bytes, the size the driver's register accesses are proven against (IO and drivers). Addresses come from the last make docs; a heap's words come from the boot arena at boot, so their address is known only then.
A fault kept
A task that breaks a rule, a store PMP denies or an instruction user mode may not run, used to stop the machine with one line that named nothing (sysk 105 changed it). Now trap.S hands the kernel the cause and where, as an offset into the kernel's code, and on-fault keeps four words in the task's slot: the cause, the offset, the tick, and how many faults it has had. The task never runs again; every channel it sends on ends: a stream's reader sees the end, and an exact channel's gets each message the task still owed empty, so neither waits for it (Channels). A job's task ends its job as a stop does, and its slot starts again at the next job. cat /sys/task/NAME/fault reads (fault (count 1) (cause store-access) (at render 312) (tick 4121)), and the task's status says faulted. Registers and the task's memory stay where they are. A trap from machine mode still stops the machine: that is the kernel's own bug.
The name comes from a table the build makes. make links the kernel twice: tools/syms.rkt reads the first link's functions with llvm-nm and writes them as data, build/functions.S, in a section after .data, which the second link adds. Only data after the code moves, so every function is where the first link put it and every offset holds. arch/rv64/symtab.S reads the table a word at a time; a kernel linked once, as a test's is, has an empty table and shows the offset alone. Hubris keeps a fault per task the same way, and leaves restarts to its supervisor; restarting is not here yet (services.md). The boot test's breaker (tests/fault) faults on purpose: it calls break.S's csrr mstatus, which user mode may not run.
The trap path
Every way from user mode into the kernel goes through trap_entry in arch/rv64/trap.S. Pick a cause and step through it.
mscratch does double duty: while a task runs it holds that task's kernel stack, and while the kernel runs it holds 0. The first instruction swaps it with sp; if the result is 0 the trap came from machine mode, which is a kernel bug, and sysk stops with sysk: trap.
Gates
In a task, a call to send cannot just jump to the kernel's send: that code runs in machine mode. When sysp compiles user code it turns each call to a gate into a call to a stub, and tools/gates.rkt writes the stubs from the interface: li a7, n; ecall; ret, plus the table trap.S dispatches through. The gates are the interface's calls, the devices' one (device-ack), and the calls only the generated wiring makes (its wiring clause: task-main's finish, and the job slots' runners' job-await, job-bound and job-done, sysk 017), which no task may name. The arguments stay in registers, so one dispatcher serves every gate, and the real functions are the ordinary sysp ones, contracts and all. The proofs do not change.
| a7 | Gate | Stub | Runs in machine mode |
|---|
The interface: what a task may name
kernel/interface.sysk lists every name a task may use that it does not define itself. tools/interface.rkt reads each file in svc/, prg/, drivers/ and lib/, as sysp expands it (the struct, put and get a byte layout makes are the file's own names, sysn 034), and rejects any that names something else, even a public kernel function. The kernel is built only if every file passes.
The list starts with its version, now 0.1.0. Below 1.0.0, the MINOR number moves when a task written against the last version may no longer verify: a name removed or renamed, a requires made stronger, an ensures made weaker. Anything else, such as a new call, moves PATCH. tools/interface.rkt rejects a list without one.
Since sysk 028 it lists the files protocol too: the call sys-serve, the library that builds requests and reads replies (fs-request, fs-status, …), and the protocol's constants, from the message's sizes to each header field's offset (Files). sysk 029 added what a server needs as well (0.6.0): fs-begin, which checks a request's header, fs-error, path-ok, the statuses a disk can give (no-space, io-error, busy, already-exists, not-empty) and the open modes for writing, so the disk's server is ordinary user code (Files on the disk). sysk 031 added a service's names (0.6.1): the type Service, its predicates, the calls service-open and service-close, the library's service-reply and service-end, and the protocol's op-lend (Files for jobs). sysk 032 added jobs-output (0.6.2), which says a receiving end is its right's jobs' output, so a launcher can hand that end to a loop of its own, as the shell does with a job in the background (The shell). sysk 033 added a read that waits (0.6.3): mode-wait, and the request's at-since and at-wait (Reads that wait).
sysk 036 made a task's record in a job's table longer, for its arguments (0.7.0, MINOR: a launcher written against 0.6 builds a table the check now refuses); the table's layout is in the list as constants (task-bytes, job-bytes, …), and the slots' runners read arguments through one more wiring gate, job-arg. sysk 046 added a node's kind, type-stream (0.7.1), for a file that never ends, such as /dev/rng (Devices as files). sysk 052 added virtio-reset to the device page (0.7.2), for a buffer a device may never give back, such as one lent to receive a frame (The network). sysk 059 added service-stamp to the library (0.7.3): a lease's stamp, its job's need in the service's rights words, by which the server caps what it lent (Within its need). sysk 063 added a tree's names (0.7.4): the type Tree, its predicates, the calls tree-recv and tree-send, the library's tree-who, tree-ended and tree-end, and the constant tree-max, so a server takes the requests of every holder of its tree (Several clients, one server). sysk 064 added tree-root to the library (0.7.5): the directory a holder's mount names, where its server roots it (A holder's root). sysc 009 added alloc-w32 and dealloc-w32 to the library (0.7.6): a buffer of 32-bit words from a task's heap, for sysc's generator in the rng driver (Memory), since sysk 091 alloc's bytes retyped, with the same contract. sysc 014 added a node's kind, type-function (0.7.7): a library part's function in /prg/PART, run as a command (Files). sysk 074 added the call job-stop (0.7.8): it ends a running job wherever its tasks are, so a launcher can stop one (The shell).
It also checks that every name in the interface exists in the kernel, so the list cannot go stale, and that no user code has an atomic block: the kernel never holds the timer off a task.
Still trusted
This is step one of two. The kernel still trusts what a task passes to a gate, a handle, a buffer, the kernel pointer k, because sysp proved every task passes good ones. A task not written in sysp would need a kernel that checks every argument. That is a later feature; until then the list of what is assumed is in The trusted base.