3.3 The Process View

The Logical view named the parts. The Process view asks the question the logical view cannot: what happens when many parts run at the same time? Concurrency turns a correct-in-isolation design into a source of races, deadlocks, and torn writes, and the more parts run at once, the more interleavings the design must survive. The Process view is the lens for that — the states a system moves through, the locks it takes, and the invariants that must hold across every one of those interleavings. Those invariants are not comments: a checker holds the running system to them, so a race cannot reach production unseen — the Alignment Thesis, read at the grain of concurrency.

This is the chapter where invariants stop being predicates over one state and become predicates over an order of events. That step-up pulls in a cluster of ideas: what an automaton is, safety versus liveness, bounded model checking, and the temporal-logic step from a state assertion to a sequence assertion. This chapter defines each as it is first needed, and The Book's Language collects them for quick reference. Two general types live here — the state machine and the automaton / formal invariant — and four real models embody the view: formal invariant verification as the verification backbone, the synchronization model, and the mediator and single-writer registries.

What is an automaton / state machine?

An automaton, or state machine, is a finite set of states and the labeled transitions between them. It models computation as "which state am I in, and which moves are legal from here." A microwave is idle, cooking, or door-open; pressing start moves idle to cooking, opening the door moves cooking to door-open. The value of drawing it: the illegal states and the missing transitions become visible. If a path leads back to cooking while the door is open, the diagram shows you the way to cook yourself. A state machine is the logical spine the Process view's invariants attach to — the invariant is a predicate over the states, and the checker walks the transitions.

Assertions over STATE vs over SEQUENCES

Some properties are about a single state: "a job is never both leased and free." You check one by visiting every reachable state and evaluating the predicate there (the invariant primer). Other properties are about order over time: "a preempted job eventually re-runs." No single state can be inspected to settle that — it is a claim about the sequence of states, that a good state is always eventually reached. Claims about order need temporal logic (LTL, linear temporal logic), which adds operators over sequences: always (□), eventually (◇), and leads-to (↝). The step-up matters because the two kinds route to different checkers — a state search for the first, a temporal model checker for the second.

The four operators the rest of this chapter leans on all describe the shape of a run — a path the system walks, one state after another. They are claims about that path, not math:

• Always (□P) — P holds at every step of every run: nothing bad ever slips through.
• Eventually (◇P) — some step of the run satisfies P: the good thing arrives, sooner or later.
• Leads-to (P ↝ Q) — every step where P holds is followed by a later step where Q holds: once P, then Q eventually.
• Until (P U Q) — P holds at every step until a step where Q becomes true, and Q does become true.

Safety vs liveness

Two shapes cover most invariants. Safety says a bad thing never happens — written □P, "always P." "Never both leased and free" is safety. Liveness says a good thing eventually happens — written P ↝ Q, "P leads to Q." "A preempted job eventually re-runs" is liveness. The shape is not decoration: it derives the checker. A safety property is settled by a state-space search that looks for any reachable bad state; a liveness property needs a temporal model checker that reasons about infinite or cyclic behaviors. Declare the shape wrong — route a liveness property to a safety runtime — and the checker structurally cannot see the violation, and reports green. So the shape is checked too: a lint asserts the declared temporal form matches the routed checker.

What is bounded model checking?

A test samples the input space — it runs the cases you thought of and sails past the one adversarial schedule you did not. Model checking instead exhaustively explores the state space: it visits every reachable state, or every interleaving of a concurrent system, and either proves the invariant across all of them or hands you a concrete counterexample trace — the exact sequence of steps that reaches the bad state. Bounded model checking does this out to a fixed depth: it explores every state reachable in k steps. Within that bound the proof is total; a bug that needs k+1 steps is out of scope, the honest limit you trade for a decidable check. Why it matters for a fleet of concurrent agents: a distributed race has failure traces no hand-picked example hits, and only an exhaustive walk of the interleavings finds them. A green sampled test over that race means nothing; a clean bounded model check means no bad state is reachable within the bound.

The general type behind these ideas — an automaton with a formal invariant — gets no separate model page; it is introduced here as trunk machinery and embodied by the first real model below: formal invariant verification, which takes an invariant's temporal shape and uses it to route the exhaustive checker that proves it.

3.3.1 Formal invariant verification

Formal invariant verification is the backbone the other three models hang their invariant tables on. It assesses invariant soundness under interleaving — whether a property holds on every reachable state, not just the schedules a test happened to try — and answers it by an exhaustive check that either proves the property or returns a counterexample trace. The distinctive move: the invariant's temporal form is a routing input, not a label. A safety form (□P) routes to a state-space search; a liveness form (P ↝ Q) routes to a temporal model checker. Get the form wrong — declare a liveness property as safety — and the safety runtime structurally cannot see the violation and reports green. So a lint checks the form against the checker that ran: the shape is consumed, and a mis-routed invariant is a build failure rather than a false all-clear. Its full construct-and-invariant treatment is in the appendix; the temporal operators it routes on are defined above.

Learn more about this governance mechanism: formal invariant verification.

That backbone proves invariants once you can state them. The next three models are about the invariants concurrency hands you: the ones nobody writes down until an inverted lock ordering deadlocks the build. Start with the locks themselves.

3.3.2 The synchronization model

A typed registry that models the system's synchronization behavior — every OS-level lock, which shared resource it guards, and the required acquisition ordering — so concurrency contracts are declared and checkable, not tribal.

(a) Quality property it helps assess. Two, both catastrophic at runtime and invisible in the code.

• Lock coverage: is every OS lock in the codebase declared, and is what it guards known? An undeclared lock is one nobody can reason about; the coverage lint makes it a build failure.
• Deadlock-freedom: can two locks be acquired in an order that deadlocks? The declared ordering graph lets a lint answer "which locks, in what order" before the code runs, so an inverted acquisition fails at author time instead of hanging in production.

(b) Constructs and relations. Three record kinds compose the registry.

• SyncLock — one OS primitive: its lock-file path, its cap (1 for a mutex, M for a semaphore), the resource it guards, its bypass-env, its audit-log.
• LockAcquirer — one declared acquisition site: where in the code a lock is taken, or a declared "takes none" with a rationale.
• LockOrdering: a before/after constraint between two locks, with a rationale. The set of these is the ordering graph the deadlock lint walks.

One SyncLock is acquired at many LockAcquirer sites and constrained by many LockOrdering edges.

(c) Visual depiction. The natural diagram, Figure 3.3-1, is an ER schema — three related record kinds with crow's-foot cardinality. Reused from the model's appendix Structure slot:

(d) Invariants, and how they are checked. A coverage lint and an ordering lint, the second doing genuine graph reasoning, collected in Table 3.3-1:

The ordering lint walks a lock-acquisition sequence against the declared graph and fails on an inversion, so a deadlock-inducing order is caught at author time:

import sys

# Declared ordering: a lock in `before` must be acquired before its `after` lock.
ORDERINGS = [("db-lock", "cache-lock")]      # db before cache, always

def ordering_lint(acquire_sequence: list[str]) -> list[str]:
    """A held-lock acquiring one that must precede it is an inversion (deadlock risk)."""
    findings, held = [], []
    for lock in acquire_sequence:
        for before, after in ORDERINGS:
            if lock == before and after in held:
                findings.append(f"acquired '{before}' while holding '{after}' — order inverted")
        held.append(lock)
    return findings

if __name__ == "__main__":
    findings = ordering_lint(walk_acquisitions())   # a code path's acquisition order
    for f in findings:
        print(f"LOCK-ORDER: {f}")
    sys.exit(1 if findings else 0)

(e) Traceability and derivation direction. Model-from-code. The coverage lint scans the real lock call sites and requires each to be a declared acquirer, so the code is the ground truth and the model is the checked view. The join key is the lock path (which lock a site takes) and the acquirer site (where the acquisition happens).

Also seen in: Physical (a lock is held per-host, so placement matters). Rendered in full here; its higher-level siblings, the mediator and single-writer registries, sit beside it below.

3.3.3 Two ways to make a concurrent write safe: the mediator and the single-writer registries

The synchronization model catalogs the raw locks. Two higher-level registries sit above it, and together they draw a distinction worth keeping sharp: there are two ways to make a concurrent write safe, and they fail differently. You can cap how many run at once, or you can insist that exactly one may write. A mediator does the first; a single-writer contract does the second. Confusing them is how a torn write hides behind a semaphore that was only ever rationing load.

Learn more about this governance mechanism: synchronization model.

Learn more about this governance mechanism: concurrency contracts.

The mediator registry

The mediator registry is the how-many half. It declares which heavy or shared-resource subprocess invocations must run through a serializer — the test runner, the build tool, the whole-repo lint mutex — and at what concurrency cap (1 for a mutex, M for a semaphore). Its quality property is mediation coverage: the serializer enforcer can only guard a call that reaches it, so a newly-added raw call that skips the serializer is invisible to the enforcer. The coverage lint closes exactly that blind spot: an unmediated call to a mediated class fails the build at author time rather than surfacing as a host-trampling race in production. The failure it prevents is resource contention: too many heavy processes on one box. Its full construct-and-invariant treatment is in the appendix.

The single-writer registry

The single-writer registry is the exactly-one half, and its failure mode is what makes it a separate model. A mediator caps how many may run; a single-writer contract says one function, and only one, may write a given piece of shared state. The failure it guards against is a torn or interleaved write — two writers corrupting the same state — which a concurrency cap of two would happily permit, because two mediated processes racing on the same record is still within cap. Its quality property is single-writer coverage: every mutator of shared state has a declared monopoly, and a second discovered writer of that state is a finding. The mediator bounds contention, the single-writer registry bounds ownership, and only naming both keeps a corruption bug from hiding inside a load limit. This one cost me a day of chasing a corrupted registry file before I saw that two "safely rationed" writers were the whole problem: the semaphore was doing its job and guarding nothing that mattered. Its full construct-and-invariant treatment is in the appendix.

---

The Process view holds the system consistent under interleaving. Next, the Development view: how the code is packaged, layered, and owned.