Several lock-free structures and a semaphore passed their stress tests with three races still inside them. Each failure required a specific interleaving that the runtime and operating system never produced during testing.
I wrote small executable models and checked every schedule allowed by their bounds. For each modeled pop, I compared the result with an expected sequential order. The models found all three races. They did not check the code's memory-order annotations. I use the same pattern in my day-to-day low-level work: reduce the problem until I can check the smaller version completely, then state exactly what that model leaves out.
Recent LLMs are especially useful in this workflow. I use them to draft the reduced model and challenge the mapping from source code to the specification. TLC is still the part that checks every state allowed by the model's bounds.
The schedules a stress test misses
Stress tests sample the schedules one machine happens to produce. A thread may run a whole push or pop between preemptions, while the failure needs another thread to act between two atomic operations.
The queue model used three processes and four nodes. The stack model used two processes and three nodes. TLC checked every state reachable inside those bounds, which is a different job from running the full implementation for longer.
Writing the state machine
I modeled the shared memory that mattered along with each thread's local variables and program counter. One transition represented one atomic load, store, or compare-exchange from the implementation.
A stress test needs lucky timing to freeze one thread mid-operation while another runs. In the model, that state is ordinary data.
Granularity mattered. Collapsing a whole push into one transition would hide the windows where these bugs occurred. Splitting one hardware-atomic compare-exchange into separate compare and swap steps would invent impossible interleavings. Each spec step therefore stayed close to one atomic operation in the implementation and quoted the source line it modeled.
One small model, end to end
Here is a reduced queue. The source operation publishes a node through an atomic exchange, then connects it to the previous tail:
Node* previous = tail.exchange(node);
if (previous)
previous->next.store(node);
else
head.store(node);The model keeps only state that can change the result: three reusable nodes, their links, the queue ends, and a sequential list named expected. Worker-local variables and program counters are added automatically by the PlusCal translation.
variables
free = <<A, B, C>>,
expected = <<>>,
steps = [w \in 1..2 |-> 0],
next = [n \in Nodes |-> None],
head = None,
tail = None;Each label in the reduced PlusCal model becomes one schedulable transition. publish_tail models the atomic exchange. The fixture appends the node to expected in that same transition because this is the chosen linearization point for the simplified queue.
procedure AppendOne()
variables node = None, previous = None;
begin
take_node:
if free = <<>> then return; end if;
node := Head(free);
free := Tail(free);
clear_link:
next[node] := None;
publish_tail:
previous := tail;
tail := node;
expected := Append(expected, node);
link_previous:
if previous # None then
next[previous] := node;
else
head := node;
end if;
return;
end procedure;The test driver does not prescribe an operation order. Two workers repeatedly choose between append, remove, and empty. TLC chooses which enabled label runs next, so a worker can stop after publish_tail while the other worker enters RemoveOne.
process Worker \in 1..2
begin
run:
while steps[self] < Limit do
count_operation:
steps[self] := steps[self] + 1;
either call AppendOne();
or call RemoveOne();
or call CheckEmpty();
end either;
end while;
end process;A successful remove reaches one extra fixture step. It compares the returned node with the front of expected, advances the sequence, and puts the node back into free so TLC can also explore address reuse.
check_remove:
assert removed = Head(expected);
expected := Tail(expected);
free := Append(free, removed);When the assertion fails, the useful output is the preceding state sequence. A shortened mismatch has this form:
worker 2 / check_remove
removed = C
expected = <<B, C>>
assert C = B failedThe shortened mismatch trace is illustrative rather than a saved counterexample. TLC normally prints the active label, shared fields, worker locals, and program counters for every state. Reading backward from the failed assertion shows the first transition where the modeled queue stopped matching its sequential reference.
TLC checks the bounded model, not compiled code. In the full specifications, source excerpts beside the labels kept each modeled transition tied to the atomic operation it represented.
Enumerating every schedule
PlusCal is an algorithm language for writing state machines like this one. Its translator produces a TLA+ specification, and TLC enumerates every reachable state. The queue configuration uses three processes and four nodes, with the sequenced front index bounded below twelve. The stack uses two processes and three nodes, with the top index bounded below seven.
Starting from the initial state, TLC takes every enabled step, records each new state, and continues until no new states remain. This covers every schedule admitted by the configured model, not every execution of the production program.
Exhaustive enumeration fits only small configurations: a handful of threads and nodes. Each thread adds its program counter and locals to the state, while each node adds possible links and owners, so the state count grows as a product across both. This is the state-space explosion: the cost comes from enumerating every reachable state, not from a slow checker.
Within those small configurations, a completed run establishes that no admitted interleaving reaches a state the model defines as wrong. That definition is the next problem.
Why the oracle mattered
Basic invariants check that counts stay valid, heads do not point to freed nodes, and elements are not delivered twice. They can still miss a queue silently dropping an element.
The expected sequence catches that loss because every remove must return its first node. This is narrower than a general linearizability checker. The spec declares the intended linearization step and checks all modeled operations against the resulting sequential order.
The three races
On a mismatch, TLC prints the thread, step order, and state after each step. Because every modeled step quotes its implementation line, the trace maps directly back to source.
1. ABA in the pop path
The first race was ABA in a pop path. Thread A loads head A and reads its next pointer B. It plans to replace head A with B through compare-exchange.
Between the load and the compare-exchange, the other threads pop A, retire B, and push a fresh node. The allocator reuses address A for that fresh node. Thread A then runs its compare-exchange. The pointer bits match, so the swing succeeds and head becomes B. But B is freed memory. The eventual crash happens later, in whichever thread touches the structure next.
Compare-exchange checked that the pointer bits still matched. The algorithm needed to know whether it was still the same node. The failing schedule required a free, address reuse, and another push inside a few instructions of the first pop. TLC treated that rare schedule like any other reachable path.
2. The last-node transition
The second race occurred while popping the last node. With one element, the producer and consumer operate on the same node and both ends of the structure must agree on the transition to empty. The checker found an order the code did not handle. Stress tests rarely stayed in the one-element state long enough to hit it.
3. A half-visible push
The third catch was not a crash. The checker found a reachable state where another thread saw a push as neither absent nor complete: part of its effect was visible and the rest was not. The reference makes push indivisible, so every observer sees the queue before or after it, never halfway through. The real model and reference therefore disagreed, and the checker printed the schedule.
The engineering cost
Each spec took one to three engineering days. The work consisted largely of restating code that already passed its tests and matching each transition to the correct atomic boundary.
The days go into modeling and into keeping the step granularity at the real atomicity boundary. A spec is code too. Fuse two atomic actions into one transition and the model gets cheaper, but the window between them vanishes, along with every counterexample that needs it.
The configurations stay small because every additional thread or node multiplies the reachable states. These are bounded checks of a sequentially consistent model, not proofs of the whole library.
The approach assumes that many lock-free logic bugs appear in small configurations. Every race found here did, but the assumption remains a limit.
Memory ordering is outside the model
These models check the logical state machine. They do not model CPU memory reordering, so a passing spec can still be wrong on weakly ordered hardware.
The model treats every transition as indivisible and immediately visible. Real CPUs and compilers can reorder visibility between transitions. For example, the model assumes that a thread seeing a ready flag also sees an earlier payload write. ARM needs the correct ordering annotations to make that true. Those executions lie outside the state space TLC searched.
This mattered more for this library than it would for a single-platform one. The code shipped across many operating systems, consoles, and toolchains, and some of those targets are weakly ordered. Code whose ordering annotations are subtly wrong can run clean for years on a strongly ordered desktop machine and then misbehave on the next platform the library is brought up on, and no green checker run would have warned anyone.
Within the configured bounds, TLC compares a sequentially consistent model with the expected sequence. The acquire and release annotations still need a separate weak-memory argument.
Spec drift
A green spec can silently describe old code because it never executes the implementation. Each spec therefore records the source revision it models. Changes to those lines require another correspondence review.