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.

Metatheory. Soundness is with respect to sequentially consistent interleaving semantics, and the apparent circularity of the parallel rule — G₁ ⊆ R₂ together with G₂ ⊆ R₁ — is discharged by well-founded induction on the length of the interleaved computation, since each step's guarantee depends only on relies established at strictly earlier steps. Xu, de Roever, and He (1997) gave the soundness and relative-completeness proof; completeness is relative in Cook's sense and, as in Owicki–Gries, requires auxiliary variables. The gain over interference-freedom checking is exact rather than rhetorical: interference is discharged by stability, a check that P and Q are closed under R and involves only one component's assertions, so the obligation count grows with the number of components rather than with their product, and each component's specification R, G ⊢ {P} C {Q} is a self-contained interface reusable in any context whose guarantee is contained in R. Every Owicki–Gries proof can be recast as a rely-guarantee proof. RGSep (Vafeiadis and Parkinson 2007) and SAGL (Feng, Ferreira, and Shao 2007) combine the method with separation logic, splitting the state into thread-local parts governed by the frame rule and shared parts governed by R and G.

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

Limitations. R and G are binary relations on states, and that is the expressiveness ceiling: a relation records what the environment may do but not when or how often, so "the environment may append to this list at most once" or "only after I release the lock" cannot be stated without adding auxiliary or ghost state. The stability requirement then bites from the other side — a rely weak enough to cover every interleaving may leave almost no useful assertion closed under it, and the two constraints can only be reconciled by strengthening R with protocol information the relation cannot carry. Because R and G range over the entire shared state, the method has no locality: there is no frame rule and no ownership transfer, which is why RGSep exists. The judgement is a partial-correctness judgement, so termination, deadlock-freedom, and fairness are outside it. Soundness presumes sequential consistency and a fixed atomic granularity, and completeness is only relative.

© 2026 Lingenic LLC