This repository contains the Coq development of Simuliris, additionally including the Tree Borrows Optimization Program Logic, and also some Tree Borrows optimizations not proven via Simuliris.
This repository contains the Coq development of Simuliris (paper presented at POPL22: https://iris-project.org/pdfs/2022-popl-simuliris.pdf).
## Prerequisites
...
...
@@ -21,13 +21,7 @@ installing the dependencies. This requires the following two repositories:
Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies.
Then run `make` to build everything.
Note that the project contains some `Check` and `Print Assumptions` for key lemmas, which will be printed when you run `make`. Don't be scared.
## Structure
Our fork of simuliris in particular includes the upstream version, which proves things about Simuliris, or about data races (in weak memory model), which is part of this archive file but not relevant for the paper.
The Tree Borrows development lives in `theories/tree_borrows` and has its own `README.md`, please consult that.
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.
...
...
@@ -41,10 +35,134 @@ The project follows the following structure below the `theories` folder:
*`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 program logics and examples for it. It's not the focus of this paper.
-`stacked_borrows` contains the definition of Stacked Borrows and program logics and examples for it. It's not the focus of this paper.
-`tree_borrows` contains the Tree Borrows development. See the `README.md` in that folder for more details.
-`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.
## Theorems, definitions, and examples referenced in the paper
We list the relevant theorems and definitions mentioned in the paper by section.
| Example from 3.2 | `theories/simulang/na_inv/examples/paper.v` | `load_na_sc_sim`, `load_na_sc_log`, and `load_na_sc_ctx` |
| Example from 3.2 with arbitrary read-only expressions (footnote 8) | `theories/simulang/na_inv/examples/paper.v` | `load_na_log`, and `load_na_ctx` |
| Example from 1,3.3 | `theories/simulang/na_inv/examples/paper.v` | `hoist_load_both_log`, `hoist_load_both_ctx` |
| Example from 1,3.3 with memory deallocation | `theories/simulang/na_inv/examples/data_races.v` | `hoist_load_both_log`, `hoist_load_both_ctx` |
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`
## More information
### Section 8
See the `README.md` in `theories/tree_borrows`
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.
