A soundness proof for GPS and RSL with Release-Acquire semantics in Iris.

iGPS & iRSL - encoding of GPS and RSL in Iris


This repository contains the Coq development of iGPS and iRSL, which are variants of GPS and RSL in Iris.


The master branch is known to compile with:

  • Coq 8.6
  • Ssreflect 1.6.1
  • Iris 3.0


The easiest way to build the development is to use OPAM. Go to coq/ra and then make build-dep. All the dependencies will be built and installed by OPAM before the actual compilation of the development.

Manually, one can build and install Iris (currently Iris@01d12014), and then make in coq/ra.


  • The operational semantics is in machine.v. The language is in lang.v.
  • The base logic is in the base folder. The model is in base/ghosts.v. Each base rule is proven in a separate file.
  • iRSL's main rules are in rsl_instances.v. The model is in rsl.v.
  • Non-atomic rules are in na.v.
  • iGPS's rules are in the gps folder. The model is in gps/shared.v
  • Examples are in the examples folder.
  • tests/message_passing.v contains a closed proof of MP without Iris statements.