Model-check the invariant before building the protocol; the checker tries the interleavings a review skips

A concurrent protocol is a set of steps plus a claim about every order they can run in. Prose and diagrams show the orders someone drew; a model checker runs through all of them. Write the design as a specification — initial state, the atomic steps, and the invariant that must hold in every reachable state — and let TLC search a small instance exhaustively. What comes back is either “no error in N states” for that instance, or a step-by-step trace that breaks the invariant, found before any code exists to defend.

---------------------------- MODULE LeaseFencing ----------------------------
EXTENDS Naturals
CONSTANTS Clients, FenceReads, FenceWrites

(* --algorithm LeaseFencing
variables
    holder = "none",   \* whom the lock service believes holds the lease
    epoch = 0,         \* last token issued, strictly increasing
    value = 0,         \* the protected resource: a counter
    maxToken = 0,      \* highest token the resource has seen
    accepted = 0;      \* increments the resource acknowledged

define
    NoLostUpdate == value = accepted
end define;

process LockService = "lock"
begin
Expire:
    while TRUE do
        await holder /= "none";
        holder := "none";    \* the TTL ran out; the holder is not told
    end while;
end process;

process Client \in Clients
variables token = 0, seen = 0;
begin
Acquire:
    await holder = "none";
    epoch := epoch + 1;
    token := epoch;
    holder := self;
Read:
    if FenceReads /\ token < maxToken then
        goto Done;           \* a newer holder already reached the resource
    else
        if FenceReads then maxToken := token; end if;
        seen := value;
    end if;
Write:    \* may run long after the lease expired: a GC pause, a slow network
    if FenceWrites /\ token < maxToken then
        goto Done;           \* the resource rejects a stale token
    else
        if FenceWrites then maxToken := token; end if;
        value := seen + 1;
        accepted := accepted + 1;
    end if;
end process;
end algorithm; *)
\* pcal.trans inserts the TLA+ translation between the algorithm and this line.
\* Model: Clients = {c1, c2}, INVARIANT NoLostUpdate, checked with tlc2.TLC -deadlock
\* (the lock service waits forever once both clients finish; that is not a bug).
=============================================================================

What the checker found in this model. With no fencing, TLC reports NoLostUpdate violated with an 8-state trace: c1 takes token 1; the lease expires; c1 reads 0; c2 takes token 2 and reads 0; c1’s delayed write lands; c2 writes; the counter is 1 after two acknowledged increments. Checking the token only on writes — the blind-write scheme of 66 — fails with the same 8-state trace, because c1’s stale write reaches the resource before it has ever seen token 2. For read-modify-write the resource must learn the newer token at read time (FenceReads), or the write must be conditional on the value that was read: with both token checks TLC finishes with no error (57 distinct states for two clients, 667 for three), and a compare-and-set variant of the write step, checked separately, also held. A design review that reads “we have fencing tokens” approves both versions; TLC separates them in a run it reports as under a second.

What “no error” means. Explicit-state model checking is exhaustive only for the constants configured — two or three clients, one counter. Bugs that need more actors or longer histories need a larger instance; the bet that most design bugs show up at small scope is a heuristic, not a guarantee. Each label is one atomic step, so the grain of atomicity is the central modelling decision: if the real resource cannot check the token and write in one step, the model above is describing a system that does not exist. And the spec is not the code — asked how they know the implementation matches the verified design, the AWS engineers answer that they don’t. The bridge is to carry the invariant into runtime assertions and into the history checker of 98, which tests the real implementation under faults.

Decision rule. Specify before coding when three things coincide: concurrency or partial failure, a small core of steps, and an invariant whose violation is irreversible — lost or duplicated data, two owners of one resource. Typical targets: lease and leader handoff (66, 91), online migrations and shard moves (17, 87), the snapshot-to-log seam of CDC (104), workflow state machines with compensations (69). Keep the spec next to the design document and re-check it on every change to the protocol: in the AWS report, specs written for DynamoDB’s replication were reused to check a later migration feature, and the checker found a bug in its first design. Model checking does not address emergent slowdowns and retry storms (24); the same report says its authors know no feasible way to model that class. Start with safety invariants; liveness needs fairness assumptions and a separate check.