IRIS-ATOMIC

Atomicity related verification based on Iris logic.

Prerequisites

This version is known to compile with:

• Coq 8.5pl2
• Ssreflect 1.6

You will furthermore need an up-to-date version of Iris. Run git submodule status to see which git commit of Iris is known to work. You can pick between using a system-installed Iris (from Coq's user-contrib) or a version of Iris locally compiled for lambda-Rust.

Building Instructions

To use the system-installed Iris (which is the default), run make iris-system. This only works if you previously built and installed a compatible version of the Iris Coq formalization. To use a local Iris (which will always be the right version), run make iris-local. Run this command again later to update the local Iris, in case the preferred Iris version changed.

Now run make to build the full development.

Update local dependency by tracking Iris master

git submodule update --remote