Model Checking: Exhaustive Search Instead of Proof

Both previous approaches need a human to supply the insight: an invariant, or a type design. That effort scales with the system, and it is the reason verification is expensive.

Model checking removes it by brute force. Build a model of the system as a finite set of states with transitions between them, state the property, and have a machine examine every reachable state.

The consequence is a completely different user experience. There is no proof to construct, no invariant to invent, and no interaction. You supply a model and a property, and the tool returns either a confirmation or a counterexample: a concrete sequence of steps that reaches a violating state.

That counterexample is the feature. A failed proof says the argument did not go through, which may mean the property is false or merely that the invariant was too weak. A model checker hands back a trace you can read and replay.

The constraint that makes this possible is finiteness. Undecidability applies to arbitrary programs; a finite state space is exhaustively searchable, so the question becomes decidable.

The properties worth checking are about sequences of states rather than single ones, which needs a logic with time in it. Temporal logic supplies four operators, and almost every real property is built from them.

Always P. P holds in every reachable state. This expresses safety: nothing bad happens. Two processes are never in the critical section together.

Eventually P. P holds at some point on every path. This expresses liveness: something good happens. A request is eventually served.

Always eventually P. P recurs forever, which is what fairness usually means. Every waiting process is served infinitely often.

Until. P holds up to the point where Q becomes true.

The safety and liveness distinction matters practically because they fail differently. A safety violation has a finite counterexample: here are twelve steps leading to a bad state. A liveness violation needs an infinite one, presented as a cycle: here is a loop the system can take forever without the good thing happening.

That difference shows up in tooling. Safety checking is a reachability search; liveness checking must find cycles, and is correspondingly more expensive.

The limitation is immediate and severe, and every technique in the field exists to fight it.

A system's state space is the product of its components' state spaces. Ten components with ten states each is not a hundred states; it is ten to the tenth, ten billion.

Concurrency multiplies it again. With n processes, the number of possible interleavings grows factorially, and each interleaving may reach different states.

components   states each   total states
     3            10          1,000
     6            10      1,000,000
    10            10  10,000,000,000

That is state explosion, and it is the central problem of the field. It bounds model checking to systems that are small, or to models that abstract away most of a system's detail.

Notice the shape of the trade against the previous two lessons. Proof-based methods scale to large systems and need human insight per system. Model checking needs no insight and does not scale. They are complements rather than competitors, and the field's history is a sequence of attempts to push the boundary.

Each branch trades something different, and knowing which one a tool uses tells you what its answer means.

Symbolic model checking, developed by Edmund Clarke, E. Allen Emerson and Joseph Sifakis, whose work on model checking earned them the ACM Turing Award, stopped enumerating states one at a time. Sets of states are represented as logical formulas, so an astronomically large set can be manipulated compactly, and the search proceeds over set-valued steps.

Bounded model checking gives up completeness deliberately. Ask only whether a violation exists within k steps, encode that as a satisfiability problem, and hand it to a SAT or SMT solver. Finding a bug proves the bug; finding nothing proves only that none exists within k steps.

Abstraction replaces the model with a coarser one, which may report violations that the real system cannot reach. The standard remedy is to check whether a counterexample is real and, if not, refine the abstraction and repeat.

Partial order reduction exploits the fact that independent concurrent events can be examined in one order rather than all of them.

The word model is doing important work, and mistaking it for the system is the most common error in applying this.

A model checker verifies a description of the system, not the system. Someone wrote that description, and it necessarily omits almost everything: timing, memory layout, the network, the operating system, and every implementation detail not thought relevant.

So the guarantee is conditional in a specific way: if the implementation refines the model, and the model captures the relevant behaviour, then the property holds.

That conditional is weaker than it looks and stronger than it sounds. Weaker, because the gap between model and implementation is real and unverified, so a correct model does not mean correct code. Stronger, because the errors this catches are exactly the ones testing cannot reach: concurrency bugs, protocol violations, and distributed-system corner cases arising from orderings nobody would think to construct.

That is why the method concentrates where it does. Cache coherence protocols, consensus algorithms, hardware designs and distributed protocols are all small enough to model faithfully and combinatorial enough that human reasoning fails.

Modelling a whole application is neither feasible nor the point. Modelling the six-state protocol at its heart is both.

A specification language for this style describes states and the transitions between them, and looks unlike ordinary code.

VARIABLES holder, requests

Init == holder = "none" /\ requests = {}

Request(p) ==
  /\ p \notin requests
  /\ requests' = requests \union {p}
  /\ UNCHANGED holder

Acquire(p) ==
  /\ holder = "none"
  /\ p \in requests
  /\ holder' = p
  /\ requests' = requests \ {p}

MutualExclusion == \A p, q : (holder = p /\ holder = q) => p = q
NoStarvation     == \A p : p \in requests ~> holder = p

Three things are worth noticing. Each action states a guard and the resulting state, so the specification is a relation rather than a procedure, and the checker explores every action enabled in every state.

The two properties are of the different kinds from earlier. Mutual exclusion is safety, and a violation is a finite trace. No starvation is liveness, using the leads-to operator, and a violation is a cycle in which a process waits forever.

And nothing here says how any of it is implemented. That is the point: the protocol is checked independently of the code that will realise it, which is why this catches design errors before any code exists.

Of the three traditions, model checking has the widest industrial use, and the reasons are about economics rather than power.

The effort is bounded and up front. Writing a model of a protocol is days of work, and the checking is automatic. Proof-based verification is open-ended: you find out how hard it is by attempting it.

The output is actionable. A counterexample trace is a bug report, readable by an engineer who knows nothing about the underlying theory. A failed proof needs an expert to interpret.

It applies before implementation. Design errors are found when the design is a document, which is the cheapest possible moment.

It targets the errors that hurt most. Concurrency and distributed protocol bugs are rare, non-deterministic, catastrophic and nearly impossible to reproduce. Exhaustive search is exactly the right instrument for them, and testing is exactly the wrong one.

The honest limitation is that a passing check licenses less than it appears to. It says the model has the property, and the distance from model to system is unmeasured.

What has actually been verified end to end, at the level of real code, is the subject of the last lesson.

The third row is the fundamental difference, and it explains why all three survive. Each hits a different wall, so none subsumes the others.

The fourth row is why the third is adopted most. Actionable failure output is worth a great deal in practice, and it is the reason a technique with weaker guarantees sees wider use than techniques with stronger ones.

Reading across the last row gives the practical allocation. Use model checking on the protocol, types to make the invariants of the core unrepresentable when violated, and deductive proof on the small piece where functional correctness genuinely must be established.

What that costs, on real systems, is the final question.