# 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.

© 2026 Lingenic LLC