Rely-Guarantee Logic

Origin. Jones introduced Rely-Guarantee (1983). Compositional reasoning for concurrent programs. Rely: what environment may do. Guarantee: what this component does. Enables modular concurrent verification. Foundation for modern concurrent separation logic.

Models. Interface between component and environment. Sequential Hoare: pre/post describe state changes. Concurrent: must also describe interference. Rely R: environment's allowed transitions. Guarantee G: this thread's transitions. Composition: thread's guarantee is others' rely.

Formalism.

Rely-Guarantee specification: R, G ⊢ {P} C {Q}

P: precondition
Q: postcondition
R: rely (environment actions)
G: guarantee (this thread's actions)

Meaning: If:

Execution starts in state satisfying P
Environment's every action satisfies R Then:
Thread's every action satisfies G
If terminates, final state satisfies Q

Stability: P stable under R: if P(s) and (s,s') ∈ R, then P(s'). Rely can't invalidate preconditions. Q must be stable under R.

Parallel composition: R₁, G₁ ⊢ {P₁} C₁ {Q₁} R₂, G₂ ⊢ {P₂} C₂ {Q₂} ──────────────────────────────────────────────── R₁ ∩ R₂, G₁ ∪ G₂ ⊢ {P₁ ∧ P₂} C₁ ∥ C₂ {Q₁ ∧ Q₂} (with compatibility: G₁ ⊆ R₂ and G₂ ⊆ R₁)

Reflexivity: Id ⊆ R (rely includes stuttering).

Transitivity: R often transitive (multiple environment steps compose).

Symbols.

Symbol	Unicode	Name	Meaning
R	—	Rely	Environment may do
G	—	Guarantee	I will do
⊢	U+22A2	Entails	Specification holds
P, Q	—	Pre, Post	Conditions
∥	U+2225	Parallel	Parallel composition
stable	—	Stable	Preserved by rely

Metatheory. Sound for interleaving semantics. Compositional: reason about components separately. Subsumes Owicki-Gries. Extended to separation logic (RGSep). Underpins concurrent verification frameworks. No built-in frame, but can be added.

Applies to. Concurrent algorithm verification. Operating systems. Lock-free data structures. Device drivers. Multicore programming. Protocol verification.

Limitations. Designing R, G requires insight. Global reasoning still needed sometimes. Complex for highly concurrent code. Interference specifications manual. Automation challenging. Action granularity matters.