I’ve spent the week putting a TLA+ model into a side project and wiring it into the checks. Not as a document that says the protocol is sound, but as something that fails when the model and the code drift apart. I understood it about halfway through doing it, which is the wrong order, so this post does it the right way round: a counter, two workers, and one new piece per section until the shape of the real thing appears.

Everything below was run. The TLC output is pasted as TLC printed it.

A counter, two workers, one step

Two workers each add one to a shared counter. When both are done the counter should read 2. Here’s the whole specification.

---------------------------- MODULE Counter ----------------------------
EXTENDS Naturals

CONSTANT Workers

VARIABLES x,    \* the shared counter
          left  \* worker -> 1 until it has done its increment

Init ==
  /\ x = 0
  /\ left = [w \in Workers |-> 1]

Inc(w) ==
  /\ left[w] > 0
  /\ x' = x + 1
  /\ left' = [left EXCEPT ![w] = @ - 1]

Next == \E w \in Workers : Inc(w)

Done == \A w \in Workers : left[w] = 0

Total == Done => x = 2
=========================================================================

Read it as a state machine, because that’s what it is. A state is a value for every variable. Init says which states you can start in. Next says which states you can move to: some worker with work left increments x and marks itself done. Primed variables are the values after the step. Total is the property I want true in every reachable state.

TLC, the model checker, needs a config that says which definitions play which role and what the constants are.

INIT Init
NEXT Next
CONSTANT Workers = {1, 2}
INVARIANT Total
CHECK_DEADLOCK FALSE

The last line matters more than it looks. When both workers are done nothing can move, and TLC calls that a deadlock unless told it’s fine. Here it’s fine. Run it:

$ java -cp tla2tools.jar tlc2.TLC -config Counter.cfg Counter.tla
Model checking completed. No error has been found.
5 states generated, 4 distinct states found, 0 states left on queue.

Four states: nobody done, worker 1 done, worker 2 done, both done. TLC visited every one of them and Total held in each. That’s what “the model holds” means, and it’s all it means. It says nothing about any program.

Split the increment the way a program does

No program does x := x + 1 in one step. It reads x, then it writes x. So the model gets a program counter per worker and a slot for the value it read.

VARIABLES x, left,
          pc,    \* worker -> "read" or "write", where it is in x := x + 1
          seen   \* worker -> the value of x it read

Read(w) ==
  /\ pc[w] = "read" /\ left[w] > 0
  /\ seen' = [seen EXCEPT ![w] = x]
  /\ pc' = [pc EXCEPT ![w] = "write"]
  /\ UNCHANGED <<x, left>>

Write(w) ==
  /\ pc[w] = "write"
  /\ x' = seen[w] + 1
  /\ left' = [left EXCEPT ![w] = @ - 1]
  /\ pc' = [pc EXCEPT ![w] = "read"]
  /\ UNCHANGED seen

Next == \E w \in Workers : Read(w) \/ Write(w)

Same config, same invariant.

Error: Invariant Total is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ seen = <<0, 0>>
/\ left = <<1, 1>>
/\ x = 0
/\ pc = <<"read", "read">>

State 2: <Read line 18, col 3 to line 21, col 26 of module Counter>
/\ pc = <<"write", "read">>

State 3: <Read line 18, col 3 to line 21, col 26 of module Counter>
/\ pc = <<"write", "write">>

State 4: <Write line 24, col 3 to line 28, col 19 of module Counter>
/\ left = <<0, 1>>
/\ x = 1
/\ pc = <<"read", "write">>

State 5: <Write line 24, col 3 to line 28, col 19 of module Counter>
/\ left = <<0, 0>>
/\ x = 1
/\ pc = <<"read", "read">>

13 states generated, 12 distinct states found, 3 states left on queue.

I’ve trimmed the unchanged lines from states 2 to 5; TLC prints them all. Both workers read 0, both write 1, both are done, x is 1. The lost update every concurrency course opens with, found by exhaustive search in five states. Nobody had to think of the interleaving. That’s the part of model checking that’s worth the Java.

Two things to notice in the output. TLC searches breadth first, so the trace it prints is the shortest one that breaks the invariant, which is what makes it readable. And each state names the action that produced it, with line numbers into the spec.

Add the fence, but keep the bug

The fix is compare-and-swap: only write if x still holds what you read, otherwise read again. The obvious move is to edit Write and rerun. I did something slightly different, and it’s the pivot of the whole approach: the fence becomes a constant, so the same model describes both the broken code and the fixed code.

CONSTANT Fenced  \* TRUE: a write only lands if x still holds what the worker read

Write(w) ==
  /\ pc[w] = "write"
  /\ Fenced => x = seen[w]
  /\ x' = seen[w] + 1
  ...

\* The compare-and-swap lost; go back and read again.
Retry(w) ==
  /\ Fenced /\ pc[w] = "write" /\ x /= seen[w]
  /\ pc' = [pc EXCEPT ![w] = "read"]
  /\ UNCHANGED <<x, left, seen>>

Next == \E w \in Workers : Read(w) \/ Write(w) \/ Retry(w)

Retry isn’t decoration. Without it a worker whose CAS lost has no enabled action and stays at pc = "write" for the rest of the behavior. Total would still hold, vacuously, because Done never becomes true. A model that can’t reach the states you care about passes every invariant you give it, which is the first way to fool yourself with one.

Now there are two configs instead of one. They differ in a single line.

CONSTANTS
  Workers = {1, 2}
  Fenced = TRUE

With Fenced = TRUE: 12 distinct states, no error. With Fenced = FALSE: the five-state trace above.

Pin both verdicts

Here’s where it turns from a document into a check. Each config gets its expected verdict on its first line, as a TLA+ comment so TLC ignores it.

\* expect: violated
INIT Init
NEXT Next
CONSTANTS
  Workers = {1, 2}
  Fenced = FALSE
INVARIANT Total
CHECK_DEADLOCK FALSE

A thirty-line script runs every config, reads the verdict out of TLC’s output, and compares it with the declared one.

for cfg in Counter-*.cfg; do
    expect="$(sed -n '1s/^\\\* expect: //p' "$cfg")"
    java -cp "$jar" tlc2.TLC -config "$cfg" Counter.tla >"$out" 2>&1 || true
    if grep -q '^Error: Invariant .* is violated' "$out"; then
        got=violated
    elif grep -q 'states generated, .* distinct states found, 0 states left on queue' "$out"; then
        got=holds
    else
        exit 2  # TLC neither finished nor found a violation
    fi
    [[ "$got" == "$expect" ]] || failed=1
done

The exit code isn’t usable, because TLC exits non-zero on a violation and a violation is the right answer for half the configs. Hence the grep. The 0 states left on queue part is deliberate too: it’s how you know TLC finished the search rather than stopping early.

$ ./check.sh
check: Counter-cas    holds     as expected
check: Counter-racy   violated  as expected

Now the two ways this can go red. I deleted the fence line from Write and reran:

check: Counter-cas    violated  EXPECTED holds
check: Counter-racy   violated  as expected

That’s the boring direction. The model of the fixed code now has the bug, someone weakened the spec, fail. The interesting direction is the other one. I flipped the racy config to Fenced = TRUE by “mistake”:

check: Counter-cas    holds     as expected
check: Counter-racy   holds     EXPECTED violated

The counterexample disappeared, and that is a failure. If you only pin the configs that are supposed to hold, a model that stops finding its own bug looks like good news. It isn’t. The bug in the code didn’t move; what moved is the model’s ability to see it. A pinned “violated” is the model checking itself: prove you can still find the problem, then prove the fence removes it.

Replay the trace against the code

So far nothing has touched a program. The model has a Fenced knob; the code has a Store and a CompareAndSwap; nothing says which one the code is actually calling. This is the gap every “we model-checked it” claim has, and the ways to close it are heavy: generate the code from the spec, or instrument the program to emit traces and have TLC validate them against the model. Both are real techniques. Neither is an afternoon.

The cheap way is to take the trace TLC printed and type it in as a test. Split the worker the same way the model splits it:

type Worker struct {
	c      *Counter
	fenced bool
	seen   int
}

func (w *Worker) Read() { w.seen = w.c.Load() }

// Write is the Write action of Counter.tla, Retry included: when the
// fence rejects the write the worker reads again and tries once more.
func (w *Worker) Write() {
	if !w.fenced {
		w.c.Store(w.seen + 1)
		return
	}
	for !w.c.CompareAndSwap(w.seen, w.seen+1) {
		w.Read()
	}
}

And the test is the five states, in order, with the invariant as the assertion.

// TestCounter_LostUpdate is the trace TLC printed for Counter-racy.cfg,
// replayed against the code: Read(1), Read(2), Write(1), Write(2).
func TestCounter_LostUpdate(t *testing.T) {
	for name, fenced := range map[string]bool{"racy": false, "cas": true} {
		t.Run(name, func(t *testing.T) {
			c := &Counter{}
			a, b := NewWorker(c, fenced), NewWorker(c, fenced)

			a.Read()
			b.Read()
			a.Write()
			b.Write()

			if got := c.Load(); got != 2 {
				t.Fatalf("x = %d, want 2", got)
			}
		})
	}
}

--- FAIL: TestCounter_LostUpdate (0.00s)
    --- FAIL: TestCounter_LostUpdate/racy (0.00s)
        counter_test.go:19: x = 1, want 2

Red for the racy worker, green for the fenced one, and no goroutines anywhere. The interleaving is scheduled by hand because TLC already did the hard part of finding it. A test that spawns two goroutines and hopes the scheduler produces the bad order is a lottery ticket; this is the winning number, copied out.

What this test proves is narrow and I want to state it exactly. It proves the code reaches the same state the model reaches on this one path, and that the code with the fence doesn’t. It does not prove the code conforms to the model on every path. One path, chosen because the model said that’s where it breaks.

What the real one looks like

In the side project the counter is an append-only log shared by a cluster of engines, the workers own objects according to a membership view, and every write is stamped with the epoch of the view the writer had. The invariant is that two engines whose view is current and whose tail is at the end of the log agree on every object. There isn’t one knob but four: whether replay applies the epoch fence, what the tail skips, whether an engine writes under a view it already knows is stale, whether the transport refuses an append with an old epoch. Five configs, each pinned. Two of them describe the code as it shipped and are expected to fail, and their counterexamples are seven steps long and need no network partition, which was the surprise. The rest describe candidate fixes, and one of them describes what the code does now. Two tests replay the two counterexamples against two real engine loops sharing one log, and that pair of tests is the whole reason I can say the model describes the code rather than a code I’d like to have.

The check takes minutes and needs a JVM, so it isn’t in the default verification target. It runs when the model, the configs or the handover code change. It’s also nowhere near a proof: the model is bounded to two engines, one object and a handful of epochs, and it abstracts a projection down to the last record folded. What it is is a ratchet. The bugs it found stay found, the fences that closed them stay closed, and if either of those stops being true a script says so before I do.

If you want to try the counter yourself, the whole thing is three files and one jar, and it runs in under a second. Which is exactly the size at which I should have started.