Concurrent Program Logic

Origin. Apt, Francez, de Roever (1980). Extended Hoare logic for concurrency. Parallel composition rule. Non-interference. 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	Parallel	Composition
await	—	Await	Conditional atomic
I	—	Invariant	Resource invariant
{P}S{Q}	—	Triple	Hoare triple

Metatheory. Sound for standard interleaving. Complete relative to sequential. Non-interference decidable for finite-state.

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

Limitations. Interference checking expensive. Global reasoning needed. Auxiliary variables clutter. Partial correctness only.