iris-atomic issueshttps://gitlab.mpi-sws.org/FP/iris-atomic/-/issues2017-09-28T22:08:04Zhttps://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/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