ReLoC

ReLoC is a mechanised logic for interactively proving contextual refinements of programs in a language with higher-order state, fine-grained concurrency, polymorphism and existential and recursive types.

ReLoC is built on top of Iris—a state of the art concurrent separation logic.

Publications and case studies

• Mechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Library, Simon Friis Vindum, Dan Frumin, Lars Birkedal. CPP 2022.
• Contextual Refinement of the Michael-Scott Queue (Proof Pearl), Simon Friis Vindum, Lars Birkedal. CPP 2021.
• ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity, Dan Frumin, Robbert Krebbers, Lars Birkedal. LMCS 2021.
• There is also an accompanying technical appendix, describing verification of a stack with helping.
• Older conference paper, describing the first version of ReLoC.

Guide to the examples

The Rocq formalization comes with a number of examples, intended to demonstrate and evaluate ReLoC:

• The “bit” module/simple representation independence example is in examples/bit.v.
• The counter refinement and the logically atomic specification for the fine-grained counter are in lib/counter.v.
• The specifications for the spin lock are in lib/lock.v.
• The HOCAP-style specifications for the counter are in experimental/hocap/counter.v and the ticket lock refinement is in experimental/hocap/ticket_lock.v.
• Equivalences between different fixed point combinator are in lib/Y.v.
• The coin flip example is in examples/coinflip.v and the late/early choice example is in examples/lateearlychoice.v.
• The (in)equational theory of non-deterministic choice is in examples/or.v.
• Treiber stack refinement is in examples/stack/refinement.v.
• A number of “higher order functions with state” examples from Dreyer, Neis, Birkedal ’10 are in examples/various.v.
• A number of examples from SDRI are in examples/namegen.v, examples/symbol.v, and examples/cell.v.
• The stack with helping example is in examples/stack_helping/.
• The Folly queue case study is in examples/folly_queue/.