RGSep & related program logics

RGSep is a program logic that combines rely-guarantee reasoning and separation logic. It has been used, both manually and automatically, to prove the correctness of several fine-grained concurrent algorithms.

Although initially developed for reasoning about programs under sequential consistency (i.e. interleaving semantics), RGSep has been recently shown to be sound under release-acquire consistency.

Main publications

• A marriage of rely/guarantee and separation logic.
  Viktor Vafeiadis, Matthew Parkinson.
  In CONCUR 2007. LNCS 4703, pp. 256-271. Springer (September 2007)
  [Paper] [@Springer] [Technical report]
  First paper about RGSep, probably difficult to read.
• Modular fine-grained concurrency verification.
  Viktor Vafeiadis.
  PhD thesis, University of Cambridge (July 2008)
  [Technical report UCAM-CL-TR-726]
  Chapter 3 of the thesis introduces RGSep in a more gentle way than the CONCUR'07 paper.
• RGSep under release/acquire consistency.
  Ellen Arlt, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 10, OOPSLA2, Article 375 (October 2026)
  [Paper] [@ACM] [Artifact @Zenodo]
  Proves soundness of (a fragment of) RGSep in a weak memory setting.

Tutorial material

• Introductory slides about RGSep
• Tutorial on rely-guarantee and separation logic

Tool support

• SmallfootRG: a memory safety checker for fine-grained concurrent singly linked list programs.
• CAVE: a more powerful tool that can infer the rely and guarantee relations and can prove linearizability of concurrent libraries.

Related program logics

• SAGL: a similar logic for assembly code.
• Local rely-guarantee: variant of RGSep supporting an interference hiding rule at the expense of additional precision requirements.
• Deny-guarantee: an extension of rely-guarantee that supports unstructured thread creation and join.
• Concurrent abstract predicates: adapts deny-guarantee to heaps and adds abstract predicates.
• Iris: a generic framework for encoding concurrent program logics

Imprint | Data protection