Skip to content
GitLab
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 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 14
    • Merge requests 14
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Merge requests
  • !733

Optimize iDestruct by avoiding superfluous iRenames

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Armaël Guéneau requested to merge Armael/iris:optimize_iDestruct into master Sep 10, 2021
  • Overview 48
  • Commits 6
  • Pipelines 12
  • Changes 7

This is not a major optimization, but it seems to be an optimization nonetheless, so I thought I'd submit it to at least get some measurements from existing iris projects. From a quick benchmark, on our project we get a ~7-8% speedup (but I expect the speedup to be lower in most cases).

The idea is to avoid unnecessary calls to iRename. Currently, when doing iDestruct "H" as "[H1 H2]", iDestruct will produce two hypotheses, generating a fresh name for the first one and reusing "H" for the second one, then will call itself recursively, renaming each hypothesis into "H1"/"H2".

These final calls to iRename are superfluous, because we could have chosen the right names directly, and those iRenames can add up to 25-30% of the time taken by iDestruct (it's the eapply of the renaming lemma that takes time, I guess just because of unification).

The first commit of the PR optimizes the split case of iDestruct (as "[H1 H2]"), as this is what I expect to be the most common use of iDestruct. The second commit optimizes the IIntuitionistic/ISpatial/IModalElim cases; the change is slightly more intrusive, as it requires generalizing the corresponding lemmas to include a renaming step.

I ran a couple synthetic microbenchmarks to confirm that this is actually achieving something.

idestruct_bench.v: https://gitlab.mpi-sws.org/-/snippets/1701 (testing the first commit) idestruct_bench_2.v: https://gitlab.mpi-sws.org/-/snippets/1702 (testing the second commit)

idestruct_bench.v:

before:
Benchmark #1: coqc idestruct_bench.v
  Time (mean ± σ):      6.105 s ±  0.092 s    [User: 5.837 s, System: 0.238 s]
  Range (min … max):    5.920 s …  6.272 s    10 runs

after:
Benchmark #1: coqc idestruct_bench.v
  Time (mean ± σ):      4.370 s ±  0.071 s    [User: 4.135 s, System: 0.216 s]
  Range (min … max):    4.271 s …  4.522 s    10 runs

idestruct_bench_2.v:

before:
Benchmark #1: coqc idestruct_bench_2.v
  Time (mean ± σ):      6.228 s ±  0.240 s    [User: 5.973 s, System: 0.235 s]
  Range (min … max):    5.638 s …  6.475 s    15 runs

after:
Benchmark #1: coqc idestruct_bench_2.v
  Time (mean ± σ):      4.644 s ±  0.442 s    [User: 4.420 s, System: 0.208 s]
  Range (min … max):    4.057 s …  5.202 s    15 runs

The measurements are kind of noisy, I suspect because part of the time is spent just doing I/O to load the iris theories; but nevertheless demonstrate that there is indeed a speedup +/- corresponding to the 25% of the time spent in iRename that I could measure before.

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: optimize_iDestruct