Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2021-02-16T11:03:04Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/405Tracking issue for HeapLang interpreter2021-02-16T11:03:04ZRalf Jungjung@mpi-sws.orgTracking issue for HeapLang interpreterThis is the tracking issue for the HeapLang interpreter added in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/564. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* Generalize the monad and move it to std++, and generalize the tactics for the monad.
* Find some way to avoid the `pretty_string` instance, or move it to std++.This is the tracking issue for the HeapLang interpreter added in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/564. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* Generalize the monad and move it to std++, and generalize the tactics for the monad.
* Find some way to avoid the `pretty_string` instance, or move it to std++.https://gitlab.mpi-sws.org/iris/iris/-/issues/385reshape_expr does not recognize `fill`2020-12-05T08:58:01ZRalf Jungjung@mpi-sws.orgreshape_expr does not recognize `fill`There was not much fallout from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/588, but the bits I saw look like `reshape_expr` is not able to traverse into a `fill K e`. That should be possible, right? If yes, it could avoid re-enabling that instance locally in ReLoC, C and Actris.There was not much fallout from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/588, but the bits I saw look like `reshape_expr` is not able to traverse into a `fill K e`. That should be possible, right? If yes, it could avoid re-enabling that instance locally in ReLoC, C and Actris.https://gitlab.mpi-sws.org/iris/iris/-/issues/369Document HeapLang2020-10-30T10:30:22ZRalf Jungjung@mpi-sws.orgDocument HeapLangThe HeapLang syntax, operational semantics, and lifted weakestpre rules should probably be stated in the Iris Documentation. Currently my thesis and the "Future is Ours" paper describe overlapping but incomparable subsets of the operational semantics, and there are likely bits that are missing from both.The HeapLang syntax, operational semantics, and lifted weakestpre rules should probably be stated in the Iris Documentation. Currently my thesis and the "Future is Ours" paper describe overlapping but incomparable subsets of the operational semantics, and there are likely bits that are missing from both.https://gitlab.mpi-sws.org/iris/iris/-/issues/357Cancelable locks2020-10-21T11:00:44ZRobbert KrebbersCancelable locksIt would be really useful to have a version of cancelable locks, where the `is_lock` predicate is equipped with a fraction. That way, we could have a couple of things:
1. A Hoare triple for the physical free operation `{{ is_lock lk 1 R }} free lk {{ R }}`
2. A rule `is_lock lk 1 R ==∗ ▷ R ∗ (▷ R' ==∗ is_lock lk 1 R')` that allows a "strong update" of the payload of the lock.
Now that we have the discardable fractional permissions, we could use those to get back the ordinary lock-spec by picking the fraction to be `DfracDiscarded`.
To implement this, we probably first want to generalize cancelable invariants, by a.) adding a discardable fraction b.) adding a rule for changing the proposition in case one owns the entire fraction.
Questions:
- For locks, do we want to equip `is_lock` with a fraction, or do we want to add a token `lock_own` (which would be timeless).
- If we equip `is_lock` with a fraction, we won't break backwards compatibility that much. One just needs to add `DfracDiscarded` everywhere. If we have a token for the fraction, backwards compatibility is a bigger issue. We could of course define `is_lock ... := new_is_lock ... ∗ lock_own DfracDiscarded` or something like that.
Any thoughts?It would be really useful to have a version of cancelable locks, where the `is_lock` predicate is equipped with a fraction. That way, we could have a couple of things:
1. A Hoare triple for the physical free operation `{{ is_lock lk 1 R }} free lk {{ R }}`
2. A rule `is_lock lk 1 R ==∗ ▷ R ∗ (▷ R' ==∗ is_lock lk 1 R')` that allows a "strong update" of the payload of the lock.
Now that we have the discardable fractional permissions, we could use those to get back the ordinary lock-spec by picking the fraction to be `DfracDiscarded`.
To implement this, we probably first want to generalize cancelable invariants, by a.) adding a discardable fraction b.) adding a rule for changing the proposition in case one owns the entire fraction.
Questions:
- For locks, do we want to equip `is_lock` with a fraction, or do we want to add a token `lock_own` (which would be timeless).
- If we equip `is_lock` with a fraction, we won't break backwards compatibility that much. One just needs to add `DfracDiscarded` everywhere. If we have a token for the fraction, backwards compatibility is a bigger issue. We could of course define `is_lock ... := new_is_lock ... ∗ lock_own DfracDiscarded` or something like that.
Any thoughts?https://gitlab.mpi-sws.org/iris/iris/-/issues/340Polymorphic equality for HeapLang2020-08-22T19:06:03ZDan FruminPolymorphic equality for HeapLangIt would be nice to have polymorphic equality testing, like in OCaml or StandardML.
Current equality testing is used both for CmpXchng and for `=`, so it only operates on unboxed values.It would be nice to have polymorphic equality testing, like in OCaml or StandardML.
Current equality testing is used both for CmpXchng and for `=`, so it only operates on unboxed values.https://gitlab.mpi-sws.org/iris/iris/-/issues/278Write `wp_` lemmas for array operations in a more `iApply`/`wp_apply` friendl...2019-12-12T22:47:43ZRalf Jungjung@mpi-sws.orgWrite `wp_` lemmas for array operations in a more `iApply`/`wp_apply` friendly waySee [this discussion](https://gitlab.mpi-sws.org/iris/iris/merge_requests/340#note_42362): `wp_apply` only works poorly for array accesses currently due to `Z` vs `nat` conflicts. We should find a way to do better.
Equipping `wp_load` with support for array accesses is certainly a good idea, but I think we should also figure out a way to write such lemmas in a more apply-friendly style that can be used by other lemmas without having to write a tactic for each of them.See [this discussion](https://gitlab.mpi-sws.org/iris/iris/merge_requests/340#note_42362): `wp_apply` only works poorly for array accesses currently due to `Z` vs `nat` conflicts. We should find a way to do better.
Equipping `wp_load` with support for array accesses is certainly a good idea, but I think we should also figure out a way to write such lemmas in a more apply-friendly style that can be used by other lemmas without having to write a tactic for each of them.https://gitlab.mpi-sws.org/iris/iris/-/issues/124heap_lang: mutable n-ary locations, n-ary products, n-ary sums2019-11-01T13:25:49ZRalf Jungjung@mpi-sws.orgheap_lang: mutable n-ary locations, n-ary products, n-ary sumsThe former is interesting to model more realistic linked lists. However, we still can't realistically do CAS on sum discriminants, so if we want to restrict CAS to "small" types, we may have to rewrite some examples.The former is interesting to model more realistic linked lists. However, we still can't realistically do CAS on sum discriminants, so if we want to restrict CAS to "small" types, we may have to rewrite some examples.