iris-atomic merge requestshttps://gitlab.mpi-sws.org/FP/iris-atomic/-/merge_requests2018-07-13T11:16:45Zhttps://gitlab.mpi-sws.org/FP/iris-atomic/-/merge_requests/7port to new atomic triples2018-07-13T11:16:45ZRalf Jungjung@mpi-sws.orgport to new atomic triplesI also removed atomic_incr.v because it is now [in Iris](https://gitlab.mpi-sws.org/FP/iris-coq/blob/33f0c2792eba821c734147c7aa4b6f6f086d8458/theories/heap_lang/lib/increment.v), generalized to work on an arbitrary logically atomic heap....I also removed atomic_incr.v because it is now [in Iris](https://gitlab.mpi-sws.org/FP/iris-coq/blob/33f0c2792eba821c734147c7aa4b6f6f086d8458/theories/heap_lang/lib/increment.v), generalized to work on an arbitrary logically atomic heap.
This relies on https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/163 being merged.https://gitlab.mpi-sws.org/FP/iris-atomic/-/merge_requests/6port to savedPred2017-11-22T12:40:12ZRalf Jungjung@mpi-sws.orgport to savedPredDepends on https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/86Depends on https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/86https://gitlab.mpi-sws.org/FP/iris-atomic/-/merge_requests/4Bump Iris version to match LambdaRust-Coq.2017-09-22T08:42:15ZGhost UserBump Iris version to match LambdaRust-Coq.https://gitlab.mpi-sws.org/FP/iris-atomic/-/merge_requests/3Improve build system & Update dependency2016-11-16T00:52:08ZGhost UserImprove build system & Update dependencyhttps://gitlab.mpi-sws.org/FP/iris-atomic/-/merge_requests/2Iris as submodule; CI support2016-11-08T09:13:02ZRalf Jungjung@mpi-sws.orgIris as submodule; CI supportThis adds Iris as a submodule, matching the structure in https://gitlab.mpi-sws.org/FP/LambdaRust-coq/. Furthermore, it sets up the CI so after pushing, the repo is built against the given Iris version (with a cache to avoid needless reb...This adds Iris as a submodule, matching the structure in https://gitlab.mpi-sws.org/FP/LambdaRust-coq/. Furthermore, it sets up the CI so after pushing, the repo is built against the given Iris version (with a cache to avoid needless rebuilding of Iris).
@zhangz if you have any unpushed changes, please push them. This branch moves all files to a subfolder `theories/`, so it will conflict with any other change.https://gitlab.mpi-sws.org/FP/iris-atomic/-/merge_requests/1Simpler syncer specs2016-11-07T12:46:32ZRalf Jungjung@mpi-sws.orgSimpler syncer specsThis simplifies the syncer specs.
The sequential syncer only is slightly improved, by changing
```
Definition synced R (f' f: val) :=
(□ ∀ P Q (x: val), ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) →
({{ P x }} f' ...This simplifies the syncer specs.
The sequential syncer only is slightly improved, by changing
```
Definition synced R (f' f: val) :=
(□ ∀ P Q (x: val), ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) →
({{ P x }} f' x {{ v, Q x v }}))%I.
```
such that `P`, `Q` don't factor in a dependency on `x` any more. Since all three are quantified at the same time, the two specs are equivalent -- and the one where `P` is not a predicate and `Q` is exactly the postcondition is arguably simpler:
```
Definition synced R (f f': val) :=
(□ ∀ P Q (x: val), ({{ R ★ P }} f x {{ v, R ★ Q v }}) →
({{ P }} f' x {{ Q }}))%I.
```
For the atomic spec, the changes are deeper. The currying on some location `l` is entirely removed. `is_atomic_syncer` better mirrors `is_syncer` from the sequential version. And finally, we use "original" atomic triples and not some modified version thereof (so `atomic_triple_base` is killed).
TODO: Fix `atomic_pcas.v`, it relied on the location currying done by `atomic_sync.v`. However, I don't entirely grok that file. @zhangz could you give that a look?