17. The failing schedule, replayed

"Ain't no rest for the wicked."— Cage the Elephant

The scheduler agrees. A runnable task is runnable until it blocks, and the explorer in this chapter exists precisely to deny your program a quiet moment it did not order.

Everything in Part 3 so far has been about making whole classes of bug unsayable. A leaked task has no spelling; a lock-order deadlock has no spelling; a data race needs a second writer the type system will not give you. This chapter is about the bugs that are left, and it starts by admitting that there are some.

17.1 The bug that typechecks

The shelf reindexes. Two workers take documents off a queue, each sends back a word count, and the collector adds them up and stops when both workers report finished:

fn worker(queue: channel[int], shelved: channel[int], finished: channel[int]) {
    for words in queue { shelved.send(words) }
    finished.send(1)
}

fn main() -> !int {
    let queue = channel[int](4)
    let shelved = channel[int](4)
    let finished = channel[int](2)
    var total = 0
    var seen = 0
    scope pool {
        pool.spawn(fn() { worker(queue, shelved, finished) })
        pool.spawn(fn() { worker(queue, shelved, finished) })
        queue.send(900)
        queue.send(640)
        queue.close()
        var workers = 2
        var draining = false
        while !draining {
            select {
                w from shelved => { total += w; seen += 1 },
                _ from finished => { workers -= 1; if workers == 0 { draining = true } },
            }
        }
    }
    print("reindexed {seen} of 2 documents, {total} words")
    0
}

$ lupin reindex.lu
reindexed 2 of 2 documents, 1540 words

That is the right answer. Run it again and it is still the right answer; the shape of the program is not doing anything clever, and a reviewer reading it in a pull request would approve it. There is no shared mutable state — total and seen are locals of main, and the workers never touch them. Every value crossing a task boundary crosses through a channel. Nothing in this program is a data race, and no amount of tightening the type system would reject it, because there is nothing here to reject.

It loses work anyway:

$ lupin run reindex.lu --seed=2
reindexed 1 of 2 documents, 900 words

One document, shelved by a worker, counted by nobody. Read the select and the reason is visible once you know to look for it: when the second worker’s finished message and the second document are both waiting, select picks one, and if it picks finished, workers drops to zero, draining becomes true, the loop ends — and the document is still sitting in shelved, buffered, unread, and about to be discarded when the channel goes out of scope.

Say what this is, and what it is not

It is an ordering bug. The composite operation “collect every result, then stop” was never atomic with respect to the two messages that decide it, and no individual message was delivered late, twice, or out of order. Every send happened before its matching receive; the memory model held perfectly; both workers were correct.

It is not a data race, and this book is not going to blur the difference in order to make a better story. Part 3’s claim has always been narrower than the folklore version: races do not compile, because a race needs two tasks with live access to one mutable location and the ownership rules do not issue that access. Ordering bugs are a different class, they survive every type system that admits message passing, and they are the class that remains after wolf has removed the others.

Which is exactly why they are worth a chapter. Once the races are gone, what is left is a small set of bugs about the order of events — and a small set of bugs about the order of events is something a machine can search.

Exercise 17-1 (comprehension · lupin) — Two tasks each deposit 50 into a balance that starts at 0, through a get-then-set protocol with the store loop in main. There is no shared mutable capture and no Mutex. Predict the balance under the default schedule — and state what the correct answer would be if deposits never interfered:

fn deposit(getreq: channel[int], getrep: channel[int], setch: channel[int]) {
    getreq.send(1)
    let v = getrep.recv() else |_| { return }
    setch.send(v + 50)
}
fn main() -> !int {
    let getreq = channel[int](0)
    let getrep = channel[int](0)
    let setch = channel[int](0)
    var balance = 0
    scope s {
        s.spawn(fn() { deposit(getreq, getrep, setch) })
        s.spawn(fn() { deposit(getreq, getrep, setch) })
        var served = 0
        while served < 4 {
            select {
                _ from getreq => { getrep.send(balance) },
                v from setch => { balance = v },
            }
            served += 1
        }
    }
    print("balance={balance}")
    0
}

Exercise 17-2 (comprehension (schedule play) · lupin) — Hunt it: run 17-1 under seeds 0 through 5. Record each balance. Which seeds produce the correct answer, and what had to happen in the schedule for 100 to come out?

17.2 The seed, the schedule, and the frontier

Three commands are the whole workflow, and the first one you have already used.

--seed=N asks for one schedule, chosen by a seed. Every scheduling decision the run makes comes out of that seed, so the same seed is the same run — the same interleaving, the same output, on any machine, as many times as you like. That is what made --seed=2 above a fact about the program rather than an anecdote about a machine that was busy.

--explore=N does not pick a schedule. It searches:

$ lupin conform-run reindex.lu --explore=500
reindex.lu: explored 10 schedule(s) in 10 execution(s) (DPOR; 0 slept, 4 pruned), frontier closed
  outcomes: 2 distinct — SCHEDULE-DEPENDENT
    exit(0) ×8 stdout=reindexed 2 of 2 documents, 1540 words\n leaks=0 forest=ok — replay: --seed=0
      decision stream: ev:0,0,0,0,0,0
    exit(0) ×2 stdout=reindexed 1 of 2 documents, 900 words\n leaks=0 forest=ok — replay: --seed=4611686018427387916
      decision stream: ev:0,0,0,1,1
  deadlocks: 0 · races: 0 · max depth: 6 decision(s)
$ echo $?
1

Read that report line by line, because it is the chapter’s centerpiece and every field in it earns its place.

explored 10 schedule(s) in 10 execution(s). The budget was 500 and ten were enough. This program has six decision points with two choices each, which would be sixty-four interleavings enumerated naively; DPOR — dynamic partial-order reduction — recognizes when two orderings cannot produce different results and runs one of them. 4 pruned is the count of branches it proved equivalent to something already tried.

frontier closed. No reachable schedule was left untried. This is the strongest thing the tool ever says, and §17.3 is about the cases where it cannot say it.

outcomes: 2 distinct — SCHEDULE-DEPENDENT. The finding. Two different observable behaviors from one program with one input, which is what an ordering bug looks like from outside. Note that both outcomes exit 0: nothing crashed, nothing trapped, no assertion fired. The bug is that the program has two answers, and the tool’s job is to notice that rather than to know which one you wanted.

×8 and ×2. Eight of the ten schedules are right and two are wrong. That is the number that makes this bug the kind people describe as impossible to reproduce: it is not rare in the space of schedules, but the schedules a real machine picks are heavily biased toward the FIFO end, so in practice it appears when a machine is loaded, and never on a developer’s laptop.

replay: --seed=…. Each outcome carries the command that reproduces it. This is the sentence the whole chapter is written for: the finding arrives with its own reproduction.

decision stream: ev:0,0,0,1,1. The schedule itself, written down. A decision stream records choices, not events: five entries, each the index of the runnable thing the scheduler picked. Two of them are 1, which means the failing schedule differs from the passing one at exactly two decisions — and comparing the two streams tells you where to look before you have read a line of the program.

exit code 1. A schedule-dependent program is a finding, so the tool fails. That is what makes --explore usable in a test suite: green means “every schedule I could reach agrees,” and nothing else means green.

Replay

The seed is a value, so reproduction is not a ritual:

$ lupin run reindex.lu --seed=4611686018427387916
reindexed 1 of 2 documents, 900 words
$ lupin run reindex.lu --seed=4611686018427387916
reindexed 1 of 2 documents, 900 words
$ lupin run reindex.lu --schedule=ev:0,0,0,1,1
reindexed 1 of 2 documents, 900 words

Twice by seed and once by the explicit stream, three identical runs. Use the seed when you want to hand somebody a number; use --schedule=ev:… when the counterexample is what you want to read, because the stream is the schedule in a form you can edit, shorten, and compare against a passing one.

This is the difference the chapter is about, stated as plainly as it can be. Go’s race detector tells you there was a race, in a run you already finished, and finding it again is your problem. Wolf hands you the failing schedule as a value, and the failing run is a command.

The fix

Now fix it, and notice that the fix deletes code. The bug was that the collector had to decide between two message kinds; the cure is that the scope’s closing brace already knows the answer. After the brace, every worker has finished — that is what a join is (§10.1) — so nobody can send another result, so closing the channel cannot cut anyone off and draining it cannot miss anything:

fn worker(queue: channel[int], shelved: channel[int]) {
    for words in queue { shelved.send(words) }
}

fn main() -> !int {
    let queue = channel[int](4)
    let shelved = channel[int](4)
    var total = 0
    var seen = 0
    scope pool {
        pool.spawn(fn() { worker(queue, shelved) })
        pool.spawn(fn() { worker(queue, shelved) })
        queue.send(900)
        queue.send(640)
        queue.close()
    }
    shelved.close()
    for w in shelved { total += w; seen += 1 }
    print("reindexed {seen} of 2 documents, {total} words")
    0
}

The finished channel is gone, the select is gone, the worker count is gone, and the loop is a for. Ask the explorer whether the class of bug went with them:

$ lupin conform-run reindex.lu --explore=500
reindex.lu: explored 2 schedule(s) in 2 execution(s) (DPOR; 0 slept, 0 pruned), frontier closed
  outcomes: 1 distinct — observably deterministic (every schedule agrees)
    exit(0) ×2 stdout=reindexed 2 of 2 documents, 1540 words\n leaks=0 forest=ok — replay: --seed=0
  deadlocks: 0 · races: 0 · max depth: 3 decision(s)
$ echo $?
0

observably deterministic (every schedule agrees), frontier closed, exit 0. Two schedules instead of ten and three decisions instead of six, which is the other thing the report measures: the fix removed choices rather than symptoms. A program with fewer decisions has less to get wrong, and max depth is a number you can watch across a refactor.

One condition on this fix, stated because it is real. Draining after the join works when the channel can hold the batch — capacity 4 for two results here. A pool whose results outnumber the buffer needs a collector task inside the scope, and then the close belongs after that scope’s brace, in an outer one. The structure is the same and the braces do the arithmetic; what does not work is deciding between “a result arrived” and “everyone is done” in one select, which was the bug.

What this replaces

It is worth naming what a project does instead of this, because the alternative is what most of us have been doing.

The usual defense against ordering bugs is repetition: run the test a thousand times, run it under load, run it on the CI machine that is slower. That finds the bugs whose failing schedules the machine happens to produce, which is a biased and unknown subset, and it produces exactly one artifact when it works — a test that failed once. The explorer’s ten executions covered every inequivalent ordering of this program, which is a stronger statement than a thousand runs, and it produced a seed.

The other usual defense is a race detector, and it is a genuinely good tool aimed at a different class. A detector watches one execution for conflicting accesses; the bug above has no conflicting accesses, so no detector will ever report it. That is not a criticism of the detectors — it is the reason wolf spent Part 2 removing the class detectors are for, and this chapter searching the class that is left.

Exercise 17-3 (fingers · lupin) — Two sends race into one channel; main prints the arrival order. Run it twice with --seed=0, once with --seed=3, and once with --schedule=ev:0,0,0. Before running: which pairs of those four runs are guaranteed to match?

fn main() -> !int {
    let ch = channel[int](2)
    scope s {
        s.spawn(fn() { ch.send(1) })
        s.spawn(fn() { ch.send(2) })
    }
    let a = ch.recv() else |_| { return 1 }
    let b = ch.recv() else |_| { return 1 }
    print("{a}{b}")
    0
}

Exercise 17-4 (comprehension · lupin) — The explorer prints the two schedules of 17-3 as decision streams ev:0,0,0 and ev:1,0,0. Three decisions, but only the first digit ever differs. What is the first decision choosing between — and why are the remaining two decisions no longer choices once it is made?

Exercise 17-5 (spelunking · lupin) — Run lupin conform-run ex17-3.lu --explore=64 and read the report back: explain explored 2 schedule(s), DPOR, frontier closed, SCHEDULE-DEPENDENT, the per-outcome replay: seeds, and the process exit code.

17.3 Scope honesty

A tool that searches a space is only as good as your understanding of the space, so here is the boundary, drawn from the inside.

The budget is part of the verdict

Run the broken program again with a budget too small to find its bug:

$ lupin conform-run reindex.lu --explore=2
reindex.lu: explored 2 schedule(s) in 2 execution(s) (DPOR; 0 slept, 0 pruned), frontier OPEN
  note: schedule budget exhausted at 2 execution(s); frontier open
  outcomes: 1 distinct — observably deterministic (every schedule agrees)
    exit(0) ×2 stdout=reindexed 2 of 2 documents, 1540 words\n leaks=0 forest=ok — replay: --seed=0
  deadlocks: 0 · races: 0 · max depth: 6 decision(s)
$ echo $?
0

Same program, same bug, green verdict, exit 0. The report is not lying — observably deterministic (every schedule agrees) is true of the two schedules it ran — and it tells you so twice: frontier OPEN, and a note: naming the budget that stopped it. Read an exploration report the way you read a benchmark: the verdict is conditional on the budget line, and frontier OPEN is the condition talking. A green run with an open frontier is a run that has not finished asking.

--explore-preemptions=N bounds the search a different way, by limiting how many times the schedule may depart from FIFO order. It makes searches cheap and shallow, which is the right trade for a large program in a pre-commit hook and the wrong one for the report you paste in a bug tracker. It also reports itself, in the same note: line.

What exploration cannot see

Three kinds of nondeterminism are outside the space, and each has an owner.

Values. The explorer permutes scheduling decisions. A hash seed, a random backoff, an identifier from the operating system, a timestamp — these vary between runs without any schedule changing, and no amount of exploration touches them. Property testing and fuzzing own that axis.

Real time. The scheduler virtualizes time: a timeout(5.ms) arm fires when the runtime decides no other arm can become ready, not after five milliseconds of wall clock. That is what makes a test with a timeout in it fast and repeatable, and it means what you validated is your handling of a timeout and never the calibration of one. Whether five milliseconds is the right number is a question for a load test against a real peer.

Anything past the membrane. A C library with its own threads, its own file descriptors, and its own signal handlers is invisible to a scheduler whose model of blocking is wolf’s blocking points (§10.2). A task inside a C call is not interrupted, inspected, or migrated (§10.4), so the explorer cannot interleave anything with the inside of that call. The audit surface of chapter 9 is the boundary, and the C library’s own test suite owns what happens past it.

The positive statement those three carve out is worth having in one sentence: exploration proves ordering properties over the events it can see and permute. Both halves are load-bearing, and neither is a disclaimer — the events it can see are every channel operation, every select, every acquisition, every spawn and join, and every proc lifecycle event in your program, which is where ordering bugs live.

What v1 does not do

Two absences, stated plainly because folklore expects otherwise.

There is no production flight recorder. Determinism here is a testing instrument: you run a program under the deterministic scheduler, and what you get back is a seed. Recording a live service’s real schedule so that a production incident can be replayed offline is a different mechanism with a different cost, and wolf does not have it. A crash in production hands you what crashes in other languages hand you, plus a task forest (§11.3) and an exit reason (§14.1).

And exploration is not verification. frontier closed covers every inequivalent schedule of this program on this input. Change the input and you have a new search; the tool says nothing about the inputs you did not run. Combining the two axes — property-generated inputs, each explored exhaustively — is a thing you can build today out of the parts in this chapter, and it is worth building for the code where ordering is the whole product.

Exercise 17-7 (comprehension · lupin) — Rerun 17-3’s exploration with --explore-preemptions=0. Predict what the report will claim about determinism before you run it, then reconcile the claim with 17-5’s.

Exercise 17-8 (design) — List three behaviors of a real concurrent service that seeded schedule exploration, as this chapter defines it, cannot find — and for each, name the tool or practice that owns it instead.

Where Part 3 leaves you

Eight chapters ago a task was a thing you started and hoped about. What you have now is smaller than a framework and larger than a library: a brace that joins, a channel that carries ownership, a select that multiplexes, a when that cannot deadlock, a proc that is a failure domain, two primitives under every supervision policy, and a seed that makes any of it repeat.

The through-line is one idea applied at four sizes. A scope owns tasks and its brace is the arithmetic (§10.1). A region owns objects and its brace is the free (§8.2). A proc owns regions and its death is the free (§14.2). And a schedule owns the order of events, so a seed is the whole of it (§17.2). Every one of those is a boundary you can point at in the source, which is why the failure modes in this part have locations rather than reputations.

What none of it does is make a concurrent program correct for you. It makes the mistakes sayable: the leak became a deadlock with a roster, the race became a compile error, the ordering bug became a seed. A program can still be wrong. It can no longer be wrong in a way nobody can hold.

Exercise 17-9 (extension (break-it-on-purpose) · lupin) — Construct a deadlock from two tasks and two rendezvous channels, each task receiving first and sending second. Predict the trap’s roster before running: how many tasks does it name, and why is the answer three when you wrote two?