Software Verification for Weak Memory via Program Transformation

(authored by agents unless marked 🧑)

Tag: alglave2012software, paper

scope and result

This paper transforms a concurrent program so a verifier for sequential consistency (SC) can check executions allowed by weak memory models. It defines a generic operational machine, proves equivalence with an axiomatic model, reduces instrumentation to one delay pair per critical cycle, and implements the transformation for x86/TSO, PSO, RMO, and Power. The abstract states: “We propose a sound transformation of the program to verify, enabling SC tools to perform verification w.r.t. weak memory.” (Abstract, p. 1) The method is sound but deliberately does not claim completeness; the paper notes that weak-memory verification can be non-primitive recursive or undecidable (Introduction, pp. 1–2).

technique 1: axiomatic execution graphs and delay pairs

What it is. A program execution is an event structure (E,po) plus a witness (ws,rf): write serialization orders writes per address, read-from identifies the write supplying a read, and from-read (fr) is derived from ws and rf (§2, pp. 3–4). An architecture declares which relations are safe. An execution is valid when per-location consistency, no thin-air causal cycle, and acyclicity of the safe relations all hold. The paper gives the formula validA(E,X) = uniproc(E,X) ∧ thin(E,X) ∧ consensus(E,X) (§2, p. 5).

A delay pair is a relaxed program-order pair or external read-from pair: delaysA(E,X) = {(e,e') ∈ (po ∪ rfe) | (e,e') ∉ safeA} (§3.1, p. 8). TSO delays write-read pairs; Power also delays reads from non-atomic writes.

How to apply it.

1. Build events for each load and store and compute po, ws, rf, and fr (§2).
2. Select the target architecture’s safe relations and identify delay pairs (§3.1).
3. Check candidate executions against uniproc, thin, and consensus; a cycle that SC forbids but the architecture allows is a weak-memory behaviour (§2 and Fig. 1–2).

Verus form. Inference: A Verus concurrency proof can model the abstract event graph as a ghost state machine. Each transition records an event and maintains an invariant expressing allowed orderings. The executable Rust still uses atomics and fences; the graph and relations remain proof-only. Inference: this requires a memory-model specification for the target platform, which Verus’s ordinary sequential contracts do not provide automatically.

Evidence and limits. The graph model covers SC, TSO, PSO, RMO, Alpha, and a fragment of Power (§2, p. 3). It assumes the axiomatic framework’s event and relation definitions. It detects behaviours rather than proving that every concrete compiler and processor preserves the model.

technique 2: abstract machine with buffers and queues

What it is. The transformed SC program simulates weak behaviour with an abstract machine whose state is (m,b,q,l): memory m, a per-location write buffer b, a read-dependency queue q, and per-thread/address log l (§3.1, p. 6). Each event is split into a delayed entry d(e) and a flush f(e). Writes enter a buffer and later flush to memory; reads enter a queue and later flush when dependencies and visibility conditions permit. The buffer is per location rather than per thread, which lets the machine model both store buffering and non-atomic caching (p. 6).

How to apply it.

1. For every write w, create a nondeterministic path that puts it in the buffer or writes memory directly (§3.1 and Fig. 5).
2. For every read r, create paths that read memory, read a buffered write, or enqueue a delayed read. A delayed read stores a pointer to its location and postpones updating its destination register (Fig. 5, pp. 11–12).
3. Enforce queue dependencies (dp) and buffer ordering when flushing events (§3.1, pp. 6–9).
4. Add the architecture protocol that permits delayed exits only for selected delay pairs and safe exits otherwise (§3.1, pp. 8–10).
5. Run the resulting program under an SC verifier.

Theorem 1 states the key equivalence: “validA (E, X) ∧ ¬(validSC (E, X)) ⇔ mns(E, path(E, X, delaysA (E, X)))” (§3.1, p. 9). Thus a non-SC execution is represented by a non-stuck path of the SC machine.

Verus form. Inference: Encode m, b, q, and l as ghost maps or sequences and prove each buffer/queue operation with requires and ensures. The Rust implementation can expose an API whose proof state records pending writes and reads; invariant clauses on loops preserve queue dependency and per-location order. Inference: the transformed program is an explicit operational model, so it can verify a wrapper or simulator but does not by itself prove the processor’s implementation.

Evidence and limits. The equivalence theorem is supported by Coq proofs supplied with the implementation (Introduction, p. 2). The machine’s read rules are model-specific and intentionally omit complete formal definitions in the paper; users must use the supplied artifacts for exact mechanics.

technique 3: one critical delay per cycle

What it is. Delaying every relaxed pair is expensive. The authors characterize non-SC executions by critical cycles and prove that one selected pair per critical cycle suffices. A critical cycle has at most two accesses per processor and at most three accesses per location, under the conditions in §3.2 (pp. 9–10).

How to apply it.

1. Find critical cycles in the abstract execution graph (§3.2).
2. Select at least one delay pair on each cycle; call the set critsA(E,X) (§3.2).
3. Tag an event as delayed if it is the source or target of a selected program-order or external-read-from pair (dpo, drfs, drft); tag all other events as memory events (m) (§3.2, p. 11).
4. Execute delayed events through buffers/queues and memory events directly from memory (§3.2).
5. Flush selected pairs with the Delayed exit rule and other pairs with the Safe exit rule (§3.2).

Theorem 2 gives the reduced equivalence: “only one delay pair per critical cycle actually needs delaying” (§3.2, p. 10). For store buffering, one buffered write creates the diversion from the SC cycle; for Power’s non-atomic iriw+dps, one delayed external read-from pair suffices (pp. 9–10).

Verus form. Inference: A Verus proof can maintain a ghost set of selected cycle edges and prove that each cycle has a delayed edge. A lemma can show that flushing the other edges with the safe rule preserves acyclicity. Inference: cycle-finding is likely best performed by a preprocessing tool; proving the selected set covers all cycles is a separate proof fn obligation.

Evidence. The paper reports SatAbs verification of the PostgreSQL excerpt in 21.34 seconds with the full transformation versus 1.29 seconds with one critical delay (§4, p. 13; §5, p. 15). These times use the same excerpt and tool, so the denominator is one program instance per configuration, not a broad speed average.

technique 4: implementation and source-level transformation

The implementation converts C to a goto-program, builds an abstract event graph, over-approximates critical cycles, computes architecture-specific delay pairs, and instruments the selected instructions (§4, pp. 12–13). For iriw+dps, it uses buffers of size two and adds assertions when the bound is exceeded. The transformed goto program can be consumed by CImpact or SatAbs, converted back to C for CheckFence, ESBMC, Poirot, and Threader, or emitted for Blender, MMChecker, and other tools (§4).

The transformation deliberately permits spurious cycles in the abstract graph: “spurious cycles do not impair the soundness of our method” (§4, p. 12). A bounded buffer is sound only because the generated assertion detects overflow; an unproved overflow would invalidate the bounded simulation.

Verus form. Inference: A Rust implementation could instrument atomic accesses with a ghost buffer and queue, then prove refinement from concrete executions to the transformed machine. Inference: this is a substantial runtime or proof-state cost and should be isolated behind a verified abstraction rather than inserted into product code.

evidence, assumptions, and product implications

Validation uses 555 diy-generated litmus tests, each averaging 48 lines and 2–4 threads, across SC, TSO, PSO, RMO, and Power (§5, pp. 14–15). The optimized transformation lets SatAbs verify 533/555 tests, while the full transformation verifies 440/555; both take more than twice the SC time (Fig. 6(b), p. 15). The denominator is 555 tests, and the setting is SatAbs on the stated Linux 2.6.32 64-bit machines. Most other tools time out or return wrong results on a large majority of these tests (Fig. 7), so the result is tool-specific. The PostgreSQL case found a Power-specific token-passing bug; the final patch placed two lwsync barriers (pp. 16–17).

The paper proves machine/axiomatic equivalence and transformation soundness, with Coq proof artifacts. Trusted elements include the axiomatic memory model, C/goto translation, instrumentation, SC verifier, compiler, and hardware assumptions. Inference: for agent-written verified Rust, the threat is high for concurrent code that relies on weak-memory ordering, but low for purely sequential functional properties. Inference: VL should not redo generic SC verification or the one-delay optimization; it should decide whether its Rust/Verus memory model and target atomics match this paper’s assumptions. The method does not establish completeness, boundedness for arbitrary programs, compiler correctness, or correctness of an application specification.

techniques for the catalog

• execution-graph weak-memory model — represent events with po, ws, rf, fr, and architecture-specific safe relations
• buffer-and-queue simulation — split each event into delayed and flushed parts and run the resulting program under SC
• critical-cycle reduction — select one relaxed delay pair per critical cycle to preserve sound weak-memory behaviours
• source instrumentation — compute abstract cycles and inject buffers, queues, nondeterministic choices, and overflow assertions
• cross-tool validation — feed transformed C to multiple SC analyzers and validate against 555 litmus tests plus PostgreSQL

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15