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)

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 control label to every atomic command, unique across all threads (section 2, pp. 3–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. for each MRD execution S = (A, lk, rf, dp), build the initial future (A, ≺) with ≺ = dp ∪ ≤|A, where ≤|A is the preserved program order restricted to the execution’s events A (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 (Example 1, section 2, p. 5; worked futures in section 4.3, pp. 10–11). 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. A read may read from any write observable to its thread and adds a reads-from edge; a write is inserted in modification order directly after an observable write; observable writes are derived from the graph as writes not succeeded in modification order by any write the thread has encountered (sections 3–4, pp. 6–10). The paper says a chosen action “is checked for consistency and added to the set of executed events” (section 4.2, p. 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) Appendix B covers both directions (pp. 20–22). The operational-to-MRD direction (Lemma 3) is argued by contrapositive. The MRD-to-operational direction (Lemma 4) is labelled a “Proof sketch” and proceeds by induction over a total acyclic extension of the union of dependency, reads-from, and preserved-order relations (Appendix B.2, pp. 21–22).

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: the precondition X implies I on the initial futures; I on the empty future implies the postcondition; I is future-stable for the program ({I} G Q {I} for every sub-future G with corresponding sub-program Q); and Init ⇒ X (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

The paper observes that the sets of futures of different threads are disjoint, and that the only inter-thread dependency in MRD is via reads-from, which does not contribute to the set of futures; this lets the monolithic invariant be decomposed into one future predicate I_t per thread (section 5, p. 12). 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 lines 3 and 4 in thread 2 (four local obligations). For global correctness the paper says the checks “are also straightforward, so omit a detailed discussion” (section 6.2, pp. 14–15). The paper also collapses event-based futures into label-based futures and notes this is valid only when the label-based representation describes exactly the futures generated by MRD, which holds for this example (section 6.2, p. 14).

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 appendix also presents a partial-conditional example (Appendix C.1, Fig. 9, p. 23), a random-number-generator (RNG) example (C.2, Fig. 10, pp. 23–24) and two dependency-chain examples, LB+data-add+ctrl (C.3, Figs. 11–12, pp. 24–25). The RNG outline establishes the postcondition [x ≉ 99] for threads 1, 2 and 3 (no thread may observe a write of 99). The paper says semantic dependencies forbid any reordering within each thread, so “its proof is straightforward”, and that the obligations were discharged “using our existing Isabelle/HOL formalisation [8] for a model that assumes program order” (Appendix C.2, p. 24). The same is said of the Fig. 11 and Fig. 12 outlines (Appendix C.3, p. 24). The paper makes no mechanization claim for the partial-conditional outline (Fig. 9).

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 Isabelle/HOL checking of the Fig. 6 outline, done by “manually encoding the re-ordering in thread 2” (section 6.2, p. 15), plus the Isabelle/HOL checks of the RNG and LB+data-add+ctrl outlines (Appendix C.2–C.3, pp. 24–25). There is no benchmark table, runtime measurement, solved-case denominator, or percentage. The examples are hand-constructed litmus tests and proof outlines.

The approach builds on MRD’s denotational semantics and dependency relation, requires that each atomic command has a unique label, and its language omits CAS, fences, non-atomic accesses and SC accesses “for simplicity” (section 2, p. 4). The text read states Lemmas 1 and 2 (the logic’s proof rules) without proofs; the only proofs given are the Theorem 1 argument in Appendix B (a sketch for one direction). The paper says “We aim to develop full mechanisation support as future work” (section 6.2, p. 15), and that the challenge of the logic is “managing the multitude of proof obligations” from the branching structure and lack of order (section 8, p. 16). Inference: the approach inherits the complexity of MRD (section 7, p. 15 calls it “remarkably complex”) and relies on the correctness of the Isabelle/HOL development for the checked outlines.

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

Last edited: 2026-10-17