iris-atomic issueshttps://gitlab.mpi-sws.org/FP/iris-atomic/-/issues2018-12-19T16:24:36Zhttps://gitlab.mpi-sws.org/FP/iris-atomic/-/issues/6LICENSE missing2018-12-19T16:24:36ZRobbert KrebbersLICENSE missingThere is no LICENSE file in the development. To allow reuse, it would be good if one were added.There is no LICENSE file in the development. To allow reuse, it would be good if one were added.https://gitlab.mpi-sws.org/FP/iris-atomic/-/issues/5Better per-item spec2017-05-20T07:26:17ZGhost UserBetter per-item spechttps://gitlab.mpi-sws.org/FP/iris-atomic/-/issues/4Thread-local storage for flat combiner2017-09-28T22:08:04ZGhost UserThread-local storage for flat combinerTwo options, either by emulation (might be verbose) or by adding primitives to heap_lang.Two options, either by emulation (might be verbose) or by adding primitives to heap_lang.https://gitlab.mpi-sws.org/FP/iris-atomic/-/issues/3Better support for using logically atomic triple2017-09-28T22:08:04ZGhost UserBetter support for using logically atomic tripleCurrently, we have to manually wire together all the pieces, which is daunting ... example from `atomic_incr.v`
```
(* open the invariant *)
iInv N as (x') ">Hl'" "Hclose".
(* mask magic *)
iVs (pvs_intro_mask' (⊤ ∖ nclose N) heapN) as...Currently, we have to manually wire together all the pieces, which is daunting ... example from `atomic_incr.v`
```
(* open the invariant *)
iInv N as (x') ">Hl'" "Hclose".
(* mask magic *)
iVs (pvs_intro_mask' (⊤ ∖ nclose N) heapN) as "Hvs"; first set_solver.
iVsIntro. iExists x'. iFrame "Hl'". iSplit.
+ (* provide a way to rollback *)
iIntros "Hl'".
iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
+ (* provide a way to commit *)
iIntros (v) "[Heq Hl']".
iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
```https://gitlab.mpi-sws.org/FP/iris-atomic/-/issues/2Improve seq_spec2017-05-20T07:26:17ZGhost UserImprove seq_spechttps://gitlab.mpi-sws.org/FP/iris-atomic/-/issues/1Possible Improvements2017-09-28T22:08:04ZGhost UserPossible Improvements- [ ] Emulated thread-local storage (https://gitlab.mpi-sws.org/FP/iris-atomic/issues/4)
- [x] Better per-item spec (nested invariants?) (https://gitlab.mpi-sws.org/FP/iris-atomic/issues/5)
- [x] Simplify the spec by avoiding the curryin...- [ ] Emulated thread-local storage (https://gitlab.mpi-sws.org/FP/iris-atomic/issues/4)
- [x] Better per-item spec (nested invariants?) (https://gitlab.mpi-sws.org/FP/iris-atomic/issues/5)
- [x] Simplify the spec by avoiding the currying issues