@@ -22,6 +22,10 @@ Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies.
## Structure
We include our fork of simuliris in its entirety.
In particular, that includes the data-race reasoning examples from the simuliris paper, as well as the Stacked Borrows development, which are not the focus of our 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.
...
...
@@ -35,134 +39,10 @@ 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 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`
-`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.
### Section 8
## More information
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.
