Simuliris Coq development

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

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 in tree_borrows/README.md.

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.