sysk, in levels
sysk is a small operating system for a RISC-V machine, written together with its own language, sysp. Before the machine runs any of it, sysp proves that the kernel and every task keep their contracts. These pages explain each part, from the hardware up, so you can find your way around the code.
Six levels
Read the stack from the bottom: each level runs on the one below it and is checked by the tools on the right. Select a level to see what lives there and which files hold it. The colour on the left edge says who vouches for the code: proven by sysp, trusted because nothing checks it, or hardware.
Checked before it runs
One typed line, through every level
Someone types greeter at the shell's prompt and presses Enter, and greeter: hello from a job comes back. Here is everything that happens in between, level by level. Step through it, or play it.
The ideas sysk tests
sysp proves that no task reads past a buffer, breaks a contract, or touches what it was not handed. Tasks still run in user mode behind PMP, so a bad access in a task's compiled code, or in assembly it calls, is caught too.
A task's memory is its stack and a heap the kernel hands it. Messages are copied into the kernel and out again, so no task ever sees another's memory.
A task can act only through values it was handed: channel handles, a heap, a device. Nothing else can be named, forged or copied.
A channel carries exactly n messages of b bytes, then closes; or it is a stream, which ends when its sender closes it. Sending once too often or closing too early is a compile error.
system.sysk says which tasks run and what each holds. It is checked, turned into code, proven with the rest, and model-checked for deadlocks.
Coming from Unix
sysk has no POSIX. What a task may do is one short file, the interface, version 0.1.0, and what a system is, is another, the manifest. Neither is a standard with many implementations: the tools check every task against both before anything is built. Where the familiar parts went:
| In Unix | In sysk |
|---|---|
| system calls | the interface's calls: . From a task each is a gate, a trap into the kernel. |
| libc | the interface's library: code that runs in the task itself, on its own heap and handles. |
| man pages | the contracts: every call says what it needs and what it promises, and sysp proves each call keeps them. |
a process, fork, exec | a task: a sysp function, listed in the manifest. No task is created at run time; a job (sysk 017) runs catalogue programs in slots the manifest set aside, checked before it starts. |
file descriptors, open | handles a task is handed when it starts: channel ends, a heap, for a driver its device. There are no global names to open. |
| pipes | channels: exactly n messages of b bytes, then closed; or a stream, any number until its sender closes it. Sending once too often, or closing before the end, does not compile. |
/dev, mmap of registers | a Device: the device's page of registers as a capability, which only files in drivers/ may name. Its driver reads and writes registers by offset, each proven inside the page. |
| a block device, files | a disk driver task (sysk 023) that reads and writes 512-byte sectors for a client over channels; what the disk may touch in memory is proven (Storage). The kernel serves its own state as files (sysk 028: /tasks, /channels, /time), through one small protocol every tree speaks (Files), and a file server task keeps a tree on the disk in the same protocol, every change copy-on-write and made whole by one root write (sysk 029, Files on the disk); a job can be lent part of it while it runs (sysk 031, Files for jobs). |
the shell, init, permissions | the manifest, system.sysk: which tasks run and what each holds, fixed before boot. The code that hands it out is the wiring, generated from it. |
| the terminal, termios | nothing in sysk: lines are edited where they are shown, by the person's terminal (make run) or a postterm window (make attach). The terminal task turns bytes into lines and writes output a whole line at a time; Ctrl-D on an empty line ends input. |
| exit status | the machine's: 0 when every task finished, 1 a failed test, 2 a panic, 3 a trap. |
select, poll | alt: wait for the first of a task's sources (its receiving channels, room on its streams, its device), with a guard on each; it returns which. |
The interface's version moves its MINOR number when a task written against the last version may no longer verify: a name removed or renamed, a contract that asks more or promises less. Anything else moves PATCH.
How to read these docs
If you are new, read How sysk is proven next: it explains the one idea everything else leans on. Then follow the pages in order, from Boot upward. Every page ends with In the source: the files it explains, with each definition's comment and contract as they are in the code today. Words you don't know are in the Glossary.