The system · L5

The manifest

One file says what the system is: system.sysk lists the channels and, for each task, the function it runs and exactly what it is handed. Change the file and you have a different system, with no change to any code, still proven and model-checked.

system.sysk and the system it describes

Select a task line or a box to see what it holds. Tasks are blue (purple for the one holding a device); channels are amber, with their message count, size and depth.

What a line means

Written	Means
`(log (messages 5) (bytes 64) (depth 2))`	a channel carrying exactly 5 messages of exactly 64 bytes; up to 2 can wait in it at once (1 if no depth is given)
`(keys (bytes 1) (depth 4))`	a stream: no message count, so its one sender sends any number of messages and then closes it (sysk 015)
`(task terminal …)`	a task that runs the sysp function `terminal`; the same function can be several tasks (the pipeline system's two spinners)
`(heap 128)`	128 bytes of heap blocks, a multiple of 8 (the nine words of free-list heads come on top); with its two stacks, the task's only memory
`(tx lines)` · `(rx lines)`	a send handle or the receive handle for `lines`; a task's receiving ends, then the streams it sends on, then its device, then its clock are its sources for `alt`, numbered in that order
`(tx log 5)`	a sender on `log` with a share of 5 messages; with several senders, the shares add up to the channel's count
`(device uart)`	the UART, a device from `arch/rv64/devices.sysk`; the task is its driver, and the device's interrupts reach it alone
`(clock)`	a `Clock`: the right to read the time, sleep, and set an alarm (sysk 022; Time); any number of tasks may hold one
`(sys)`	a `Sys`: the right to read the kernel's tree of files, its tasks, channels and time (sysk 028; Files); any number of tasks may hold one. Its task names are the manifest's: the function's, numbered when several tasks share it, and `slot-N` for a pool's slots
`(namespace)`	the task's namespace as text, read-only: `(PATH SOURCE) …`, each tree named by the `alt` source of room on its requests, `sys` for the kernel's (sysk 053; Files). The manifest must say it:
`(namespace shell ("/" fs-ask) ("/dev" dev-ask) ("/sys" sys))`	where `shell` finds its files: each path, `/` or `/NAME`, is the tree of the task that receives on the stream named, one the task sends on, or the kernel's; one mount is `/`, and a path is under the longest that starts it. A third word names a tree the server serves besides its first: `("/prg" sys prg)`, the kernel's programs (sysk 057). `/sys/task/shell/ns` shows it
`"spin-a"`	a string argument
`(serves NAME)`	a `Service`: the right to serve the jobs clause's service NAME, the server's ends of its two pool streams while a job that binds them runs (sysk 031; Files for jobs); one task serves each service
`(service NAME (bytes b))`, in the jobs clause	two pool streams, NAME-ask and NAME-reply, of b bytes, between a job and the task that serves NAME. There may be several, `files` and `talk` (sysk 058): a job binds the one whose server's tree holds what it was lent
`(catalogue)`	the catalogue as a text, read-only: each program with its parameters, the pool, the launcher's output, and each program's arguments (sysk 018: the shell reads what it can run from it; 036: and what it may be told)
`(jobs jout)`	the right to start jobs in the pool, reading their output on its channel `jout`: the launcher (sysk 017); `jout` is also its last `alt` source, so it can read a job's lines while it waits for other things (sysk 032)
`(jobs (programs …) (slots n (heap b)) (channels …))`	a pool for jobs: the programs they may run, each a name or, with arguments, `(name (argument default) …)` (sysk 036), n tasks that run them, and channels with fixed sizes and depths but no counts; see Jobs. A program that takes a `Clock` after its heap is handed one: time costs nothing to grant (sysk 058, `ping`)

Arguments are passed in order after the kernel, so they must match the function's parameters, and the function's precondition must hold for them. A spinner that logs 5 lines needs a share of 5; a terminal that allocates four buffers needs a heap big enough for all four; a task that says (tx-stream out) needs a stream.

From manifest to proven code

tools/wire.rkt checks the manifest. Within the kernel's limits: 1 to tasks and 1 to channels (sysk 027; 8 and 8 before), messages of 1 to bytes, depths of 1 to . Every channel has one receiver and one sender, or several senders whose shares add up; a stream has one sender and no share. A device exists on the platform, has one holder, and an interrupt source of 1 to 31. Heaps are whole words. No task gets the kernel's console. With a jobs clause: one launcher, pool channels named by no task clause, and catalogue programs whose contracts the job check can judge, whose heap fits a slot and which do not use alt (read from the user code, which the build passes it). A namespace names one task handed (namespace), mounts / once, and serves each path by a stream the task sends on or by sys (sysk 053).
It generates build/wiring.sysp: the task and channel counts, where each channel's ring sits in the kernel's mail buffer, each task's heap and device page, which task owns which interrupt source, each task's sources for alt, each task's namespace as the kernel shows it (task-ns), and start-task, which hands each task its arguments. With a pool, also the tables jobs are judged by and each slot's runner (Jobs). wire.rkt --uses lists the files that hold the functions the manifest names, the files those call into (sysk 033), and every library in lib/, so the build compiles only the tasks this system runs.
sysp proves the wiring with everything else. If a manifest's numbers disagree with a task's contract, the call in start-task fails to verify, and there is no build.
tools/model.rkt checks the whole system can always finish, from the same manifest and the tasks' code. See Model checking.

Here is the heart of the generated code for this manifest, start-task. Handles are minted with the Wire, which only task-main holds, so this is the only code that can make them:

Manifests that must be rejected

Each of these is a test: wire.rkt must refuse it with the message shown. They are read from tests/manifest/.