The system · L4 and L3

Files for jobs

A job can be lent part of the disk's tree for as long as it runs (sysk 031). The shell lends, the file server enforces, the kernel connects the two only while the job runs, and the build checks that no job can stall the server. You type wc /notes/shopping; wc reads that one file, and nothing else.

A lend, step by step

Step through wc /notes/shopping. Blue boxes are tasks, purple the job, green the kernel.

/ % echo (milk eggs) > /notes/shopping
/ % wc /notes/shopping
(wc (bytes 12) (lines 1))
job ended

A service: two pool streams with a fixed server

The jobs clause declares the service; one task serves it. That makes two more pool channels, streams of 576 bytes: files-ask, a job's requests, and files-reply, its replies. Their other ends are the server's.

(task fsd (heap 32768) (tx disk-ask) (rx disk-answer) (tree (bytes 576)) (serves files))
(jobs
  (programs (wc (needs (read file)))
    (follow (quiet 5000) (needs (read file))) (ping (times 3) (needs (talk icmp host))) (tell (needs (talk tcp host)))
    (host (needs (talk dns name))) (datagram (quiet 2000) (needs (talk udp host))))
  (slots 4 (heap 4096))
  (channels (j0 (bytes 8) (depth 2)) (j1 (bytes 8)) (out (bytes 64) (depth 2)))
  (service files (bytes 576) (rights read write mutate))
  (service talk (bytes 576) (rights read write icmp tcp dns udp)))

(serves files) hands the server a Service, a capability like Jobs, which keeps where its holder is in the protocol: no lease, the requests' end given, both ends given. When a job that binds the service starts, the kernel marks it fresh: a new kind of alt source. The server opens a lease (service-open gives the receiving end of the requests, service-reply the sending end of the replies), serves it, and once the requests have ended, service-close ends the replies.

One lifetime argument makes the kernel's part small. A job ends only when its tasks have finished, and the client finishes only once it has received the replies to their end, which service-close sends. So by the time the next job-start empties the pool's channels, the server holds no end of them. The contracts carry it: close-rx needs a stream's end received, and only service-close gives it.

The job check counts the server

A service's channels have one end outside the job, as the shell's out does: its requests a receiver (the server), its replies a sender. A job may bind them only to the parameters of a program that was checked as the service's client (below), and that needs what the service can stamp (below, sysk 059), and both or neither. Reasons 3 and 5 of the check say so. To the check's waits rule, a wait for the service is never held up, as a wait for the launcher's output is not: what makes that true is the client check at build time.

Checked when the catalogue is built: a well-behaved client

Every program that could be bound to a service is judged, when the system is built, together with a server that answers each request, until the requests end, and then ends its replies. The rule of the deadlock check judges the two as it judges any system. wc asks, then reads the reply, every time, so it passes; it and follow ask through one function, files-ask in prg/files-client.sysp. A program that sends four requests before it reads any reply could leave the server holding a reply it cannot send while the program waits to send again, and the build stops:

tests/manifest/service-greedy.sysk: the catalogue: `greedy`, as a client of service `files`,
could get stuck: greedy waits for room on p0; the service waits for room on p1

The real server does what the reference server does, or less: it may take its time. It serves the shell and the job together with alt, and while a reply to the job is unread it reads none of the job's requests, but goes on serving the shell. A job that stopped reading would stall itself, not the server.

What a job can reach

What a job attaches to is the node the shell lent, with the rights the shell lent it, no more than the shell's. Paths only go down (no ..), so nothing above the lent node can be named. Every fid carries rights, and each operation needs its own:

The test system tests/fsd/lend.sysk runs a launcher that holds the disk through a profile, (profile disk-only ("/" fsd)) (sysk 063), and makes /d/a and a sibling /s, then five jobs. A probe lent /d to read tries each operation; wc is lent /d/a; the probe again, lent nothing; the probe lent /d with every right, which its stamp cuts to read (below); and follow, which needs nothing, bound to the service. Each line is one job's:

(probe 0 0 2 0 2 2 4 2 1)
(wc (bytes 8) (lines 2))
(probe 2)                      ; lent nothing: the attach is not permitted
(probe 0 0 2 0 2 2 4 2 1)      ; lent every right, stamped read: what it saw the first time
refused 3                      ; follow needs nothing: no client of the service
(pair 0 2 0 0 2 0 1)           ; two loans, each lent every right: loan 0 read, loan 1 write, no loan 2

When a job's requests end, the server forgets what it lent, frees the job's fids, and drops any file the job was writing and never closed: only the shell's own requests survive a job.

Within its need (sysk 059)

A program says what it needs, beside its defaults in the catalogue: (read file), a path it reads, or (talk icmp host), a peer it holds a conversation with. Each service says the words of its rights, the ones its server understands, as Hydra's type managers defined their own: read, write and mutate are the files protocol's (1, 2 and 4), any other the service's own, from 8. The need is a channel requirement, as Singularity's manifests said the endpoints a program needs, and it is in the program's file in /prg, so its one hash covers the code and what it may hold.

Three holders, each enforcing what it can see:

The kernel sees which services a job binds: a program binds a service only if its need is in the service's words, so a program that needs nothing has no files and no network, whatever the launcher says (refused 3 above). It copies the job's stamp from the catalogue's table into the lease, as seL4 mints a badge into a capability, and never reads it. The server sees every lend: at service-open it caps what was lent by the stamp (fs-stamped), so a lend of every right to a program that needs to read is a lend to read. The shell sees what the person named, and only says which file or which peer: designating is granting. The worst a confused shell can do is lend the wrong one, within the need.

A lease holds up to fs-loan-max loans, two (sysk 089), so a program can read one file and write another, as cp does, or read two, as cmp (both sysk 078): (needs (read file) (write file)), its needs in order, the j-th file need going with the j-th file argument. A lend names its loan by number in the request's offset, and so does a job's attach, 0 by default, so a program with one file is as it was; an attach beyond the loans there are answers no-such-name. The stamp is still one byte: loan j's three protocol rights are its bits 3j to 3j + 2, and fsd caps each loan by its own (fs-stamped takes the loan's number), so a shell that lends wrongly still cannot give a source to write. A service with rights of its own, as talk has, keeps one loan, since its own rights take the bits from 3 up, and wire.rkt refuses a program with two needs bound to it. The test system's pair is lent /d/a and /s, each with every right: it reads the first and cannot write it, writes the second and cannot read it, and finds no third.

The rejected designs: a service per right (a window that only reads, beside one that writes) multiplies the services as servers times rights; a server that asks the kernel who its client is adds a call at run time where everything else is fixed at build time.

In the shell

A program's kind of need says how the words after its name are read (sysk 059): for files a path each, lent with its own need's rights: (wc /notes/shopping), or through sugar wc /notes/shopping; cp /notes/x /notes/y lends the first to read as loan 0 and the second to write as loan 1 (sysk 078). The program's service parameters are bound to the service of the tree the path is in, the rest wired as a pipe of one. Since sysk 058 there are two services, fsd's files and netd's talk, and a program is the client of any service of its message size, not of one by name: the namespace says which server serves jobs, (/ 4 (jobs 3 4)) … (/net 7 (jobs 5 6)), so wc /net/eth/addr binds talk-ask and talk-reply, and wc /notes/shopping binds files-ask and files-reply. For talk an address, and a conversation dialed in the need's protocol, its data lent (The network); for none, a channel's name. The shell lends after the job check passes and before the job starts, so a job the check refuses leaves no lend behind. With several files it finds every path first, lends each to read, and only then makes or empties each to write, as > makes its file, and lends it: the job is lent no right to make or empty one, and a refusal empties nothing. A file both read and written, cp /f /f, is refused, since emptying it would empty what is read. A loan lent before a later one is refused stays with fsd until that loan is lent again; a job reaches only the loans its own command lent, since its stamp gives rights to as many loans as it has needs, and the shell lends them all. The paths are on one tree, whose service the job binds: cp /notes/x /sys/x is not permitted. The refusals come in the command's terms:

Not yet: a job that binds two services at once, or holds more than two files; mv, which is one rename on one tree, not a copy. A job can follow a file as it grows: a read of its may wait for a change (Reads that wait, sysk 033), as follow's do.