The system · L5

Jobs

The manifest fixes every task before boot, and everything is checked then. Jobs (sysk 017) let one task decide while the system runs which programs run next, without opening a hole: the manifest fixes what may run, and each job, a small manifest of its own, is checked before it starts, as strictly as the system was.

What the manifest fixes

The jobs test system (tests/jobs/system.sysk): a printer, a launcher, and a pool.

(system
  (channels (log (bytes 64) (depth 4)))
  (task line-printer (device uart) (heap 64) (rx log))
  (task launcher (heap 512) (jobs jout) (tx log))
  (jobs
    (programs producer filter consumer talker greeter)
    (slots 3 (heap 256))
    (channels (j0 (bytes 8) (depth 2)) (j1 (bytes 8)) (jout (bytes 64) (depth 2)))))

• The catalogue, (programs …): task functions a job may run. Each takes the kernel, its heap, a clock if it keeps time (sysk 058), then channel ends, then its arguments (sysk 036: a number, i64, or a flag, bool), and says in its contract what each end must be (message size, an exact count or a stream), what range each number is in, and how much heap it needs. The catalogue gives each number its default: the default system's is (programs … wc (follow (quiet 5000))), and a flag is off unless named. tools/wire.rkt reads those contracts and refuses a program it cannot judge, or one that waits on several sources at once (alt), or needs more heap than a slot has.
• The slots, (slots n (heap b)): n tasks made at boot like any other, each with its heap, that run the catalogue's programs. No task is ever created at run time; a job only decides what a slot runs.
• The pool's channels: their message sizes and depths are fixed, so their rings stay in the generated wiring and the kernel's invariant keeps its shape. A job decides only who holds which end.
• Services, (service NAME (bytes b)) (sysk 031): two more pool streams whose other ends belong to the one task handed (serves NAME); a job binds them to a program checked, at build time, as a client of a service of their size. The default system has two, the disk's files and the network's talk (sysk 058), and a job binds the one whose server's tree holds what it was lent: Files for jobs.
• The launcher: the one task handed (jobs c), the right to start jobs, whose output it reads on pool channel c. Slots and pool channels count toward the kernel's limits of tasks and channels.

A job is a table

A job is a buffer of bytes in the launcher's heap: the number of tasks, then 21 bytes per task (task-bytes): its program's index in the catalogue; for each of its 8 parameters, the pool channel bound to it (255 for none); and its 4 arguments, 3 bytes each, least significant first (sysk 036; 0 where the program has none). The launcher keeps the receiving end of its output channel. Select one of the test launcher's jobs to see its table (the arguments' bytes dashed) and what the check made of it.

The check

job-check is a kernel call. It judges the table against the catalogue's contracts and the pool (kernel/jobs.sysp, verified sysp like the rest of the kernel) and, if it passes, copies it into kernel memory. It returns the reason, and keeps the verdict in the launcher's right: where the problem is (job-detail), and, for an accepted job, how many messages will reach the launcher. Inside the kernel the verdict is an enum, Verdict (sysk 040): passed with its count, or a variant for each reason with what that reason names, the task, the parameter, the channel or an argument's value, and a channel's own verdict may be unused, where before a number 0 meant both that and passed. At the kernel call it is still a number, reason-of, and three details, detail: a gate passes numbers. The first check that fails is the reason:

Reason 8 is the rule of sysk 016, split in two. At build time tools/waits.rkt explores each catalogue program alone, as it explores every task, and the wiring gets its waits as tables over parameter numbers: what each wait wants and what it still owes. At run time the kernel puts the job's waits together from those tables and the table's bindings and runs the same removal to a fixpoint, the launcher counting as always listening on the output (with a job in the background, the shell listens between commands, and no command waits on the job: sysk 032). Reading the code happens once, at build time; the join is a few thousand steps. The test script judges nineteen jobs and runs eleven in under 100 timer ticks of a millisecond. (Reason 8 was 7 until arguments came: it is checked last, after the table alone has passed.)

Slots run what they were given, proven

Each slot runs a generated runner. It waits for its slot to be given a program (job-await), reads the channels bound to it (job-bound), checks them against that program's contract, renews its heap, mints exactly the handles the contract names and calls the program; when the program returns it reports the slot idle (job-done). For the producer:

(fn job-run-producer ((k (shared Kernel kernel-rely)) (h (mut Heap)) (w Wire) (slot i64)) unit
  (effects io)
  (requires (and (running k) (system-ok k)))
  (let c0 (job-bound k slot 0))
  (let c1 (job-bound k slot 1))
  (let room (heap-renew h))
  (if (and (<= 10 room) (<= 0 c0) (== (bytes-of c0) 8) (<= 0 c1) (== (bytes-of c1) 64))
    (producer k h (tx w c0 3 8) (tx w c1 3 64))))

A program with arguments has them read too (job-arg) and checked against its range: follow's runner calls it only when (<= 1000 a0) (<= a0 60000), and passes a flag as (== a0 1). sysp proves the call meets the producer's contract whenever the checks pass: the same proof start-task has for a task the manifest wires, made over values checked at run time instead of constants. So the runner does not trust job-check; both rest on the same generated tables, and a check that failed would only leave the slot idle. job-bound returns pool channels only, so no job is ever handed a device or a channel of the permanent system. The heap is renewed between programs (heap-renew, which only the wiring names): a program returns only once it has freed every block it took, and the runner holds none, so no block is in use (the trusted base).

One job at a time, by contract

The launcher holds one Jobs, and it keeps where the launcher is in the protocol in its fields, its phase (an enum, Phase, since sysk 040; a number before) and the last verdict, as a channel handle keeps its count (sysk 018; in 017 a separate Staged value did this, but sysp keeps resources out of variables, and a shell's loop must hold the right across commands). Each call's contract says which state it needs and which it leaves:

• job-check needs an idle right: while a job runs, a second job-check does not verify.
• job-start needs a right whose last job passed: what starts is exactly what was judged, and a refused one is discarded with job-discard.
• job-end needs a running right and the job's output end, done: every message received, or the stream's end. It waits until every slot of the job is idle; the pool is free.
• jobs-close consumes an idle right: the runners return and the slots finish, so the system still stops.

The negative tests show sysp rejecting a task that forges Jobs, a launcher that starts a job without asking whether it passed, one that ends a job before reading its output, and one that judges a second job while the first runs.

The system around jobs stays checked

The permanent tasks are still checked for deadlock before every build. In the static model the launcher holds one receiving end of a stream, its jobs' output: opened by each job-start, consumed by job-end. A job only ever waits on the launcher, for room on that output, so it can never close a cycle of its own; a wait for its output is never stuck, as a wait for the device is not, and its end comes. A launcher that, while a job runs, waits for something that waits for it is rejected, naming the cycle (tests/model/jobs-stuck.sysk).

A run

The test launcher runs the pipeline twice and producer to consumer once in the same three slots, then a job refused for each reason, each followed by one that runs. Its log, abridged:

sysk: starting 5 tasks, 4 channels, preemptive (1 ms quantum)
producer: sending message 0
filter: passing message 0
consumer: message 0: 8 bytes, sum 56
…
launcher: job ended: 1
…
launcher: job ended: 3
launcher: job refused, reason 1
greeter: hello from a job
launcher: job ended: 4
launcher: job refused, reason 2, task 0
…
launcher: job refused, reason 7, task 0, parameter 0, channel 5
greeter: hello from a job
launcher: job ended: 10
launcher: job refused, reason 8, task 0, parameter 1, channel 1
greeter: hello from a job
launcher: job ended: 11
sysk: all tasks finished