Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version)

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

scope and result

This paper builds a deductive logic for C11-style relaxed memory in which operations may execute out of source order when no semantic dependency requires their order, while writes may also propagate non-multi-copy-atomically. It starts from the denotational MRD (Modular Relaxed Dependencies) event-structure semantics, defines an operational semantics over sets of executable futures, and then supplies Hoare and Owicki-Gries rules for proofs. The abstract states: “We prove that our operational semantics is sound and complete with respect to the denotational semantics.” (abstract, p. 1)

The motivating problem is thin-air behavior. In load buffering, a data dependency from a read to a later write creates a semantic dependency, but an independent read/write pair may reorder. The logic therefore cannot assume ordinary sequential composition. The authors state: “The key idea of our operational semantics is to take the semantic dependency relation as the only order in which programs must be executed, thereby allowing intra-thread reordering.” (section 1, p. 2)

Inference: VL should treat this as a concurrency-model and proof-architecture lesson. Verus state-machine proofs usually expose an explicit transition order; this paper shows how to index invariants by a partial-order future when relaxed atomics permit multiple legal execution orders.

technique: derive semantic dependencies and futures

MRD yields a coherent event structure containing events, conflict, partial executions, reads-from edges, justification, and preserved program order (section 2, pp. 4–5). Each atomic command has a globally unique label. Convert syntax to an atomic set, unrolling loops with fresh labels. For each MRD execution, construct a future (K, ≺) where K is the remaining event set and ≺ is semantic dependency union preserved program order. An action is available when some matching event is minimal in this order.

Apply the future construction as follows:

1. assign a unique label to every atomic assignment or load (section 2, p. 4)
2. obtain MRD’s event structure and dependency relation (section 2, pp. 4–5)
3. convert each thread to a set of labeled atomic statements, with loop iterations separately labeled (section 4.1, p. 9)
4. initialize each future with all events and the union of dependency and preserved-order edges (section 4.1, p. 9)
5. mark action a enabled when at least one future has a minimal event labeled a (section 4.1, p. 9)
6. after executing a, remove every event with that label and discard futures in which a was unavailable (section 4.1, p. 9)

The paper’s load-buffering example has a dependency from line 1 to line 2 but none from line 3 to line 4, so line 4 may execute before line 3 (section 2, pp. 4–5). The operational rule Future-Step consumes one available event, updates the tagged action graph and local registers, and replaces the future set by a . F (section 4.2, p. 10).

Inference: in Verus, represent a future as a ghost Set or Seq of action identifiers plus a relation predicate for allowed predecessors. A transition requires minimality in that relation and removes one identifier. This is an inference; Verus does not provide MRD event structures or relaxed C11 execution automatically.

technique: prove operational and denotational equivalence

The operational state contains a program’s atomic-set syntax, a weak-memory tagged action graph (D,sb,rf,mo), thread-local registers, and a set of futures. Reads add a reads-from edge from an observable write; writes update modification order and per-thread views; all consistency checks are applied incrementally (sections 3–4, pp. 6–10).

The central theorem is: “Every execution generated by the MRD model can be generated by the operational semantics, and every final state generated by the operational semantics corresponds to a complete execution of the MRD semantics.” (Theorem 1, section 4.2, p. 10) The appendix proves both directions by induction over an acyclic extension of dependency, reads-from, and preserved-order relations (Appendix B, pp. 21–23).

Inference: this two-way correspondence is a useful VL trust pattern. A Verus concurrency proof should establish that each executable transition corresponds to one abstract protocol step and that every allowed abstract step is implementable, rather than proving only forward simulation.

technique: future-indexed Hoare triples and invariants

A standard Hoare triple is strengthened to quantify over all executions under the initial future set. A future predicate I(F) maps a set of futures and a configuration to a state assertion. The single-step triple {I} G Q {I′} quantifies over every sub-future G and every enabled transition of sub-program Q (section 5, pp. 11–12).

The invariant lemma requires three conditions: the precondition implies I on the initial futures; I on the empty future implies the postcondition; and I is future-stable under every sub-future transition (Lemma 1, p. 12). This replaces a single program-counter invariant with an invariant parameterized by the remaining partial-order work.

Inference: Verus can encode I as a ghost predicate over protocol state and a ghost set of remaining actions. A while invariant alone is insufficient when independent actions can occur in either order; the invariant must quantify over both residual action sets.

technique: modular Owicki-Gries interference checks

Because futures for different threads are disjoint except for reads-from effects, the global invariant can be decomposed into one future predicate I_t per thread. Lemma 2 requires:

1. local correctness: each I_t is stable under every sub-future of thread t
2. global correctness: for distinct threads t1 and t2, every step of t2 preserves I_t1 while assuming both thread assertions

The paper summarizes the resulting obligations as: “Thus, we establish {X}P{Y} through a series of smaller proof obligations.” (section 5, p. 13) In practice, establish initialization, each thread’s initial assertion, each local step, and every cross-thread interference step (section 5, p. 13).

The load-buffering proof uses two view assertions: [x = v]_t means thread t observes the latest write of value v; [x ≈ v]_t means t may observe a write of v (section 6.1, pp. 13–14). The proof outline checks both execution orders for the unordered pair of operations in thread 2 and then checks cross-thread stability (section 6.2, pp. 14–15).

Inference: Verus state machines can use one invariant per participant and explicit interference lemmas. The paper’s view predicates correspond to ghost observations, while Verus atomic permissions and transition guards must additionally account for ownership and linear resources.

technique: validate relaxed-memory properties with view assertions

A view assertion is evaluated against the writes currently observable by a thread in the tagged action graph. Use synchronized views when the latest write must be observed and possible views when any write with a value may be observed. For the load-buffering example, assertions constrain register values and forbid impossible observations such as r1 = r2 = 1 (section 6, pp. 13–15).

The paper also presents partial-condition, random-number-generator, and dependency-chain examples. The RNG proof shows that a postcondition [x ≠ 99] holds because semantic dependencies force the relevant operations to remain ordered (Appendix C.2, pp. 23–24). The proof outlines for the other examples are checked in an existing Isabelle/HOL formalization (Appendix C.2–C.3, pp. 24–25).

Inference: a VL benchmark for verified Rust atomics should include both positive and negative litmus outcomes and require the generated proof to state which thread views are possible. A proof that assumes one global memory view would miss the paper’s central relaxed-propagation behavior.

evidence, limits, and trust

Formal evidence consists of the soundness and completeness theorem for the operational semantics (Theorem 1, p. 10), the invariant and Owicki-Gries lemmas (section 5, pp. 12–13), and mechanized checking of the example proof outlines in an Isabelle/HOL development (section 6.2, p. 15). There is no benchmark table, runtime measurement, solved-case denominator, or percentage. The examples are hand-constructed litmus tests and proof outlines.

The approach assumes MRD’s denotational semantics and dependency relation are correct, that labels uniquely identify atomic commands, and that omitted C11 features (CAS, fences, non-atomic accesses, and sequentially consistent accesses) are irrelevant to the modeled program (section 2, p. 4). It also inherits the complexity of MRD’s event-structure construction and the trusted Isabelle/HOL formalization. The paper notes that full mechanization support for the new reordered semantics remains future work (section 6.2, p. 15).

Inference: threat to VL is high for products claiming generic verified concurrency. The paper demonstrates that relaxed-order proofs need explicit partial-order state and interference obligations; Verus acceptance alone does not supply a C11 memory-model theorem. VL should reuse future-indexed invariants, local/global interference decomposition, view assertions, and bidirectional semantics proofs. It should not claim C11 relaxed-atomic correctness from ordinary sequential Verus invariants.

techniques for the catalog

• semantic dependency futures — execute only minimal events in futures ordered by dependency and preserved program order
• operational/denotational correspondence — prove both soundness and completeness between step semantics and event structures
• future-indexed Hoare logic — parameterize assertions by residual futures and require stability for every sub-future
• modular Owicki-Gries reasoning — split global invariants into local correctness and cross-thread interference obligations
• relaxed-memory view assertions — express per-thread synchronized and possible observations over tagged action graphs

Checked 2026-10-15 against the paper by a Codex agent for owicki_gries_reasoning_for_c11_programs__20261014.md: checked quotations, numbers, references, techniques, and conclusions; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: 2026-10-15