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.

A new version of ReLoC is under development and is available online at https://gitlab.mpi-sws.org/iris/reloc/. Do check it out!

• Read a recent (2020) pre-print describing ReLoC ReLoaded.
• Check out an accompanying Technical appendix (last edited June 24, 2020).

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.

• 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.

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

• LICS 2018 Preprint
• Technical report, contains some notes on the formalisation, linking the rules, proofs and statements from the paper to those in the Coq source code
• LICS slides
• Slides from the Logic and Semantics seminar in Aarhus
• Slides from the EUTypes meeting in Krakow by Robbert Krebbers