ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency

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

ReLoC ReLoaded

A new version of ReLoC is under development and is available online at https://gitlab.mpi-sws.org/iris/reloc/. It diverges a bit from the logic described in the LICS18 paper, but 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. Do check it out!

Documentation

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.

Overview

Examples from the paper/technical report:

Last updated: 2019-03-18 Mon 12:07

Emacs 26.2 (Org mode 9.2.4)

Validate