Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 148
    • Issues 148
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 8
    • Merge requests 8
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #20

Closed
Open
Created Jun 17, 2016 by Joseph Tassarotti@jtassaroDeveloper

wp_store/wp_load run slowly with multiple points to assumptions in context

The wp_store and wp_load tactics appear to be very sensitive to the order of points to assumptions in the context. Consider the following snippet, placed after heap_e_spec in tests/heap_lang.v

  Definition heap_e2  : expr [] :=
    let: "x" := ref #1 in
    let: "y" := ref #1 in
    '"x" <- !'"x" + #1 ;; !'"x".
  Lemma heap_e2_spec E N :
     nclose N ⊆ E → heap_ctx N ⊢ WP heap_e2 @ E {{ v, v = #2 }}.
  Proof.
    iIntros {HN} "#?". rewrite /heap_e2. iApply (wp_mask_weaken N); first done.
    wp_alloc l. wp_let.
    wp_alloc l'. wp_let.
    time wp_load.
  Abort.

The wp_load takes 109 seconds to complete on my machine. The problem appears to be in the call to iAssumptionCore in wp_load, which tries to find an assumption l |-> ?v in the context. Because of the order of assumptions, it will first try to unify with l' |-> 1. For some reason, this does not fail instantaneously. You can check that this is the source of delay with the following example:

Remark bad_unify (l l': loc): True.
Proof.
(evar (v: Z );
  let v0 := eval unfold v in v in
unify (l ↦ #v0)%I (l' ↦ #1)%I).
Abort.

The obvious work-around is to just re-order the two points to facts in the context, or use "remember" to "hide" one of them temporarily, but this is obviously brittle. I am not an expert on how unification works under the hood, so it is hard for me to diagnose why it's so slow here.

First, does this occur for others? I am using coq 8.5pl1 and ssreflect ad273277ab38b. If so, is there some more robust work-around?

Assignee
Assign to
Time tracking