@@ -180,7 +180,7 @@ As mentioned in the related work section, we have verified the reorderings and e
For further information on this, we refer to Section 5 of the technical appendix.
### Mechanization notes
### Mechanization notes
* As mentioned in footnote 5, we omit assertions controlling the size of allocations which are needed for deallocating an allocation and escaping an entire allocation at once.
The resources `† l …s n` and `† l …t n` state that the allocation starting at `l` has size `n` (in source and target, respectively), and appears in the corresponding rules in Coq.
* As mentioned in the paper, the definitions in Section 6 are simplified in order to ease presentation. The full definitions (given in the appendix and used in the Coq code) are slightly more complex to obtain all of the relevant rules for exploiting non-atomic accesses.
...
...
@@ -268,10 +268,16 @@ The following list gives an overview over the examples we have proved with Simul
### Axioms
We assume the axiom of constructive indefinite description (available as `constructive_indefinite_description` in `Coq.Logic.IndefiniteDescription`) and the law of excluded middle (available as `classic` in `Coq.Logic.Classical_Prop`).
Both of these are needed in our proof of fair termination-preservation (`theories/simulation/fairness.v`).
They are known to be consistent in combination (https://github.com/coq/coq/wiki/The-Logic-of-Coq#what-axioms-can-be-safely-added-to-coq).
We assume the axiom of constructive indefinite description (available as `constructive_indefinite_description` in `Coq.Logic.IndefiniteDescription`) and the law of excluded middle (available as `classic` in `Coq.Logic.Classical_Prop`). They are known to be consistent in combination (https://github.com/coq/coq/wiki/The-Logic-of-Coq#what-axioms-can-be-safely-added-to-coq).
We use excluded middle in `behavior.v` to relate two different notions of refinement.
We have defined a more constructive notion of refinement that we prove from our simulation and a more traditional notion that we use in the paper.
We use classical reasoning (excluded middle) to get from one to the other.
We use both axioms in `fairness.v` to relate different notions of fairness.
We have a standard notion, `fair_div`, and other notions (e.g., `fair_div_coind`), which are used as intermediate steps in the adequacy proof.
The final adequacy result is only about `fair_div` (e.g., see `prog_ref` or `has_beh` in `simulation/behavior.v`).
