feat: Rewrite simp_mem to build a new expression, thereby localizing the effects of rewrites [6/?] #237
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
bollu
changed the title
2 tasks
bollu
force-pushed
the
simp-mem-mem-omega-6
branch
from
c00bd93 to
eca1315
Compare
shigoel
reviewed
Oct 28, 2024
shigoel
reviewed
Oct 28, 2024
bollu
force-pushed
the
simp-mem-mem-omega-6
branch
from
eca1315 to
d4d23b9
Compare
…the effects of rewrites [6/?]
bollu
force-pushed
the
simp-mem-mem-omega-6
branch
from
d4d23b9 to
f119628
Compare
shigoel
reviewed
Oct 31, 2024
|
@bollu Could you turn off all the tracing options so that the build is less noisy? |
shigoel
approved these changes
Oct 31, 2024
shigoel
added a commit
that referenced
this pull request
Oct 31, 2024
### Description: We increase the ITPness of `simp_mem` by making it less of a proof hammer, and more of a user-controllable rewrite engine. Description of the new design follows: ---- The simp_mem tactic allows simplifying expressions of the form `Memory.read_bytes rbase rn (mem')`. `simp_mem` attempts to discover the result of the expression by various heuristics, which can be controlled by the end user: - (a) If `mem' = Memory.write_bytes wbase wn mem` and we know that `(rbase, rn) ⟂ (wbase, wn)`, then we simplify to `mem.read (rbase, rn)`. - (b) If `mem' = Memory.write_bytes wbase wn wval mem` and we kow that `(rbase, rn) ⊆ (wbase, wn)`, then we simplify to `wval.extract (rbase, rn) (wbase, wn)`. - (c) If we have a hypothesis `hr' : mem'.read_bytes rbase' rn' = rval`, and we know that `(rbase, rn) ⊆ (rbase', rn')`, then we simplify to `rval.extract (rbase, rn) (rbase', rn')`. These simplifications are performed by reducing the problem to a problem that can be solved by a decision procedure (`omega`) to establish which hypotheses are at play. `simp_mem` can be controlled along multiple axes: 1. The hypotheses that `simp_mem` will pass along to the decision procedure to discover overlapping reads (like `hr'`), and hypotheses to establish memory (non-)interference, such as `(rbase, rn) ⟂ (wbase, wn)`. + simp_mem using []: try to perform the rewrite using no hypotheses. + simp_mem using [h₁, h₂]: try to perform the rewrite using h₁, h₂, as hypotheses. 2. The kind of rewrite that simp_mem should apply. By default, it explores all possible choices, which might be expensive due to repeated calls to the decision procedure. The user can describe which of (a), (b), (c) above happen: + `simp_mem ⟂` : Only simplify when read is disjoint from write. + `simp_mem ⊂w` : Only simplify when read overlaps the write. + `simp_mem ⊂r hr` : Simplify when read overlaps with a known read `hr : mem.read_bytes baseaddr' n' = val`. This is useful for static information such as lookup tables that are at a fixed location and never modified. + `simp_mem ⊂r` : Simplify when read overlaps with known read from hypothesis list. 3. The targets where the rewrite must be applied. (This needs some thought: does this even make sense?) + `simp_mem at ⊢` + `simp_mem at h₁, h₂, ⊢` --- - [ ] add `simp_mem using []` - [ ] add `simp_mem ⟂/⊂w/⊂r hr/⊂r` Stacked on top of #237 --- @shilgoel the branch shows appreciable speedups, by controlling the lemmas we pass to mem_omega: In total, it goes from 34s to 13s #### Batch mode use, measured by `lake build` : * before: `lake build Proofs.Experiments.Memcpy.MemCpyVCG 33.39s user 0.89s system 99% cpu 34.512 total` * after: `lake build Proofs.Experiments.Memcpy.MemCpyVCG 12.33s user 0.56s system 97% cpu 13.206 total` #### Individual breakdown during Interactive use, measured by #time MemCpyVCG: - theorem Memcpy.extracted_2 (s0 si : ArmState) : ~ 11 seconds to 1.6 seconds(:tada: !) + before mem_omega filtering: 11214 ms . + after mem_omega filtering: 1576 ms. - theorem Memcpy.extracted_0 : ~ 12 seconds to 3.2 seconds + before mem_omega filtering: 12023 ms + after mem_omega filtering: 3128ms - theorem partial_correctness : 7.6 s to 6.6 seconds + before mem_omega filtering: 7598 + after mem_omega filtering: 6580ms (this only has a single call to mem_omega) I feel that this, plus if we get the instantiateMVars fix, will help quite a bit with scaling :slightly_smiling_face: ### Testing: What tests have been run? Did `make all` succeed for your changes? Was conformance testing successful on an Aarch64 machine? No semantics were changed, conformance succeeds. ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. Co-authored-by: Shilpi Goel <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Issues:
Resolves
Remove this section if this PR doesn't address any open issues.
Description:
A detailed description of your contribution. Why is this change
necessary?
Testing:
What tests have been run? Did
make allsucceed for your changes? Wasconformance testing successful on an Aarch64 machine?
License:
By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.