Vx

Checking the deadlock watcher

Aditya Kumar · 3 November 2026

TL;DR — When each task of a Vx program waits and nothing can wake one, the runtime stops the program and names each wait. A program that it stops by mistake is worse than a program that hangs. So we wrote a TLA+ model of the watcher that makes this decision, and the TLC model checker tried every order of its steps at a small size. TLC found a gap of three lines in the timer thread. In that gap, a busy machine could make the watcher report a deadlock that did not exist. A flag now closes the gap. The model was ten times larger with the watcher in it, so only the smallest models turn the watcher on. A proof in Lean, a proof assistant, also found that select, which waits on several channels at once, could pass over a channel forever.

A deadlock in a concurrent program often looks like a program that is slow. Vx tells the two apart. The runtime has a watcher thread. When it is sure that no task can go on, it stops the program and prints where each task waits. A mistake in either direction costs the user. If the watcher misses a deadlock, the program hangs with no message. If it reports a deadlock that is not there, it stops a correct program. This post is about how we checked the watcher, and the bug that the check found.

What the watcher prints

Here is a report from a test of the runtime, with its file name made shorter. One task holds a lock and waits for a value on a channel. A second task waits for the lock. The main code and a third task send on a full channel that nothing reads:

vx: deadlock: each task of the program waits, and nothing can wake one. The program stops.
  the main code waits in `send` at deadlock.vx:49 on channel 1, made at deadlock.vx:77
  a task waits in `lock` at deadlock.vx:44 on lock 1, made at deadlock.vx:73
    in the task from the `spawn` at deadlock.vx:80
  a task waits in `recv` at deadlock.vx:34 on channel 2, made at deadlock.vx:76
    in the task from the `spawn` at deadlock.vx:83
  a task waits in `send` at deadlock.vx:66 on channel 1, made at deadlock.vx:77
    in the task from the `spawn` at deadlock.vx:86

Each line names the wait, the line that made its channel or lock, and the spawn that started the task. Two waits on the same channel name the same number.

How the watcher decides

Every wait in the runtime is a wait on a word of memory. A task in Vx is a fiber, a small stack that a worker thread runs. When a fiber waits, it parks: it leaves its worker and goes on a list of the waiters of that word. A thread that is not a worker sleeps on a condition variable instead. A waker changes the word and then wakes the fibers and threads on its list.

Every 100 ms, the watcher looks at four things:

fn stuck() -> bool {
    let fibers_parked = program_scheduler().is_none_or(|s| s.all_parked());
    fibers_parked
        && WAITING.load(SeqCst) == THREADS.load(SeqCst)
        && !timer::pending()
        && !io::pending()
}

Every fiber must be parked. WAITING counts the threads that sleep with no time limit, and THREADS counts all threads of the program, so every thread must sleep. No deadline of a wait with a time limit may be still to come, and no I/O may be in flight. A counter, PROGRESS, goes up at each wake. The watcher reports a deadlock only when two looks in a row are stuck and the counter did not move between them.

None of the four reads is atomic with the others. A fiber can park after the watcher counted the fibers and before it counted the threads. The watcher is correct only if every such order still gives the right answer. Tests try a few orders. A model checker tries all of them.

A model of the protocol

formal/runtime/WaitWake.tla is a TLA+ model of the wait and wake protocol. Each step of the code that another thread can see is a step of the model. Here is the step where the timer takes a deadline and gets ready to wake its word:

\* The deadline of a fiber comes, and the timer wakes the word of the fiber.
Fire(k) ==
    /\ pc[k] = "set"
    /\ k \in Timer
    /\ \E f \in armed :
         /\ armed' = armed \ {f}
         /\ expired' = expired \cup {f}
         /\ firing' = f
    /\ pc' = [pc EXCEPT ![k] = "wake"]

The model has fibers that park, threads that sleep, and two wakers that share one list. It also has a cancel, which ends a tasks block and wakes every task in it. It has a task under a callback from foreign code, waits with a time limit, and the timer thread. Last, it has the seed mode for tests, where a seed fixes the order of the tasks and the main thread runs every task itself. The watcher is three steps, one for each separate read in the code: the progress counter, the parked fibers, and the counts of threads and deadlines.

TLC checks these claims for every order of the steps:

A check that can fail

A claim that holds tells us little if it could not fail. A model can be too weak, or a claim can be true for a reason that has nothing to do with the code. So run_tlc.py also puts 16 mistakes into the model, one at a time. TLC must report the claim that each mistake breaks, and the run fails if it reports another claim or none.

Two of the mistakes are bugs that we fixed in the runtime before the model existed. In the first, a thread still counted as waiting after its wake, until it ran again (#2505). On a busy machine the watcher then saw every thread asleep, though one of them could go on. In the second, a task under a callback from foreign code waits on its worker's thread and does not park. The scheduler counted it as running, so a deadlock that included it was never reported (#2522). With these bugs put back, TLC reports NoFalseDeadlock for the first and DeadlockIsReported for the second.

The gap in the timer

The first run of the full model failed. In the model of a task that waits with a time limit, TLC reported NoFalseDeadlock. This was the loop of the timer thread:

fn run(t: &'static Timer) {
    let mut d = t.deadlines.lock().unwrap();
    loop {
        // ... wait until the earliest deadline comes ...
        d.pop();
        drop(d);
        wake(bucket(word as *const i64), Fibers::Of(word));
        d = t.deadlines.lock().unwrap();
    }
}

The timer takes the deadline off its heap, lets go of the lock, and then wakes the word. Between the pop and the wake, the heap can be empty, so timer::pending() is false. The wake did not happen yet, so PROGRESS did not move. The task is parked. Each check of stuck() is true.

TLC printed a trace of 21 states. Here are its last steps, in words:

  1. The main thread and both wakers end. Task f2 parks on a word that no one sets, with a deadline.
  2. The deadline comes. The timer takes it off the heap, and the heap is now empty. The timer does not run its wake yet.
  3. The watcher looks. Progress moved since its last look, so it does not report. But every fiber is parked, every thread of the program ended, and no deadline is pending, so this look is stuck.
  4. The watcher looks again. The timer still did not run. Progress did not move, and the look is stuck again. The watcher reports a deadlock.

The next step of the timer would wake f2, and the program would go on. The report was false.

On a real machine, this happens only if the timer thread stays off the CPU for about 200 ms between two lines. That needs a machine with more ready threads than cores, or a timer thread that the operating system stops for some other reason. It is rare. It is also the kind of failure that a user cannot reproduce and that a test suite never shows.

The fix (#2615) keeps a flag next to the heap, under the same lock:

fn pending(&self) -> bool {
    !self.heap.is_empty() || self.firing
}

The timer sets firing when it takes a deadline off the heap and clears it after the wake ends. The model has the same rule, and the mistake the_timer_looks_idle_before_its_wake puts the old rule back. A unit test checks pending() at each step: with no deadline, with a deadline on the heap, and with a deadline that the timer took but did not wake yet.

Small models

The watcher has its own state: where it is in its three reads, and what it saw at the last look. That state multiplies with every other state of the program. With the watcher in it, a model was about ten times larger. The nine models took 3,330 seconds on two TLC workers, which is too slow for CI. Without the watcher they took about 160 seconds.

So most models turn the watcher off, and they still check the protocol. Five more models turn it on, with one fiber and one thread. Each watcher mistake still breaks its claim in these small models, and they take 10 to 90 seconds each. The whole run, 14 models and 16 mistakes, took 4 minutes on 14 workers.

This is the usual bet of a model checker. Most concurrency bugs need only two or three actors to show. The timer bug needed one task, one thread and the timer. A bug that needs ten tasks will not show in these models.

Select and Lean

The same work checked select, which waits on several channels at once. The design says that it takes turns: if a channel has a value at each of n calls, for n channels, one of the calls chooses it. select started its search at the count of all channel events, modulo n. A Lean proof showed that this count can starve a channel. Take two channels that always have a value. Each call takes one value, which is one event. Then a send on channel 0 is a second event. So the count goes up by 2 between two calls, the count modulo 2 is always 0, and every call starts at channel 0:

theorem count_starves : ∀ c, pick 2 ((2 * c) % 2) (fun _ => true) ≠ some 1 := by
  intro c
  rw [Nat.mul_mod_right]
  decide

Now a Selector keeps the index after its last choice and starts its next search there (#2568). The theorem after_last_within_n proves that this rule takes turns for any n.

What the model does not check

We write the model by hand from the code. If the code changes and the model does not, TLC checks the old code. The model also checks the protocol, not the tests of the protocol. On the same day, CI failed on the test that prints the report above. The main code and a task both sent on a channel that holds one value. The test expected the main code to send first, and on CI the task sent first. The runtime had no bug, and the test checked the outcome of a race. The test now makes the task send first.

What is left

The model is formal/runtime/WaitWake.tla, and formal/runtime/run_tlc.py runs it with each mistake. The select proofs are in formal/memory_model/lean/VxMemoryModel/Select.lean. The changes are Vx#2566, Vx#2568 and Vx#2615. Vx is Apache 2.0 with the LLVM exception — install it and try the examples.