ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency


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—state of the art concurrent separation logic.

ReLoC ReLoaded

A new version of ReLoC is under development and is available online at Do check it out!

ReLoC Reloaded improves on the logic described in the LICS18 paper in several ways. In terms of the formalization it works with the latest version of Iris, and it is build directly on top of heap_lang – the programming language that comes directly with Iris.

Guide to the examples

  • 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 experimental/helping/helping_stack.v.

Legacy version

Below you can find the documentation and code associated with the previous version of ReLoC.

Compiling legacy version

The legacy version of ReLoC that accompanied the LICS18 paper is still available online.

This version compiles only with older versions of Iris (and I’ve only tested it with Coq 8.6). The following libraries are the prerequisites:

Once all the dependencies are installed, just run make in the top-level directory.