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 16) (depth 4)) | a stream: no message count, so its one sender sends any number of messages and then closes it (sysk 015); each message carries up to 15 typed bytes after a count (sysk 071) |
(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 |
(profile observer) | everything the profile gives (sysk 062; Profiles): first its mount table 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); then, in the profile's order, what it grants and each mount's ends. A task holds one profile at most |
(profile observer (jobs out) (catalogue) (clock) ("/" fsd) … ("/sys" kernel)) | a profile: what a shell holds, by name. Its grants are written as a task's arguments are; each mount, / or /NAME, names the task that serves the tree there, or kernel. One mount is /, and a path is under the longest that starts it. A third word names a tree the kernel serves besides its first: ("/prg" kernel prg), its programs (sysk 057). For a task server it is a directory of its tree, ("/" fsd "/pub"), where the server roots the holder (sysk 064, A holder's root): the holder never names it, and a profile mounts a task server once. /sys/task/shell/ns shows the mounts as written |
(tree (bytes 576)) | a Tree: the task serves a tree, in messages of 576 bytes, to each holder of a profile that mounts it, up to four, in the order of the tasks (sysk 062, 063; Several clients, one server). wire.rkt makes the two streams between it and each holder, named after both, fsd-ask-shell and fsd-reply-shell, and the server holds them all as one handle |
"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) (rights W ...)), 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. Its rights (sysk 059) are the words its server understands: read, write, mutate the files protocol's, any other its own, at most five |
(P ... (needs NEED)), in the programs list | what program P needs (sysk 059): (read NAME), a path it reads, or (talk PROTO NAME), a peer it talks PROTO with, NAME name when the shell is to read the word as a host's name, not an address (sysn 021). A job binds P only to a service whose rights have the need's words, and the lease is stamped with them; a program with none binds no service. Refused: a need on a program with no client's channels, another kind, a need no service can stamp |
(P ... (letter l FLAG)), in the programs list | a letter for P's flag FLAG (sysk 066): (wc (letter l lines)) makes wc -l /notes/x mean (wc /notes/x (lines)). The shell resolves it, from the catalogue. Refused: a letter that names no flag of P's, a letter twice |
PART, in the programs list | a library part's runner (sysc 014): sysc runs the functions ../sysc/commands.sysk names, (commands sha-256), as /prg/sysc/NAME, and sysn its checksum, sum (sysn 014), and frame (sysn 015) (Files). tools/wire.rkt makes the runner from the functions' types, and its argument and its need, (read file), are derived, so it is named alone. Refused: a name in the register of parts (kit/parts.js) for a part that offers no commands, so a program and a part's directory never meet in /prg; arguments or a need written for a runner; a command that is not a public function, has effects, or takes what the shell cannot write, each by name |
(views (HEAD (show F ...) (units (F U) ...) (mark (F V) "T") ...) ...) | how a host shows a record by its head, whoever says it (sysk 066; Views): the fields shown unless the person asks for more, what a number measures (bytes, ms, ns), and text after the first field when field F holds V. (entry (show name) (units (length bytes)) (mark (type dir) "/")) is ls's. Refused: two views for one head, another part |
(views) | the views as text, a line each, read-only: the terminal sends them to a host that speaks syst (sysk 066) |
(names (NAME (ip A.B.C.D)) ...) | what the system's own names mean (sysn 026; By name): /net/cs answers them before it asks DNS. Each entry's fields are named, so a key can join later. Not what may be reached: that is a program's talk need. Refused: a name twice (without case), an address that is not A.B.C.D, more than 512 bytes as text, and names with no task to hold them |
(names) | the names as text, NAME A.B.C.D a line, read-only: netd copies them at start (sysn 026) |
(catalogue) | the catalogue as a text, read-only: each program with its parameters, the pool, the launcher's output, and each program's arguments, needs and letters (sysk 018: the shell reads what it can run from it; 036: and what it may be told; 066: and its letters) |
(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.
Profiles: what a shell holds, by name
A shell holds only its profile (sysk 062; docs/authority.md, part 1). Its line in the manifest lists its heap, the commands it reads and the answers it writes; everything else it may reach is the profile observer: starting jobs, the catalogue, the clock, and its trees, each named by the task that serves it, as /sys/task/shell/ns names them. The person writes no channel between the shell and a server: tools/profile.rkt rewrites each profile, first thing, into the forms the rest of wire.rkt and the model already read, so a profile means the same to the kernel's tables and to the model. For each tree server it makes two streams named after the server, of the size its (tree (bytes N)) says, and hands one end of each to the holder and one to the server.
A profile names servers, not channels, so it reads the same whoever holds it. A server takes the requests of every holder of its tree, through one handle (sysk 063; Several clients, one server): several tasks may hold one profile, and several profiles may mount one server. A server may hold one too: netd's, (profile keyed ("/" rng)), mounts only the entropy driver's tree, so netd can read the key of its TCP sequence numbers and nothing else of the system (sysn 012; The stack's key). A tree server mounted by more than four holders is refused. So is a profile that no task holds, and so are a task with two profiles, a profile named like a task, a program or job, a mount of a task that serves no tree, a tree server no profile mounts, and a task handed itself what its profile gives it.
Rules: what no task or job may ever reach
A (rules ...) clause says what the wiring must never give, and what it must (sysk 061; docs/authority.md, part 5). Nothing moves a handle at run time but a lend within a program's need (sysk 059), so who can ever hold what is decided before anything runs: a task reaches what it is handed; a job running program P reaches the pool's channels its parameters fit, a clock if its contract takes one, and each service it is a client of with the words of its stamp, when its launcher can send to the service's server, since a job is lent only what its launcher holds (sysk 062): in tests/unmounted.sysk the launcher's profile mounts a file server but not talk's, so although ping needs talk, no job reaches it, and (never (reaches job (talk))) passes. wire.rkt decides the rules over the same values it writes the kernel's tables from, so a rule and the table it speaks of cannot disagree. Rules only deny: the wiring is the same with or without them, and a test says so.
| Written | Means |
|---|---|
(never (reaches job (sys))) | no holder the subject names ever reaches the object. A subject is a task's name, a program's, job, any job the pool can run, or a profile's: the tasks that hold it and the jobs they start (sysk 062) |
(must (reaches observer (sys))) | some holder does: a manifest cannot pass its nevers by wiring nothing |
(only (fsd) (tx disk-ask)) | never, for every task and job not listed |
(tx disk-ask) · (device) · (files mutate) | an object, as the manifest writes what a task is handed, or a service with one of its rights; without its last word, any of the kind. A tree's channels are written with the names wire.rkt makes, (tx fsd-ask-shell). A path is not an object: /sys names different trees in different profiles, so a rule says (sys) |
A broken rule is refused with the chain of holdings that breaks it, each step with the line that makes it. Here tests/manifest/rules-never-job.sysk forbids what its catalogue gives:
What the rules are decided over, every holding with its chain, the declared names and the rules with their lines, wire.rkt writes beside the wiring before it decides them, a broken rule too: build/wiring.holdings.sx (sysk 086), and beside it the facts they are made from, each with its line, build/wiring.facts.sx (sysk 088). sysq decides the same rules from them again, and its reports must be these. And build/wiring.tasks.sx says which function each task runs, by its id and its name in /sys/task: (task 3 shell (entry shell)), or for a job slot every program of the catalogue, (task 9 slot-0 (slot wc follow ...)) (sysk 111), so sysi can bound each task's stacks from the image without reading the wiring.
The rules system.sysk keeps today:
From manifest to proven code
tools/wire.rktchecks 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'sconsole. 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 usealt(read from the user code, which the build passes it). A profile is held by one task, mounts/once, and names for each path a task handed(tree ...)or the kernel; a tree server is mounted by one holder, for now (sysk 053, 062). Then it decides the rules, before it writes anything (sysk 061).- 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 foralt, each task's namespace as the kernel shows it (task-ns), andstart-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 --useslists the files that hold the functions the manifest names, the files those call into (sysk 033), and every library inlib/, 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-taskfails to verify, and there is no build. tools/model.rktchecks the whole system can always finish, from the same manifest and the tasks' code. See Model checking.
Nothing checks wire.rkt itself but its tests, so a manifest is also printed back (sysk 108). racket tools/print.rkt MANIFEST writes it in canonical form: what wire.rkt would assume written out, a channel's (depth 1) and its one sender's share, (tx c n); a catalogue entry's defaults, letters and needs in that order; the clauses in one order, each kind as written, since there order is meaning. tests/print-test.rkt wires every manifest in the tree and its printed form, and compares the tables as data, never as text: the wiring, the holdings and the facts, without the manifest's lines. A manifest that must be rejected is rejected for the same reason once printed. So a generator that drops or defaults what a manifest said fails a test, as nftables' printer did when it dropped a match that its restore then accepted (Red Hat bug 1998903).
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/.