Concurrent Program Logic

Origin. Owicki and Gries (1976) for shared variables: parallel composition rule, interference freedom, auxiliary variables. Lamport (1977) gave a related shared-variable system. Apt, Francez, and de Roever (1980) gave the counterpart for CSP message passing, where a cooperation test replaces the interference-freedom test. Foundation for shared-memory verification.

Models. Parallel composition P₁ ‖ P₂. Shared variables. Interference freedom. Auxiliary variables for coordination.

Formalism.

Parallel composition: {P₁} S₁ {Q₁} {P₂} S₂ {Q₂} interference-free ───────────────────────────────────────────────────── {P₁ ∧ P₂} S₁ ‖ S₂ {Q₁ ∧ Q₂}

Interference freedom: For each atomic action a in S₁ and each proof outline for S₂:

a preserves S₂'s intermediate assertions
And vice versa

Proof outline: Program annotated with assertions at each point. pre{a}post for each atomic action.

Non-interference check: {Iₛ₂ ∧ pre(a)} a {Iₛ₂} for each assertion Iₛ₂ in proof outline of S₂.

Auxiliary variables: Ghost variables for coordination. Not in actual program. Updated atomically with real variables.

Await statement: await B then S end Atomically: wait for B, execute S. {P ∧ B} S {Q} ───────────────────── {P} await B then S {Q}

Resource invariants: Shared resource with invariant I. Each critical section: {I ∧ P} S {I ∧ Q}

Symbols.

Symbol	Unicode	Name	Meaning
‖	U+2016	Double vertical line / Parallel composition	Interleaved execution
∧	U+2227	Conjunction	Combines component assertions and guards
Iₛ₂	—	Outline assertion	An assertion appearing in S₂'s proof outline
pre(a)	—	Action precondition	Assertion labelling atomic action a
await	—	Await	Atomic guarded statement
I	—	Resource invariant	Restored on leaving a critical section
{P}S{Q}	—	Hoare triple	Partial correctness of a component

Metatheory. The system is sound for sequentially consistent interleaving at the declared atomic granularity, and complete relative to an oracle for the assertion language in Cook's sense, provided auxiliary variables are available — without them the parallel rule cannot record the control state on which an interleaving argument depends, and completeness fails. The interference-freedom obligation is the product of the components' proof outlines: each atomic action of one thread is checked against every assertion of every other, so the number of verification conditions grows as that product. For finite-state threads the underlying decision problem is decidable but hard — reachability in the product of k finite-state components is PSPACE-complete, a bound already implied by Kozen's 1977 result that emptiness of an intersection of finite automata is PSPACE-complete, and this is the exact source of state explosion. The boundary is sharp: Ramalingam (2000) proved that reachability becomes undecidable once two threads are recursive and synchronize, so context-sensitive and synchronization-sensitive analysis cannot both be exact.

Applies to. Shared-memory concurrency. Operating systems. Concurrent algorithms. Thread verification.

Limitations. The parallel rule is not compositional: it takes the components' proof outlines as premises, not their triples, so a component has no context-independent specification and introducing a third thread invalidates every prior interference check. Obligations scale as the product of the annotation sizes. Auxiliary variables are needed for completeness yet must be shown eliminable, and nothing produces them. Everything derivable is partial correctness under sequential consistency: divergence, deadlock, starvation, and fairness assumptions are not expressible, and a weaker memory model or a coarser-than-assumed atomic step invalidates the derivation. The await construct presupposes an atomic test-and-execute primitive that hardware need not supply. For recursive threads the reachability problem underlying the method is undecidable, so no complete algorithmic version exists.