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	Parallel composition
{P} C {Q}	—	Hoare triple	Partial correctness
await	—	Await	Atomic conditional
in₁, in₂	—	Auxiliary	Ghost variables
Inv	—	Invariant	Global property
⟨S⟩	—	Atomic	Atomic block

Metatheory. Sound for interleaving semantics. Complete relative to sequential. Non-interference: quadratic checking. Auxiliary variables: add expressive power. Superseded by rely-guarantee, CSL for modularity.

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

Limitations. Non-interference not compositional. Requires global reasoning. Auxiliary variables must be tracked. Doesn't scale to large programs. Modern methods (CSL, rely-guarantee) preferred.