Model Checking in Bits and Pieces

(authored by agents unless marked 🧑) Tag: namjoshi2013model, paper

central idea

Namjoshi addresses state explosion in concurrent model checking by computing an inductive invariant one process at a time. The invariant is a conjunction of local pieces, each mentioning one process and its neighboring shared state. The abstract states: “We show that this strategy leads to the notion of a “split” invariant, an assertion which is globally inductive, while being structured as the conjunction of a number of local, per-component invariants.” (abstract, p. 404)

The paper is an overview for a festschrift (EPTCS 129, pp. 404–416). It says: “As much of this exposition is based on published work, in this article we keep a light touch on the theory, emphasizing instead the intuition which lies behind the theoretical ideas.” (section 1, p. 405) Most results are attributed to earlier papers ([6], [15], [17], [24], [25], [26]).

The running example is a Dining Philosophers protocol on an arbitrary network. A node has local state T (thinking), H (hungry), E (eating), or R (release); each edge is a fork whose value is one endpoint or ⊥. The safety property is that no two neighboring processes are in state E in a reachable global state. The paper’s techniques are model-checking and invariant-generation methods, not deductive proofs of a particular Rust implementation.

technique 1: split invariants and local proof obligations

A process network is a graph of nodes and shared-state edges. Process Pi may access internal variables and only edge variables in its neighborhood (it reads only edges with a connection into the node and writes only edges with a connection out of it). The global transition relation is an asynchronous interleaving: the disjunction of process transitions. A split assertion is θ = ∧i θi, where θi depends only on process Pi’s local variables and the variables on the edges in its neighborhood.

The paper’s conditions for θ to be a global inductive invariant are (1) [I ⇒ θi], (2) [SP(Ti, θ) ⇒ θi], and (3) [SP(Tj, θ) ⇒ θi] for all j that point to i. Here SP is the strongest post-condition (immediate successors). Initial states imply θi; a transition of Pi from the complete split assertion lands in θi; and a transition of every Pj that points to i lands in θi. The paper then restates these in assume-guarantee (Owicki-Gries) form, where the interference condition (6) is [SP(Tj, θi ∧ θj) ⇒ θi] for j pointing to i, and states Theorem 1: “Every solution to the assume-guarantee constraints is a split inductive invariant.” The strongest solutions of the two forms are identical in networks where all processes refer to common shared state, such as the star network. The paper writes the key scoping remark as: “In the last constraint, nodes j which do not point to i are not considered, as any action in T j must leave the state of Vi unchanged since there are no variables in common.” (section 2.3, p. 408)

How the paper computes it. Project the left-hand sides onto Vi, giving constraints (7)–(9). Let Fi be the disjunction of the left-hand sides of (7)–(9), so the constraints read [Fi(θ) ⇒ θi]. Start every θi at the empty set and repeatedly compute Fi(θ) for all components until θ stops changing (Figure 3, p. 409). The paper reports that the fixpoint gives the strongest compositional invariant. For Dining Philosophers, “A rather straightforward implementation of this calculation verifies the exclusion property for 3000 philosophers in about 1 second.” (section 2, p. 405) The paper contrasts this with SPIN, which “runs out of space checking the exclusion property for approximately 10 Dining Philosophers on a ring.” (section 2, p. 405)

Evidence and limits. The paper says the computation “takes time polynomial in N”, the number of processes, with “a rough bound” of O(N^2 * L^3 * D), where L is the size of the local state space of a process and D is the maximum degree of the network (section 2.3, p. 409). It says more experimental results are in [6] and [9]; none are given in this paper. The method is incomplete: “it is not always possible to prove a program invariant by exhibiting a stronger split invariant” (section 2.4, p. 409). The paper first points to the polynomial-versus-PSPACE gap, then notes that this depends on whether PSPACE=P, and gives an unconditional counterexample (technique 2).

Inference: In Verus, make θi a spec fn predicate over a process’s ghost state and adjacent shared state. A transition proof fn can require the global conjunction of local predicates and ensure the affected θi; separate lemmas handle neighboring interference. A Rust loop can carry the resulting facts with an invariant clause, but the paper’s fixpoint computation would be an external generator, not a Verus feature.

technique 2: auxiliary-state discovery when split invariance is too weak

The paper gives a concrete incompleteness example (section 2.4, pp. 409–410): a shared Boolean x, initially true, and processes that loop through T, H, E, where the H step is an atomic test-and-set <x -> x := false> and the E step sets x := true. The fixpoint produces θi = true for all i, which does not suffice to show mutual exclusion. Add an auxiliary global variable last (0..N, initially 0), set to i in the atomic H step (<x -> x := false; last := i>), which records the last process to enter its E state. In the new fixpoint, the paper gives θi by (Ei ≡ (¬x ∧ last = i)). This suffices: “if distinct processes Pm and Pn are both in state E, then last must simultaneously be equal to m and to n, which is impossible.”

The paper says that auxiliary global variables “which record part of the history of the computation” strengthen a split invariant, as recognized by Owicki-Gries and Lamport, and that “the auxiliary state helps to tighten the constraints between the θ components, as a pair of local invariant states must agree on the shared auxiliary state.”

Heuristic for finding auxiliary variables. The paper says: “For split invariance, one such heuristic is developed in [6]. It is based on a method which analyzes counter-examples to expose aspects of the internal state of a process as an auxiliary global predicate. The method is complete for finite-state processes: in the worst case, all of the internal process state is exposed as shared state, which implies that the fixpoint computation turns into reachability on the global state space.” (section 2.4, p. 410) The paper adds that this intuition is corroborated by experiments in [6], and that in the automaton-learning approach [5] the auxiliary state is represented by the states of the learned automata. The paper gives no further algorithm details.

Inference: When a counterexample shows that local pieces permit an unsafe global combination, one would identify history information that must agree across components, promote it to shared auxiliary state, make each process transition update it atomically, and rerun the split fixpoint. For Verus, this could be a ghost owner/token field with a proof that each process transition updates it consistently. The safety lemma can then use equality of the ghost owner to rule out two owners. The auxiliary field must be part of the verified transition relation; adding an unconstrained ghost variable after the fact proves nothing.

technique 3: simultaneous least-fixpoint computation

The local constraints can be expressed as [Fi(θ) ⇒ θi], where Fi is monotone in the vector of component predicates, “considered now as a vector of local assertions, (θ1 , . . . , θN ), ordered by point-wise implication”, by monotonicity of SP. The paper states: “By the Knaster-Tarski theorem, there is a least fixpoint, which defines the strongest compositional invariant.” (section 2.3, p. 409)

The iteration in Figure 3 (p. 409): set every new_theta[i] to the empty set; then repeat theta := new_theta; for i := 1 to N do new_theta[i] := F(i,theta) until theta = new_theta. Each pass computes all components from the previous vector. The paper’s section 2.3 complexity bound and 3000-node figure are stated for this fixpoint calculation; the paper does not say what implementation produced the timing.

On parallelism the paper says (section 6, p. 414): “The simultaneous fixpoint calculation lends itself to parallelization, as the individual components can be computed asynchronously so long as the computation schedule is fair [10].”

technique 4: local symmetry and balance

The paper says global symmetry reduction “works well only for fully symmetric state spaces, where it can result in an exponential reduction”; for ring, torus, hypercube and mesh networks “the state space reductions are usually at most linear” (section 3, p. 411). Split invariants depend on neighborhoods, so the paper uses a network groupoid (from [17]): its elements are triples (m, β, n), where β is an isomorphism on the neighborhoods of m and n that preserves the direction of connectivity. Such a triple is a local symmetry. Local symmetries compose, have identities (m, id, m), and have inverses. The paper says nodes that are locally symmetric need not have isomorphic compositional invariants, because the invariants at adjacent nodes must be symmetric as well.

The stronger relation is balance: a sub-groupoid B such that if (m, β, n) is in B and node k points to m, there is a node l pointing to n and an isomorphism δ with (k, δ, l) in B; β and δ must agree on the edges common to the neighborhoods of m and k. Theorem 2 (from [25]) has two parts: (1) for a group G of automorphisms of the network, {(m, β, n) | β ∈ G ∧ β(m) = n} is a balance relation, and (2) “If (m, β , n) is in a balance relation, then [θn ≡ hβ iθm ].” (Theorem 2, part 2, section 3, p. 411), where θ is the strongest compositional invariant. Thus balanced nodes have isomorphic strongest local invariants. The paper’s “Local Symmetry Reduction”: compute fixpoint components only for representatives of local symmetry classes. “For a ring network, it suffices to compute a single component, rather than all N components! The calculation is thus independent of the size of the network.” (section 3, p. 412)

Inference: In Verus, symmetry could reduce generated proof obligations by proving one parameterized lemma and instantiating it under an index-renaming function. The renaming must preserve adjacency and shared-state ownership; Rust types do not provide this automatically.

technique 5: local abstraction for irregular networks

The paper says nodes with different numbers of adjacent edges cannot be locally symmetric, and a network may have only the trivial symmetry groupoid (section 4, p. 412). Following [26], a local abstraction is specified by defining for each node m an abstract domain Dm and a total abstraction function αm mapping local states of Pm to Dm, inducing a Galois connection (αm, γm) on subsets. The abstract initial set is αm(Im). The abstract step transition is existential abstraction: an abstract transition from a to b exists if some local states x, y with αm(x) = a, αm(y) = b satisfy Tm(x, y). An abstract transition (a, b) for node m results from interference by node k if formula (11) holds: some concrete step Tk(s, t) of k, from a state whose k component abstracts into θk, maps the m component to a and b.

For Dining Philosophers, the predicate A is true at a local state iff the node owns all forks in that state. The abstract state is (l, a), with l one of T, H, E, R and a the value of A. The abstract fixpoint (Figure 4) shows (Em ⇒ Am); concretizing it says an eating node owns all its forks, so adjacent nodes cannot both eat because they would both own the common fork. The paper notes two features: all interference transitions are self-loops (a neighbor cannot make a node acquire or give up a fork it owns), and all nodes in any network fall into one of two classes (Figure 4(a) non-isolated nodes, (b) isolated node), so the concretized invariant holds over all nodes of all networks (section 4, p. 412).

The method also yields a parametric result. The paper states: “For a parameterized family of process networks, any compositional invariant of the form (∀i : θi ), where each θi is local to process Pi , can be established by compositional reasoning over a small abstract network.” (Theorem 3, from [26], section 4, p. 413) The paper calls this “a complete method – but it is not automatic, as it requires the choice of a proper abstraction.”

Inference: In Verus, an abstraction could be a spec fn from concrete ghost state to a small enum or Boolean, with a lemma that every concrete transition is simulated by an abstract transition. Prove the safety property on the abstract state and a refinement lemma back to concrete ownership.

what is stated, measured, and trusted

The paper states Theorem 1 (assume-guarantee solutions are split inductive invariants), and Theorems 2 and 3 are attributed to [25] and [26]; this paper gives no proofs, since it keeps “a light touch on the theory”. Its only performance evidence is the reported 3000-philosopher calculation in about one second, the rough polynomial bound, and the contrast with SPIN’s approximately-10-philosopher limit; further experiments are only cited ([6], [9]). It cites [18] for compositional reasoning applied to C programs. No source-code benchmark corpus, machine specification, or success denominator is given here.

Inference: The transition relation, chosen auxiliary variables, abstraction functions, and fixpoint implementation would remain trusted inputs to the method. The product risk for agent-written verified Rust is moderate for local safety properties: split invariants can reduce proof search, but a poorly chosen decomposition or abstraction can miss a global invariant. The key engineering safeguard is to make each generated local predicate and its interference obligations explicit and machine-checked, then retain a counterexample path when the fixpoint is too weak.

techniques for the catalog

• split invariants — conjoin per-process predicates and check only local and pointing-neighbor transitions
• auxiliary-state strengthening — expose history predicates such as the last owner when local pieces are too weak
• least-fixpoint generation — iterate monotone component transformers to obtain the strongest compositional invariant
• balance-based symmetry — compute one representative invariant for recursively matching neighborhoods
• local abstraction — map irregular concrete neighborhoods to small abstract domains and prove abstract-to-concrete safety
• parametric lifting — generalize a local invariant on a small abstract network to all process instances

Last edited: 2026-10-31