The system · L5 and L4

Deadlock freedom

sysp proves each function on its own. It cannot see two tasks that each wait for the other forever. Before every build, tools/model.rkt shows that this cannot happen: first by a rule read off each task alone, and, only where the rule cannot decide, by exploring every order in which the tasks' channel steps can happen.

The rule

A task listens on a channel at a wait when that wait includes the channel: receiving from it, or waiting for room to send on it. A blocking send or recv is a wait on one channel; an alt is a wait on every source it wants. Listening is what breaks a wait: if one task waits for a message on a channel while the sender waits for room on it, the channel is empty, so there is room, and the sender is not stuck after all; and the other way round for a full channel.

tools/waits.rkt reads each task alone, against an environment that lets every channel step happen whenever the task's own counts allow it, and collects its waits: where it can block, what it wants, which channels it still owes. Then it removes every wait that cannot stick, over and over, until nothing changes; whatever is left forms a cycle. For the default system that is waits from states of single tasks, checked in well under a second. Its cost grows with each task's own code; the exact check's grows with the product of all of them.

Every wait of the default system, and why it cannot stick

Read off the code by the last make docs. A receiver that listens on its channel whenever it waits is a fixed point every chain of waits ends at; here that is . Every other wait is safe because the task it waits for is never stuck where it does not listen, which the rule works out task by task.

Five systems

A rejection names the cycle, one wait per line with its source location, then the exact check's shortest run to the problem:

model: 3 tasks, 3 channels: a cycle of waits, each held up by a task that is not listening
  1. chatter (task 1) waits for room on ab  (tests/model/relay.sysp:53:5)
     chatter (task 2) owes ab, and waits at 2 without listening on it
  2. chatter (task 2) waits for room on ba  (tests/model/relay.sysp:53:5)
     chatter (task 1) owes ba, and waits at 1 without listening on it
  rule: a task waits forever only if the task it waits for is itself stuck where it does not listen on that channel

Why it is sound

• A wait that lasts forever implicates a peer. If a task waits forever for a message on a channel, the channel stays empty and open, so some sender still owes it and never sends. A task that is never stuck reaches its end, and reaching its end means it has sent all it owes (sysp proves each task keeps its counts). So that sender is stuck forever too, at a wait where it owes the channel and, by the argument above, does not listen on it. The same holds for room and the receiver.
• So the stuck waits are inside what the rule keeps. Every wait a task can reach is among the waits read off it alone, and the rule removes only waits that cannot be part of such a set. If it removes them all, no task is ever stuck forever.
• Every stream ends. A second, smaller check makes sure nobody loops forever instead: a stream closes after whatever its sender waited for first, and that must not depend on the stream itself. In the default system the chain runs lines (closed when input ends), answers, out, keys.
• Checked against the exact check. A test runs both on every system in the tests, and on 300 small systems generated at random each run: the rule has never accepted one that the exact check finds stuck. What both rest on is in the trusted base.

When the rule cannot decide: the exact check

Some cycles are safe only because a channel holds enough messages: two chatters with room for two each never both fill up. The rule does not read depth, so it finds the cycle and does not decide. Then the exact check runs, up to 200,000 states, and its answer stands; past that, the system is rejected as too large to check. --exact runs it alone.

A state is where each task is in its code, how many messages wait in each channel, and which streams have ended. From a state, any task that can take its next channel step gives a new state. The exact check builds every reachable state, breadth first, as the TLA+ checker TLC does, and checks two things: no state is stuck with tasks unfinished (a deadlock), and from every state some run leads to the end, every task finished and every channel empty.

A client and its server: balances

The shell asks the file server and waits for the reply; the server, between requests, waits for the next one. Read alone, each holds the other up: the shell waits on fs-reply, which the server owes, while the server waits on fs-ask, which the shell owes. What rules it out is order: a reply comes only after a request. The rule reads that order as a count (sysk 031). Between two tasks with channels of their own both ways, each keeps its balance: the messages it has sent the other less those it has received from it. In any run, the messages between the two are the sum of their balances. So two waits can hold each other up only if they can be reached at once:

• Both waiting to receive needs the channels between them empty: the balances must sum to 0. The shell waits for a reply only when it has sent a request it has no answer to (balance 1); the server waits for a request only when it owes no reply (balance 0). The sum is 1: never at once.
• Both waiting for room needs the channels full: the balances must sum to their depths.
• Balances are kept only between tasks that share channels both ways, up to 2 either way; past that, or where several tasks send on one channel, nothing is assumed.

Each task is still read alone, so this costs little however large the two are, and the default system needs no exact check at all, not even of two tasks: the rule decides it from waits. The file server and the disk driver are a client and a server the same way. When balances do not settle a cycle of two tasks, the exact check still explores those two alone, every other task standing outside as an environment that takes and gives whenever asked (sysk 029). Two talkers that each send three messages on one-message streams before they listen (tests/model/pair-both.sysk) are found stuck that way; a talker and a listener (pair-one.sysk) pass. A random cross-check runs the rule against the exact check on 300 small systems each time the tests run; it found an early version of balances wrong, which tests/model/oneway.sysk now keeps out.

A client of several servers

Each task is read alone, so a configuration of the shell carries what it knows of every server at once: whether a server's replies have ended, and its balance with each. Those are independent, so they multiply. When the shell became a client of a second server, the entropy driver behind /dev (sysk 046), its configurations went from 10,398 to 41,311, and the rule from about 8 s to 30. Two facts brought them down (sysk 047):

• A reply's end needs the requests' end. A server that answers until its requests end closes its replies only after that end: every way to its close, which the check that every stream ends already walks, waited for it. The client sends those requests, alone, so while it still holds their stream open the replies cannot have ended, and the rule drops a recv-more's end there. A server that closes its replies early has a way to the close that does not wait, and is left alone: tests/model/early.sysk keeps that so.
• A balance of 0 is no balance. A balance back at 0 after a reply was kept as a 0, while one never begun was absent: the same knowledge, two configurations. Each server doubled the shell's for nothing.

Both only remove configurations the code cannot reach, so the rule accepts nothing it did not; the cross-check against the exact check on 300 random systems gives the same counts as before, and tests/model/two-servers.sysk (a client of two servers, accepted) and wait-own.sysk (a client that waits for the end of replies it keeps from ending, a cycle) are checked both ways.

Calls, read once

The shell asks its servers from some sixty places: cat, ls, writing into a file, watch, completion, ping, each through ask, which goes one of four ways, to the kernel's tree or a server's pair. Read as it once was, every call was inlined, and a configuration is what is left to run, so the same exchange at sixty places was sixty sets of configurations: each server, and each command that asks one, multiplied the shell's. sysk 055 reads a call once for each state it is entered in, its channel ends and what the rule knows of them, and that summary serves every call that enters it so: its waits are the task's, and the states it can return in are where the caller goes on. Pick a reading.

A call does not depend on the booleans it does not read, so those are not part of its state; and no call sets a caller's boolean (sysp has none to set), so every boolean leaves as it came. A call is a function of the task files handed a channel end, as before; one read from the same channel ends and literal booleans is the same program, shared, so its summary is too. A call of one step is its own first step, and is left inline.

The verdict is the rule's as before, wait for wait. Two tests say so: 300 random systems whose tasks call functions, two or three channel operations each, some calling another, give the same verdict and the same waits read once or inlined, and none it accepts does the exact check find stuck; and tests/model/calls-ok.sysk, a client asking through a function it calls twice, is accepted, while calls-stuck.sysk, the same client and a server that answers the second request only after a go the client sends after it, is a cycle.

The count barely moves: what a call costs is not how many configurations it has but how long each is. Inlined, a configuration inside ask carried the whole stack of calls above it, and every step compared it whole; read once, it carries only ask's own steps. The next server, or a job's client of netd, adds summaries, not another layer of everything.

Explore two small systems

Two chatters each send two messages, then receive two. With channels that hold one message each, both fill their channel and then wait to send again: a deadlock that sysp cannot see, since each chatter is correct on its own. With room for two, every run finishes. Each dot is a state, by distance from the start; select one to see it.

What a failure looks like

When the check fails, the tool prints the shortest run to the problem and what each stuck task waits for, with the source location of each step. Here it is for the chatters, rebuilt from the state graph above, without the locations:

What the code reader follows exactly

• A loop of the form (var i a) (while (< i n) … (set i (+ i 1))), or (for (i a n) …), runs exactly n − a times when that matters: when it sends or receives on a counted channel, or runs at most 16 times (three sends on a one-message stream must be three). A longer loop on streams only, such as the file server's walks over a 128-entry index sector, may run any number of times in the model, which says so (sysk 029). So does a loop that runs until a handle is spent, (while (> (rx-remaining h) 0) …).
• return ends the function where it is: what follows is read only along the ways that do not return (sysk 029). An if whose branch only returns is a way of its own when anything after it may touch a channel (sysk 038): before, the model read such an if as not there, so a task that returned early, skipping a send another task waited for, was read as sending. tests/model/tell.sysk was accepted then, and is stuck. A return is the last step on its way, and what follows the function follows it too: nothing before it is copied. Following the returns, among them the file server's commits, which a disk error ends at any of its writes, took the server's states from 6,740 to 9,576 and the rule's time from about 3.5 s to about 6. (A first version, which split each function into the ways that return and those that go on, copied each return's prefix and quadrupled them.) break ends its loop where it is (sysk 037): the loop goes round along its body's ways that do not break, and is left both where its condition is false and along each way that breaks, so a task that stops reading a stream early is followed past its loop. tests/model/leave.sysk is stuck only on that way out; tests/model/drain.sysk, which reads the stream to its end before it goes on, is not.
• A match (sysp 028) is read as an if on each variant in turn, the last clause taken when the others are not: which variant a value is, is data, so each clause is a way the task may go.
• Channel ends held in a struct (sysk 048): (let ns (new Ns (fs-ask fsa) …)) makes ns a bundle of those ends, (. ns fs-ask) names one as a variable would, a function handed ns is read with it as it is with ends, and (let (Ns s a r …) ns) takes them out again. The shell's namespace is one, so a server more is a field more, not two parameters more of every function that reaches a file.
• An inlined function's names are its own: a variable holding an alt's result, or a tracked boolean, in the caller is not the callee's of the same name (sysk 031: the file server's s in its loops was once read inside commit).
• A service (sysk 031): a wait for a job to open it is never stuck, as a wait for the device is not; a job's end of its channels is outside the system, so a request or the end may come at any time, and a reply always finds room. That rests on the client check at build time.
• Streams: (while (recv-more k in b) …) runs once per message and then takes the end, and (if (recv-more …) a b), or a variable bound to its result and tested later, takes a on a message and b on the end.
• A loop or an if whose condition reads a handle (rx-remaining, tx-remaining, rx-ended) or a local boolean set only to true or false (the terminal's held), under not, and, or and comparisons, goes the way the code would (sysk 016: booleans in the rule only; the exact check treats them as data). Where the task waits, a boolean it will set again before it next reads it is forgotten, so a function's flag, left as it was when the function returned, does not tell two states apart (sysk 031: the default system's single-task states fell from about 15,000 to about 5,300, and the rule's time from 5 s to 2). A boolean parameter handed true or false is the callee's own tracked boolean, set as it is called (sysk 032: the shell's command, run beside a job with busy true, never reaches the code that starts one). And a state is remembered only where the ways part, at an if the model cannot decide or a loop, not at every step (sysk 032: the rule twice as fast).
• A branch on alt's result is taken only when its source is ready and its guard wants it; a source followed by a receive on it, or room followed by a send, is one step, since only this task takes from its channel or fills its stream. A way that starts with a choice of the task's own is not: its source is taken first, then the task chooses (sysk 037: the shell's (if streams (recv-more …) (recv …)) after its alt).
• Anything else, a loop or an if on data, is a choice that may go either way, so the checks see more runs than the code has; they say where. To the exact check such a choice is a step the task takes, and from then on it keeps to the way it took, as the code does (sysk 030). Before, a task at a choice counted as stuck only if every way was, so a deadlock behind one way of an if went unseen: tests/model/choice.sysk, a task that may listen first beside one that always does, was accepted. A choice the world decides, a message or the end, alt's ready source, a test on handle counts, has no such step: what happens next decides it. A chain of the task's own choices with nothing another task could see between them is one step, to wherever they lead.
• Handle counts are tracked, as sysp proves of the code: a send needs messages left, a close needs none. Runs that break them are dropped.
• A launcher's job-start (sysk 017) gives it a receiving end of its jobs' output, a stream whose sender is not a task here: a wait for it is never stuck, as a wait for the device is not, and its end comes, because what a job runs is checked when it starts. job-end consumes that end; rx-streams is known. See Jobs.
• The scheduler is assumed fair: a task that can move eventually does. Round robin with a timer gives that.

How many states, and why the rule

Before sysk 013 the system had 49 states. Then five tasks started sharing log, and every order in which their lines can arrive became its own path: 45,867 states. The interactive system of sysk 015 multiplied that again, about eighteen times for each background task, until the default system had to shrink to four tasks. sysk 016 changed the question's method, not the question: the rule reads each task once, and the eight-task system came back.