Simuliris Coq development

This repository contains the Coq development of Simuliris (paper presented at POPL22: https://iris-project.org/pdfs/2022-popl-simuliris.pdf). It also contains the proofs for Tree Borrows.

Prerequisites

This version is known to compile with:

• Coq 8.20.0
• A development version of Iris
• A recent version of Coq-Equations

Building from source

When building from source, we recommend to use opam (2.0.0 or newer) for installing the dependencies. This requires the following two repositories:

opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

Once you got opam set up, run make build-dep to install the right versions of the dependencies.

Structure

The project follows the following structure below the theories folder:

• logic and base_logic contain libraries for defining fixpoints as well as general ghost state constructions.
• simulation contains the language-generic parts of the framework, in particular the definition of the simulation relation and the general adequacy proof.
  • language.v contains our generic language interface.
  • slsls.v defines the simulation relation, weakest preconditions for source and target, and general rules for them.
  • lifting.v contains general lifting lemmas as well as the definition of the generic "source-safety" judgment for exploiting UB.
  • closed_sim.v contains the definition of the closed simulation (removing the call case) used in the adequacy proof.
  • behavior.v defines our notion of behavioral refinement and whole-program refinement.
  • fairness.v defines our notion of fairness and proves it equivalent to alternative definitions that are crucial for the fairness proof.
  • fairness_adequacy.v proves that the simulation relation is fair termination-preserving.
  • adequacy.v plugs this all together and shows that Simuliris's simulation in separation logic implies a meta-level simulation, and then derives our general adequacy statement.
  • gen_log_rel.v defines a language-generic version of our logical relation on open terms.
• simulang contains the definition of SimuLang and our program logics and examples for it. We have defined two program logics for SimuLang: a "simple" one without support for exploiting non-atomics, and a version extended with support for exploiting non-atomics.
  • lang.v contains the definition of SimuLang and its operational semantics, as well as its instantiation of the language interface.
  • logical_heap.v contains the ghost state for the heap.
  • heapbij.v contains the heap bijection ghost state that is used for both program logics.
  • globalbij.v contains support for global variables.
  • primitive_laws.v instantiates the simulation relation with SimuLang. It is parametric over an additional invariant on the state and proves basic proof rules for SimuLang.
  • gen_val_rel.v defines a generic value relation for SimuLang that is used by both program logics, but parametric over the notion of relatedness for locations.
  • log_rel_structural.v, gen_refl.v, and pure_refl.v contain conditions on the logical relation as well as general reflexivity proofs used by both program logics.
  • behavior.v defines our notion of behavior and contextual refinement for SimuLang.
  • simple_inv contains the simple program logic, with no support for exploiting non-atomics.
    • inv.v contains the invariant on the state (mainly the bijection, which does not allow to take out ownership) and basic laws.
    • refl.v contains the reflexivity theorem.
    • adequacy.v derives the adequacy proof of the logical relation (i.e., that it implies contextual refinement).
    • examples contains examples using this logic, see below for a list.
  • na_inv contains the non-atomic program logic, with added support for exploiting non-atomics.
    • na_locs.v contains the pure invariants and reasoning about data races.
    • inv.v contains the invariant on the state (allowing to take out ownership from the bijection), basic laws, and rules for exploiting non-atomic accesses.
    • refl.v contains the reflexivity theorem.
    • adequacy.v derives the adequacy proof of the logical relation (i.e., that it implies contextual refinement).
    • readonly_refl.v contains a reflexivity theorem for read-only expressions which allows to thread through ownership of exploited locations.
    • examples contains examples using this logic, see below for a list.
• stacked_borrows contains the port of the Stacked Borrows language and optimizations to Simuliris.
  • lang_base.v, expr_semantics.v, bor_semantics.v, and lang.v contain the language definition.
  • logical_state.v defines the invariants and instantiates the simulation relation.
  • steps_refl.v and steps_opt.v prove the main execution lemmas.
  • behavior.v defines the notion of contextual refinement and expression well-formedness.
  • adequacy.v contains the resulting adequacy proof.
  • examples contains example optimizations, see below.
• tree_borrows contains the Simuliris development of Tree Borrows. This development has its own README.

Theorems, definitions, and examples referenced in the paper

We list the relevant theorems and definitions mentioned in the paper by section.

Section 2

Section 3

Section 4

The definition of contextual refinement is language-specific as the contexts are language-specific. Similarly, the specific logical relation is specific to the different program logics (although we have factored out a common structure and other common components that can be re-used in a language-generic way, see theories/simulation/gen_log_rel.v). They are instantiated for the fundamental theorems.

Section 5

Section 6

Section 7

The optimizations ported and extended to concurrency from the original Stacked Borrows paper can be found in the following files:

• theories/stacked_borrows/examples/opt1.v
• theories/stacked_borrows/examples/opt1_down.v
• theories/stacked_borrows/examples/opt2.v
• theories/stacked_borrows/examples/opt2_down.v
• theories/stacked_borrows/examples/opt3.v
• theories/stacked_borrows/examples/opt3_down.v

Section 8

As mentioned in the related work section, we have verified the reorderings and eliminations by [Ševčík, 2011]. They can be found in file theories/simulang/na_inv/examples/program_transformations_in_weak_memory_models.v. For further information on this, we refer to Section 5 of the technical appendix.