Skip to main content

Finite Models and Protocol Correctness

Prerequisites: S1 invariants; S5 interleavings; S6 transactions. Budget: 30-45 hours. Outcome: discover a protocol counterexample by exploring reachable states and state the limits of the result.

Diagnostic​

Draw the interleaving where two increments lose an update. Distinguish “a bad state never occurs” from “work eventually finishes.” These correspond to safety and liveness; they need different arguments.

The mechanism​

A finite transition model has an initial state, permitted actions, and successor states. An invariant must hold initially and after every permitted transition. Breadth-first search can explore reachable states and retain predecessor edges to explain a failure.

Choose a bounded domain so exploration terminates. The bound is part of the result. Checking two clients and one request does not prove correctness for arbitrary clients, storage failures, or request identities. A model also excludes any behavior you forgot to represent.

Worked counterexample: deduplication after the effect​

A request should increment a durable counter once despite repeated delivery. The naive handler checks a durable seen flag, applies the increment, then marks the request seen. If a crash occurs between the effect and marker, a retry repeats the increment.

The following executable Python model represents one logical request, a durable counter, a durable marker, and a volatile handler phase. The counter saturates at 2 because reaching 2 already violates the invariant. Crashes retain durable state and restart the handler.

from collections import deque

def successors(state, atomic=False):
    count, seen, phase = state
    if phase == "idle":
        if seen:
            yield "duplicate ignored", state
        elif atomic:
            yield "atomic effect and marker", (min(2, count + 1), True, "idle")
        else:
            yield "check unseen", (count, seen, "checked")
    elif phase == "checked":
        yield "apply effect", (min(2, count + 1), seen, "applied")
    elif phase == "applied":
        yield "mark seen", (count, True, "idle")
    if phase != "idle":
        yield "crash and restart", (count, seen, "idle")

def counterexample(atomic=False):
    initial = (0, False, "idle")
    queue = deque([initial])
    paths = {initial: []}
    while queue:
        state = queue.popleft()
        if state[0] > 1:
            return paths[state]
        for action, nxt in successors(state, atomic):
            if nxt not in paths:
                paths[nxt] = paths[state] + [(action, nxt)]
                queue.append(nxt)
    return None

assert counterexample() is not None
assert counterexample(atomic=True) is None
print(counterexample())

The failing path checks, applies, crashes, checks again, and applies again. The repaired model commits effect and marker in one durable transition. That repair is appropriate only when the real storage mechanism can atomically commit both. It does not make an external email or payment participate in a database transaction.

Guided assignment​

Run the model and retain its counterexample. Add two distinct request IDs, a bounded delivery sequence, and a result cache so duplicates return the original response. Specify the invariant per request identity. Then model the effect occurring in an external subsystem with its own failure boundary.

Acceptance: preserve the original failure trace; the atomic local model has no counterexample within the documented finite bounds; an external-effect variant exposes why the local transaction alone is insufficient. Map each abstract transition to the code or storage operation it represents. Record whether a crash means process loss, machine loss, or simulated loss of volatile state.

Transfer and limitations​

Reverse the naive order: write the marker, crash, then apply the effect on a later step. Check: a retry can suppress an effect that never happened. This avoids duplication by risking omission; it does not satisfy the original contract.

Explain why the model does not establish liveness under infinitely many crashes. Introduce a fairness or eventual-recovery assumption before claiming eventual completion.

Use Specifying Systems, beginning with state and transition specifications, to express the same bounded problem in TLA+ as a stretch exercise. Passing a model checker is evidence about the model and configuration, not a universal certificate for an implementation. Apply the rubric.