Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2022-05-06T12:56:32Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/402iFrame performance issues2022-05-06T12:56:32ZRalf Jungjung@mpi-sws.orgiFrame performance issuesThere are some situations where iFrame is rather slow.
- For example [here](https://gitlab.mpi-sws.org/iris/examples/-/merge_requests/43#note_60969) it seems to backtrack a lot on the disjunctions. Maybe it should just not descend into ...There are some situations where iFrame is rather slow.
- For example [here](https://gitlab.mpi-sws.org/iris/examples/-/merge_requests/43#note_60969) it seems to backtrack a lot on the disjunctions. Maybe it should just not descend into disjunctions at all by default?
- Also, @tchajed noticed that `iFrame` is doing a lot of `AsFractional` everywhere, which might also be a too expensive default -- this is tracked separately in https://gitlab.mpi-sws.org/iris/iris/-/issues/351.
- Cc https://gitlab.mpi-sws.org/iris/iris/-/issues/183 for the general "power vs performance" tradeoff in `iFrame`.
- https://gitlab.mpi-sws.org/iris/iris/-/issues/434 for diverging iFrame because Hint Mode is accidentally being circumvented.https://gitlab.mpi-sws.org/iris/iris/-/issues/317Use `byte` based strings for proof mode2020-05-16T19:16:11ZRobbert KrebbersUse `byte` based strings for proof modeNewer versions of Coq have a type `byte` with 256 constructors. We could use strings based on `byte` in the proofmode. Maybe that gives a significant speed up compared to the current `ascii` based strings.
@tchajed said the construction...Newer versions of Coq have a type `byte` with 256 constructors. We could use strings based on `byte` in the proofmode. Maybe that gives a significant speed up compared to the current `ascii` based strings.
@tchajed said the construction of `byte` based strings does not exist in the Coq stdlib but can be defined as:
```
From Coq Require Import Init.Byte.
Record bytes := bytes_from_list { bytes_to_list : list byte }.
Declare Scope bytestring_scope.
Open Scope bytestring_scope.
String Notation bytes bytes_from_list bytes_to_list : bytestring_scope.
Definition foo : bytes := "foo".
```https://gitlab.mpi-sws.org/iris/iris/-/issues/419Iron slowdown investigation2021-06-17T07:20:40ZRalf Jungjung@mpi-sws.orgIron slowdown investigationIron has [slowed down by 1.8%](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=instructions&var-project=iron&var-branch=master&var-config=All&var-group=().*&from=1621369920715&to=1622831955880) just by updating Iri...Iron has [slowed down by 1.8%](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=instructions&var-project=iron&var-branch=master&var-config=All&var-group=().*&from=1621369920715&to=1622831955880) just by updating Iris from `dev.2021-03-06.3.b0708b01` to `dev.2021-06-03.0.2959900d`. I am not sure if we can do anything about that, but it would be good to at least figure out which changes caused the slowdown (though it looks like there at several, so this might be "death by a thousand cuts").https://gitlab.mpi-sws.org/iris/iris/-/issues/418library inG instances should be local2021-06-02T14:46:21ZRalf Jungjung@mpi-sws.orglibrary inG instances should be localCurrently, the `libG → inG` instances in library are usually `Global`. This is bad, we should treat them as library implementation details and make them `Local`.Currently, the `libG → inG` instances in library are usually `Global`. This is bad, we should treat them as library implementation details and make them `Local`.https://gitlab.mpi-sws.org/iris/iris/-/issues/406Slow typechecking / nonterminating Qed when using auxiliary definitions in RAs2021-03-18T08:26:06ZArmaël GuéneauSlow typechecking / nonterminating Qed when using auxiliary definitions in RAs```coq
From iris.base_logic Require Export invariants gen_heap.
From iris.program_logic Require Export weakestpre ectx_lifting.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth gmap excl list.
Defin...```coq
From iris.base_logic Require Export invariants gen_heap.
From iris.program_logic Require Export weakestpre ectx_lifting.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth gmap excl list.
Definition memspecUR : ucmraT :=
gmapUR nat (prodR fracR (agreeR (leibnizO nat))).
Definition regspecUR : ucmraT :=
gmapUR nat (prodR fracR (agreeR (leibnizO nat))).
Definition memreg_specUR := prodUR regspecUR memspecUR.
Definition exprUR : cmraT := (exclR (leibnizO nat)).
Definition cfgUR : ucmraT := prodUR (optionUR exprUR) memreg_specUR.
Class cfgSG Σ := CFGSG {
cfg_invG :> inG Σ (authR cfgUR);
cfg_name : gname }.
Section S.
Context `{cfgSG Σ}.
Lemma spec_heap_valid (e:option (excl (leibnizO nat))) a q w
(rm: gmapUR nat (prodR fracR (agreeR (leibnizO nat))))
(mm: gmapUR nat (prodR fracR (agreeR (leibnizO nat)))) :
False →
own cfg_name (● (e,(rm,mm))) ∗
own cfg_name (◯ (ε, (∅,{[ a := (q, to_agree w) ]})))
-∗ False.
Proof. intro.
iIntros "(Hown & Ha)".
iDestruct (own_valid_2 with "Hown Ha") as "HH". exfalso. assumption.
Qed.
End S.
```
The snippet above:
- works fine with Iris 3.3
- takes a very long time at Qed with Iris 3.4 (modulo replacing `cmraT` with `cmra` in the script)
The issue seems to be with the use of auxiliary definitions to define the resource algebra `cfgUR`. Manually inlining `cfgUR` and the other auxiliary definitions in the definition of `cfgSG` makes it work again with Iris 3.4.
Since the fix is relatively simple, this issue doesn't seem to be too big of a deal, but I thought that I'd report it just in case.
Coq version used: 8.12.1 in both cases.https://gitlab.mpi-sws.org/iris/iris/-/issues/347"solve_inG" is very slow for larger RA combinators2021-03-03T13:07:08ZRalf Jungjung@mpi-sws.org"solve_inG" is very slow for larger RA combinatorsIn his Iris fork, @jtassaro has a [rather large RA](https://github.com/jtassarotti/iris-inv-hierarchy/blob/0ecbb628ff5c49826873f800a2127e5bfcfb48ae/theories/base_logic/lib/wsat.v#L43) that completely explodes `solve_inG`. Before https://...In his Iris fork, @jtassaro has a [rather large RA](https://github.com/jtassarotti/iris-inv-hierarchy/blob/0ecbb628ff5c49826873f800a2127e5bfcfb48ae/theories/base_logic/lib/wsat.v#L43) that completely explodes `solve_inG`. Before https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/498, it took around 15s, and then `Qed` took another 15s.
Since !498, they just don't terminate any more. I can make the proof itself go through by adding a `simpl in *` in `solve_inG` (before [this `intros`](https://github.com/jtassarotti/iris-inv-hierarchy/blob/0ecbb628ff5c49826873f800a2127e5bfcfb48ae/theories/base_logic/lib/own.v#L45)), but then `Qed` still takes forever. To make `Qed` work I added some awful hack that seemingly successfully guides Coq towards using the right reduction strategy for `Qed`.
I am not sure what we can do here, besides entirely sealing functors and thus making them non-computational (so we'd have to prove unfolding lemmas about them all, and somehow use them in `solve_inG`).https://gitlab.mpi-sws.org/iris/iris/-/issues/321Make `contractive_proper` into a lemma, or control other instances that make ...2020-10-20T09:21:24ZPaolo G. GiarrussoMake `contractive_proper` into a lemma, or control other instances that make it costly.Successful typeclass searches for `contractive_proper` take 0.1s — as shown by replacing `contractive_proper _` with `_`. So it should maybe be disabled like `ne_proper` (see 6df6c641aadd50cd9808035f77e41048a99e6600).
Logs like https://...Successful typeclass searches for `contractive_proper` take 0.1s — as shown by replacing `contractive_proper _` with `_`. So it should maybe be disabled like `ne_proper` (see 6df6c641aadd50cd9808035f77e41048a99e6600).
Logs like https://gist.github.com/Blaisorblade/541416169b97729e60bb80fb0f259b7d reveal that the problem is that `proper_reflexive` is tried first, and then search diverges. Finding a way to blacklist certain instances for `Reflexive (equiv ==> equiv)%signature` would be useful — maybe removing them and replacing them with `Hint Extern`?https://gitlab.mpi-sws.org/iris/iris/-/issues/303Canonical structures have major performance impact2022-08-12T14:48:02ZRobbert KrebbersCanonical structures have major performance impactAs I mentioned on [Mattermost](https://mattermost.mpi-sws.org/iris/pl/49pr68ips3yuifgbd9qow6u81o), I had a [fun experiment](https://gitlab.mpi-sws.org/iris/iris/-/commit/294ef2ef2df5478db81065f6cd5edc1d831419a1) collapsing the `sbi` and ...As I mentioned on [Mattermost](https://mattermost.mpi-sws.org/iris/pl/49pr68ips3yuifgbd9qow6u81o), I had a [fun experiment](https://gitlab.mpi-sws.org/iris/iris/-/commit/294ef2ef2df5478db81065f6cd5edc1d831419a1) collapsing the `sbi` and `bi` canonical structures.
- [37.40% overall on lambdarust-weak](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=masters%2Fweak_mem&var-commit1=bcc7c0be5ba2def0989d727c97d94a8492b9e40b&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi_weak&var-commit2=4ea92744abcd644f385696c398206a20a2cab7cf&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 72.22%.
- [23.28% overall on Iron](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iron&var-branch1=master&var-commit1=4dcc142742d846037be4cd94678ff8759465e6c1&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=37f90dd22db3ca477377d16ae72d761cb617412c&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 38.13%.
- [3.8% overall on Iris](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iris&var-branch1=master&var-commit1=9b2ad256fbf948933cdbf6c313eb244fd2439bf3&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=294ef2ef2df5478db81065f6cd5edc1d831419a1&var-config2=build-coq.8.11.0&var-group=().*&var-metric=instructions), with improvements for individual files up to 13.16%.
- [5.2% overall on lamdarust master](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=master&var-commit1=fe35f4cd910f3f3235fd3c6b6c46fc142d3ce13f&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=bea9f4a02efe48a38894fe1286add7ab25a2d2de&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 10.18%.
These differences are major, especially for the projects that use BI formers (monPred in lambdarust-weak and fracPred in Iron)! So it looks like there is really something we should investigate.https://gitlab.mpi-sws.org/iris/iris/-/issues/298Guide typeclass search via more specialized typeclasses2020-06-17T16:51:55ZMichael SammlerGuide typeclass search via more specialized typeclassesFind places where a general typeclass (like `SetUnfold` before) can be split into more specialized typeclasses (like `SetUnfoldElemOf`) such that typeclass search is always guided by the head symbol. https://gitlab.mpi-sws.org/iris/stdpp...Find places where a general typeclass (like `SetUnfold` before) can be split into more specialized typeclasses (like `SetUnfoldElemOf`) such that typeclass search is always guided by the head symbol. https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/66 applied this optimization to `SetUnfold`.
cc @robbertkrebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/272Fix performance regressions in Iris and std++ in Coq 8.10.1 compared to Coq 8...2020-02-12T10:10:51ZRobbert KrebbersFix performance regressions in Iris and std++ in Coq 8.10.1 compared to Coq 8.9.0This issue is to track the status of the performance regression in Coq 8.10.1.
* [Compare Timing for std++](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=stdpp&var-branch1=master&var-commit1=9e267150f49e87f4c...This issue is to track the status of the performance regression in Coq 8.10.1.
* [Compare Timing for std++](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=stdpp&var-branch1=master&var-commit1=9e267150f49e87f4c9e15e61e5e48a2c57acf8d6&var-config1=coq-8.9.0&var-branch2=master&var-commit2=3a0c0ae002a0b51c0ab25586c6ed2fd43173aef8&var-config2=coq-8.10.1&var-group=(.*)&var-metric=instructions)
* [Compare Timing for iris](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iris&var-branch1=master&var-commit1=891124d61509345967eec12e004eda252f76342a&var-config1=coq-8.9.0&var-branch2=master&var-commit2=e46457b2a05b94c4815ec08d9e9f4506c52e0e42&var-config2=coq-8.10.1&var-group=(.*)&var-metric=instructions)
A possible cause: https://github.com/coq/coq/issues/11063https://gitlab.mpi-sws.org/iris/iris/-/issues/203Seal off local and frame-preserving update2019-11-01T12:50:04ZRalf Jungjung@mpi-sws.orgSeal off local and frame-preserving updateThat might solve `apply` diverging all the time.That might solve `apply` diverging all the time.https://gitlab.mpi-sws.org/iris/iris/-/issues/188eauto very slow when there is a chain of Iris quantifiers2019-11-01T12:49:47ZRalf Jungjung@mpi-sws.orgeauto very slow when there is a chain of Iris quantifiersSteps to reproduce:
* Change the `iIntros` hints in `ltac_tactics.v` to `iIntros (?).` and `iIntros "?".`.
* Compile `ectx_lifting.v`
`wp_lift_atomic_head_step_no_fork` takes forever:
```
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e...Steps to reproduce:
* Change the `iIntros` hints in `ltac_tactics.v` to `iIntros (?).` and `iIntros "?".`.
* Compile `ectx_lifting.v`
`wp_lift_atomic_head_step_no_fork` takes forever:
```
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
to_val e1 = None →
(∀ σ1, state_interp σ1 ={E}=∗
⌜head_reducible e1 σ1⌝ ∗
▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
⌜efs = []⌝ ∗ state_interp σ2 ∗ default False (to_val e2) Φ)
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_head_step. done.
(* now it gets slow *) eauto.
```
Something seems to be exponential in the number of quantifiers. We currently use `iIntros.` to introduce them all at once but that's more of a work-around. I can't even really figure out what is taking so long, but I can definitely see tons of `FromAssumption` in the trace.
Cc @robbertkrebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/180Explore performance implications of gen_proofmode2019-11-01T12:49:47ZRalf Jungjung@mpi-sws.orgExplore performance implications of gen_proofmodea74b8077f199e2d21ff49e91b5af0dfdcee362ff (more control over typeclass search) made lambdaRust noticeably slower.
Also see the conversation following <https://mattermost.mpi-sws.org/iris/pl/btp695ny3prqjdqzojw9sj5i9w>. In particular:
> y...a74b8077f199e2d21ff49e91b5af0dfdcee362ff (more control over typeclass search) made lambdaRust noticeably slower.
Also see the conversation following <https://mattermost.mpi-sws.org/iris/pl/btp695ny3prqjdqzojw9sj5i9w>. In particular:
> yeah, the bottelneck is definitely notypeclasses refine: https://gitlab.mpi-sws.org/FP/LambdaRust-coq/-/jobs/9346 took 29:47 user time
> btw we also have a 1min regression in this range: https://gitlab.mpi-sws.org/FP/LambdaRust-coq/compare/8799209d9c00f825e9ac059b3b864119e34f9aec...00b0c7704278028c4a73c9f0686a9070e92d3a06
> and ~30sec over https://gitlab.mpi-sws.org/FP/LambdaRust-coq/compare/474f82283e423b03ccf0adeb367e36eb68346a29...8799209d9c00f825e9ac059b3b864119e34f9aec
Looking at the [performance graph](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-project=lambda-rust&var-branch=ci%2Fgen_proofmode&var-config=All&from=1516679125714&to=now), the two commit ranges with the most sustained impact are LambdaRust-coq@c2c2b874eea8...00b0c7704278 and LambdaRust-coq@00b0c7704278...158d46797c99. They correspond to iris-coq@aa5b93f6319b9cb2d17a1c9f61947233b4033484...1a092f96b1350896c3801edb90b453f5b4d2a4cf and iris-coq@1a092f96b1350896c3801edb90b453f5b4d2a4cf...a74b8077f199e2d21ff49e91b5af0dfdcee362ff in Iris. The latter is just a74b8077f199e2d21ff49e91b5af0dfdcee362ff (more control over typeclass search), but the former is just a whole bunch of commits that, altogether, seem to have made things slower by 40sec in LambdaRust.
There is also some variation in [this part of the graph](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-project=lambda-rust&var-branch=ci%2Fgen_proofmode&var-config=All&from=1518563995005&to=1520160053680) but I am not sure if that's real or just noise.https://gitlab.mpi-sws.org/iris/iris/-/issues/172String-free proofterms2020-09-08T16:20:11ZRalf Jungjung@mpi-sws.orgString-free prooftermsThe goal of this is to end up in a situation where the proof terms constructed by the proof mode do NOT contain the variable names. Such names really should not end up in the proof term. @ppedrot and @janno are convinced this would give...The goal of this is to end up in a situation where the proof terms constructed by the proof mode do NOT contain the variable names. Such names really should not end up in the proof term. @ppedrot and @janno are convinced this would give us significant speed-up. (We have a bet going here, with the threshold being 40% speedup. Let's see. ;)
@ppedrot, @janno and me recently spent some time thinking about this and I want to write this down before we forget. The basic idea is to have a version of `envs_entails`, say `envs_entails_nameless`, that takes two lists of propositions, instead of lists of pairs of strings and propositions. Now, we can `change` back and forth between `envs_entails named_env` and `envs_entails_nameless nameless_env` -- the two are convertible as we always have concrete lists for our environments. So before we apply any Coq tactic like `apply`, we always `change` the goal to its nameless form, and then `change` it back when we are done. These conversions are not actually recorded in the proof term; they only affect the type of the evar as stored in Coq, which is irrelevant at `Qed` time. Essentially, we use the type of the evar as per-goal mutable state to store the names in.
The main problem with this is that the `coq_tactics` would have to be written in nameless style, and the Ltac tactics wrapping them would have to take care of setting the right names in the subgoals they create. However, this is a problem that any solution to the issue will have -- if strings move out of the proof terms, we can't have them in Coq-level lemmas. Maybe Ltac2/Mtac could provide some other (less hacky) form of per-goal mutable state, but that wouldn't change this problem.