Owicki-Gries Logic

Origin. Owicki and Gries developed method (1976). Extends Hoare logic to parallel programs. Auxiliary variables for coordination. Non-interference: parallel threads don't invalidate each other's proofs. Foundation for concurrent verification.

Models. Parallel Hoare logic. Sequential Hoare: {P} C {Q}. Parallel: {P₁} C₁ {Q₁} ∥ {P₂} C₂ {Q₂}. Non-interference: C₁'s actions preserve C₂'s proof (and vice versa). Auxiliary variables: ghost state for proof only.

Formalism.

Parallel rule: {P₁} C₁ {Q₁} {P₂} C₂ {Q₂} non-interference ───────────────────────────────────────────────── {P₁ ∧ P₂} C₁ ∥ C₂ {Q₁ ∧ Q₂}

Non-interference: Every atomic action a of C₁ must preserve validity of {pre(C₂)} C₂ {post(C₂)}. Formally: {Q ∧ pre(a)} a {Q} for each assertion Q in C₂'s proof.

Auxiliary variables: Variables in assertions but not affecting control flow. Used to relate values across threads. Must be eliminable: program correct without them.

Example (mutual exclusion): {¬in1 ∧ ¬in2} [in1 := true; CS1; in1 := false] ∥ [in2 := true; CS2; in2 := false] {¬in1 ∧ ¬in2}

Invariant: ¬(in1 ∧ in2) Requires atomic actions preserve invariant.

Atomicity: Assumes atomic actions (no interleaving within action). await b then S end: atomic conditional.

Limitations addressed: Rely-guarantee: more compositional. CSL: separating conjunction.

Symbols.

Symbol	Unicode	Name	Meaning
∥	U+2225	Parallel to / Parallel composition	Interleaved execution of two components
∧	U+2227	Conjunction	Combines component pre- and postconditions
¬	U+00AC	Negation	Used in the mutual-exclusion invariant ¬(in1 ∧ in2)
{P} C {Q}	—	Hoare triple	Partial correctness of a component
pre(a)	—	Precondition of an action	Assertion labelling atomic action a in its outline
await	—	Await	Atomic guarded statement
in₁, in₂	—	Auxiliary variables	Ghost variables recording control state
Inv	—	Global invariant	Property held across the interleaving
⟨S⟩	—	Atomic bracket	S executes without interleaving

Metatheory. The method is sound for sequentially consistent interleaving semantics at the declared granularity of atomic actions, and Owicki proved it complete relative to an oracle for the assertion language, in Cook's sense — the same expressiveness hypothesis that Hoare logic needs. Auxiliary variables are necessary rather than convenient: without them the parallel rule is incomplete, because the correctness of an interleaving can depend on control-flow information that no assertion over the program variables records, and the completeness proof works by introducing auxiliary variables that encode each thread's program counter. The interference obligations are not free — each atomic action of one component must be checked against every assertion in every other component's proof outline, so the number of verification conditions is the product of the annotation sizes and hence quadratic in the size of the annotated program for two threads, and grows with the product across k threads. The key structural fact is that the parallel rule's premises include the entire proof outlines and not merely the triples {P₁} C₁ {Q₁} and {P₂} C₂ {Q₂}; this is exactly what Jones' rely-guarantee method (1981) repaired by promoting the interference assumption into the specification itself.

Applies to. Concurrent algorithm verification. Mutual exclusion. Producer-consumer. Readers-writers. Classic synchronization. Educational foundation.

Limitations. The parallel rule is not compositional: its premises are the components' full proof outlines, so a component has no specification that survives a change of context, and adding a third thread invalidates every existing non-interference check rather than adding new ones. The obligation count is the product of the annotation sizes, which is where the growth comes from — this is a property of the rule, not of any implementation. Soundness is stated for sequential consistency and for a fixed atomic granularity; a weaker memory model, or an atomic action that turns out to compile to several machine steps, invalidates the proof. Auxiliary variables are required for completeness but must be shown eliminable, and no procedure produces them. Everything proved is partial correctness at the declared interleaving: deadlock-freedom, starvation-freedom, and fairness assumptions cannot be stated, and the await construct assumes an implementation that may not exist. Completeness is only relative, and the interference checks are themselves Hoare triples needing the same assertion-language oracle.