Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Df/caching termlike hashes #3338

Merged
merged 7 commits into from Nov 22, 2022
Merged

Df/caching termlike hashes #3338

merged 7 commits into from Nov 22, 2022

Conversation

treeowl
Copy link
Contributor

@treeowl treeowl commented Oct 26, 2022

Cache the hash of the TermLikeF in the TermLike, and extract it in the Hashable instance instead of recursing into the TermLikeF.

The precomputed hash in produced using the derived Hashable instance of TermLikeF, which will call hash on the respective sub-structure (like And, Or, ...), wrapped into one of the TermLikeF constructors. For all such sub-structures, the derived Hashable instance will then recurse into the contents (containing a TermLike again for the case of TermLike), thereby using the cached hashes directly instead of performing a deep recursion.

Partially addresses #3113

Fixes #nnnn

Scope:

Estimate:


Review checklist

The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.

  • Summary. Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history.
  • Documentation. Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing.
  • Tests. Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests.
  • Clean up. The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes!

@treeowl treeowl mentioned this pull request Oct 26, 2022
4 tasks
@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-sum-to-n.sh -0.000005 0
test/regression-evm/test-dsvalue-peek-pass-rough.sh -0.000019 -0.001585
test/regression-evm/test-flipper-addu48u48-fail-rough.sh 0.000001 0.000004
test/regression-evm/test-lemmas.sh -0.000005 0
test/regression-evm/test-totalSupply.sh -0.000001 0.000007
test/regression-evm/test-functional.sh 0.000012 0.000026
test/regression-evm/test-storagevar03.sh -0.000000 0.000026
test/regression-wasm/test-wrc20.sh -0.235160 0.086063
test/regression-wasm/test-locals.sh -0.007116 0.025619
test/regression-wasm/test-memory.sh -0.031959 0.021318
test/regression-wasm/test-loops.sh -0.059915 0.025880
test/regression-wasm/test-simple-arithmetic.sh -0.011376 0.021209

@jberthold
Copy link
Member

  • to fix the Update/Style issues: look at what nix run .#format (or run scripts/fourmolu.sh if you have fourmolu installed)
  • for the failing integration test where the ordering of outputs changed, you can create a new "golden" output file using
$ cd test/regression-c
$ make golden

This re-creates the one *.out.golden file that is checked after running the shell script.

@jberthold
Copy link
Member

See #3303 for an example how to trigger a profiling run with a tarball (this tarball is from #3286)

@github-actions
Copy link

github-actions bot commented Nov 1, 2022

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-sum-to-n.sh 0.000006 0
test/regression-evm/test-dsvalue-peek-pass-rough.sh -0.000052 0.000053
test/regression-evm/test-flipper-addu48u48-fail-rough.sh -0.000001 0.000000
test/regression-evm/test-lemmas.sh 0.000029 0
test/regression-evm/test-totalSupply.sh -0.000006 0
test/regression-evm/test-functional.sh 0.000017 0
test/regression-evm/test-storagevar03.sh -0.000004 0
test/regression-wasm/test-wrc20.sh -0.235131 0.082518
test/regression-wasm/test-locals.sh -0.007116 0.025618
test/regression-wasm/test-memory.sh -0.031950 0.021319
test/regression-wasm/test-loops.sh -0.059957 0.025880
test/regression-wasm/test-simple-arithmetic.sh -0.011475 0.021209

@treeowl treeowl force-pushed the df/caching-termlike-hashes branch 2 times, most recently from 2e495a1 to 7316801 Compare November 1, 2022 16:00
@github-actions
Copy link

github-actions bot commented Nov 1, 2022

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-sum-to-n.sh 0.000004 0
test/regression-evm/test-dsvalue-peek-pass-rough.sh 0.000111 0.002451
test/regression-evm/test-flipper-addu48u48-fail-rough.sh 0.000000 0.000000
test/regression-evm/test-lemmas.sh -0.000017 0
test/regression-evm/test-totalSupply.sh -0.000007 -0.000000
test/regression-evm/test-functional.sh 0.000051 0
test/regression-evm/test-storagevar03.sh 0.000003 0
test/regression-wasm/test-wrc20.sh -0.235205 0.085991
test/regression-wasm/test-locals.sh -0.007116 0.025618
test/regression-wasm/test-memory.sh -0.032096 0.021318
test/regression-wasm/test-loops.sh -0.059970 0.025880
test/regression-wasm/test-simple-arithmetic.sh -0.011430 0.021206

@treeowl treeowl force-pushed the df/caching-termlike-hashes branch 2 times, most recently from 699ae15 to 82e7c64 Compare November 8, 2022 16:21
@ana-pantilie ana-pantilie self-requested a review November 8, 2022 16:25
@github-actions
Copy link

github-actions bot commented Nov 8, 2022

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-sum-to-n.sh 0.000002 0
test/regression-evm/test-dsvalue-peek-pass-rough.sh 0.000040 -0.006290
test/regression-evm/test-flipper-addu48u48-fail-rough.sh -0.000000 0
test/regression-evm/test-lemmas.sh 0.000040 0
test/regression-evm/test-totalSupply.sh 0.000002 -0.000000
test/regression-evm/test-functional.sh -0.000010 0
test/regression-evm/test-storagevar03.sh 0.000006 0
test/regression-wasm/test-wrc20.sh -0.235135 0.095871
test/regression-wasm/test-locals.sh -0.007104 0.025618
test/regression-wasm/test-memory.sh -0.031854 0.024929
test/regression-wasm/test-loops.sh -0.059836 0.024503
test/regression-wasm/test-simple-arithmetic.sh -0.011448 0.021159

@treeowl
Copy link
Contributor Author

treeowl commented Nov 14, 2022

/KEVM-perf-run

@github-actions
Copy link

Cache the hash of the `TermLikeF` in the `TermLike`, and extract it
in the `Hashable` instance instead of recursing into the `TermLikeF`.

The precomputed hash in produced using the derived `Hashable` instance
of `TermLikeF`, which will call `hash` on the respective sub-structure
(like `And`, `Or`, ...), wrapped into one of the `TermLikeF`
constructors.  For all such sub-structures, the derived `Hashable`
instance will then recurse into the contents (containing a `TermLike`
again for the case of `TermLike`), thereby using the cached hashes
directly instead of performing a deep recursion.

Partially addresses #3113
Write a specialized

    from :: TermLike Concrete -> TermLike variable

I was hoping this would remove a number of the new `Hashable`
constraints; unfortunately it was not so successful in that regard.  It
did, however remove quite a lot of `InternalVariable` constraints, so I
guess that's a win.
`fourmolu` support for CPP is experimental, limited, and
basically buggy. It's apparently okay to make whole top-level
declarations conditional, so let's do it that way.
@treeowl
Copy link
Contributor Author

treeowl commented Nov 14, 2022

/KEVM-perf-run

@github-actions
Copy link

@treeowl
Copy link
Contributor Author

treeowl commented Nov 14, 2022

The KEVM test suggests I lack adequate permissions.

@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-sum-to-n.sh 0.000003 0
test/regression-evm/test-dsvalue-peek-pass-rough.sh -0.000054 0.002107
test/regression-evm/test-flipper-addu48u48-fail-rough.sh 0.000002 0
test/regression-evm/test-lemmas.sh 0.000019 0
test/regression-evm/test-totalSupply.sh -0.000001 0
test/regression-evm/test-functional.sh 0.000047 0
test/regression-evm/test-storagevar03.sh 0.000005 0
test/regression-wasm/test-wrc20.sh -0.246006 -0.209063
test/regression-wasm/test-locals.sh -0.007110 0.025618
test/regression-wasm/test-memory.sh -0.031978 0.021301
test/regression-wasm/test-loops.sh -0.060928 0.025864
test/regression-wasm/test-simple-arithmetic.sh -0.011540 0.021159

@jberthold
Copy link
Member

The KEVM test suggests I lack adequate permissions.

That's a gotcha in the github settings - you need to be publicly a member of the RV organosation, i.e. make your membership publicly visible.
The /KEVM-perf-run might still not work properly at the moment, though - unfortunately there is a problem that I was unable to track down.

@github-actions
Copy link

@github-actions
Copy link

@treeowl
Copy link
Contributor Author

treeowl commented Nov 14, 2022

/KEVM-perf-run

@github-actions
Copy link

Running KEVM test with 1e6ae6c and K version as https://github.com/runtimeverification/haskell-backend/actions/runs/3466091969

@treeowl
Copy link
Contributor Author

treeowl commented Nov 15, 2022

Profiling? Maybe?

@github-actions
Copy link

Running test with 1e6ae6c and kevm-bug-storagevar03-with-conditions.tar.gz as https://github.com/runtimeverification/haskell-backend/actions/runs/3466278670

@github-actions
Copy link

github-actions bot commented Nov 15, 2022

KEVM test finished: https://github.com/runtimeverification/haskell-backend/actions/runs/3466091969

EDIT: pasting results here 🎉 looks like a consistent 10% speedup 🎉

Test 1e6ae6c time 78738f3 time Ratio
erc20/hkg/transferFrom-failure-1-spec.k 569.81 680.58 0.8372417643774427
erc20/hkg/transferFrom-success-2-spec.k 492.68 574.97 0.8568794893646625
erc20/ds/transferFrom-failure-1-d-spec.k 380.28 442.83 0.8587494072217329
erc20/hkg/transferFrom-failure-2-spec.k 427.18 495.48 0.8621538709937838
erc20/ds/transferFrom-failure-2-c-spec.k 264.61 306.57 0.8631307694816845
specs/mcd/end-subuu-pass-spec.k 160.04 184.76 0.8662048062351159
erc20/ds/transferFrom-failure-2-a-spec.k 641.78 737.34 0.8703990018173433
erc20/ds/approve-success-spec.k 512.32 586.7 0.8732231123231635
erc20/hkg/approve-spec.k 190.26 216.87 0.8772997648360769
specs/mcd/vow-fess-fail-rough-spec.k 480.69 547.36 0.8781971645717627
erc20/ds/transfer-failure-1-c-spec.k 358.42 407.46 0.879644627693516
specs/mcd/vow-flog-fail-rough-spec.k 449.0 508.71 0.8826246781073697
specs/mcd/vat-move-diff-rough-spec.k 870.57 985.93 0.8829937216638098
erc20/ds/transfer-success-2-spec.k 837.56 948.17 0.8833437041880675
specs/mcd/flipper-addu48u48-fail-rough-spec.k 128.34 145.26 0.8835192069392813
erc20/ds/transfer-failure-1-a-spec.k 731.42 826.11 0.8853784604955756
erc20/ds/transfer-failure-2-b-spec.k 308.23 347.86 0.8860748577013742
erc20/hkg/transfer-failure-1-spec.k 322.14 363.51 0.8861929520508377
specs/mcd/flopper-cage-pass-spec.k 287.73 324.09 0.8878089419605666
specs/mcd/cat-exhaustiveness-spec.k 209.4 234.88 0.8915190735694823
specs/mcd/cat-file-addr-pass-rough-spec.k 310.27 347.6 0.8926064441887226
erc20/hkg/transfer-success-1-spec.k 411.5 460.09 0.8943902279988698
erc20/hkg/transfer-success-2-spec.k 255.32 285.34 0.8947921777528562
specs/mcd/vat-deny-diff-fail-rough-spec.k 550.0 614.48 0.8950657466475719
erc20/hkg/allowance-spec.k 166.4 185.27 0.898148647919253
specs/mcd/dai-symbol-pass-spec.k 289.07 321.52 0.8990731525255039
specs/mcd/vat-subui-pass-rough-spec.k 495.49 548.0 0.9041788321167883
erc20/hkg/transfer-failure-2-spec.k 223.7 247.39 0.9042402684021181
erc20/ds/transfer-failure-2-a-spec.k 640.61 707.97 0.9048547254827182
specs/mcd/vat-mului-pass-spec.k 362.38 400.29 0.9052936620949811
erc20/ds/allowance-spec.k 327.45 361.61 0.9055335859074694
specs/benchmarks/encode-keccak00-spec.k 461.0 508.98 0.9057330346968446
specs/mcd/vat-addui-fail-rough-spec.k 350.64 386.79 0.9065384317071278
specs/benchmarks/encodepacked-keccak01-spec.k 251.89 277.46 0.9078425719022561
erc20/ds/balanceOf-spec.k 227.02 249.73 0.9090617867296681
specs/benchmarks/requires01-a0gt0-spec.k 190.29 209.25 0.9093906810035842
specs/bihu/forwardToHotWallet-failure-1-spec.k 285.95 313.62 0.9117722084050761
specs/bihu/forwardToHotWallet-failure-2-spec.k 398.02 435.84 0.9132250367107195
specs/mcd/vat-subui-pass-spec.k 495.69 542.07 0.9144390945818804
specs/benchmarks/staticloop00-a0lt10-spec.k 314.97 344.23 0.914998692734509
specs/mcd/dai-adduu-fail-rough-spec.k 121.87 133.16 0.9152147792129769
specs/mcd/vat-subui-fail-rough-spec.k 357.73 390.44 0.9162227230816515
erc20/hkg/balanceOf-spec.k 135.31 147.37 0.9181651625161159
specs/benchmarks/staticarray00-spec.k 253.21 275.76 0.9182259936176386
erc20/ds/approve-failure-spec.k 157.31 171.15 0.9191352614665498
specs/benchmarks/storagevar02-nooverflow-spec.k 173.98 189.15 0.9197991012424002
specs/bihu/forwardToHotWallet-failure-3-spec.k 446.52 483.57 0.9233823438178547
specs/benchmarks/requires01-a0le0-spec.k 150.75 163.25 0.9234303215926493
specs/mcd/flipper-ttl-pass-spec.k 394.03 426.38 0.9241287114780242
specs/mcd/flipper-tau-pass-spec.k 410.74 443.14 0.9268854086744596
specs/bihu/forwardToHotWallet-success-2-spec.k 828.67 891.61 0.929408597929588
specs/benchmarks/bytes00-spec.k 313.88 337.68 0.929519071310116
specs/benchmarks/overflow00-nooverflow-spec.k 193.09 207.39 0.9310477843676166
specs/benchmarks/storagevar01-spec.k 160.37 172.08 0.9319502556950255
specs/bihu/forwardToHotWallet-failure-4-spec.k 815.01 873.55 0.9329860912369069
specs/benchmarks/keccak00-spec.k 279.04 298.96 0.9333690125769335
specs/benchmarks/overflow00-overflow-spec.k 187.18 200.1 0.935432283858071
specs/benchmarks/storagevar00-spec.k 145.77 155.72 0.936103262265605
specs/bihu/forwardToHotWallet-success-1-spec.k 825.75 881.99 0.9362351047064026
specs/benchmarks/storagevar02-overflow-spec.k 169.8 180.95 0.9383807681680023
specs/examples/sum-to-n-spec.k 70.24 74.84 0.9385355424906466
erc20/ds/totalSupply-spec.k 160.12 169.97 0.942048596811202
specs/examples/solidity-code-spec.md 245.64 260.09 0.9444423084316967
specs/benchmarks/address00-spec.k 221.32 233.74 0.9468640369641481
erc20/hkg/totalSupply-spec.k 82.84 87.2 0.95
specs/benchmarks/ecrecover00-sigvalid-spec.k 1618.47 1703.64 0.9500070437416355
specs/benchmarks/ecrecover00-siginvalid-spec.k 1342.17 1411.36 0.9509763632241244
specs/mcd/dstoken-approve-fail-rough-spec.k 1097.39 1153.6 0.9512742718446604
specs/benchmarks/storagevar03-spec.k 134.54 140.49 0.957648231190832
specs/mcd/dsvalue-read-pass-spec.k 594.02 620.26 0.957695160094154
0 101.48 105.08 0.9657403882755996
specs/bihu/functional-spec.k 50.79 52.57 0.9661403842495719
specs/functional/infinite-gas-spec.k 56.63 54.53 1.0385109114249038
specs/functional/lemmas-spec.k 68.63 65.61 1.0460295686633134
TOTAL 27994.410000000003 30769.350000000006 0.909814799467652

@github-actions
Copy link

@treeowl
Copy link
Contributor Author

treeowl commented Nov 15, 2022

Looks promising! It would be good to see what happens with the stricter versions.

@jberthold
Copy link
Member

jberthold commented Nov 15, 2022

indeed...worth a try. These are the top consumers now (from the prof file in the tarball inside the zip file 📦), still have hashWithSalt1 but a lot better than before.

COST CENTRE MODULE %time %alloc SRC
ravel Data.Generics.Internal.VL.Lens 1.8 1.6 src/Data/Generics/Internal/VL/Lens.hs:66:1-42
simplifySubstitutionWorker Kore.Simplify.SubstitutionSimplifier 1.6 1.9 src/Kore/Simplify/SubstitutionSimplifier.hs:(267,1)-(399,78)
compare Data.InternedText 1.6 0.0 src/Data/InternedText.hs:(82,5)-(86,61)
guardAgainstBottom Kore.TopBottom 1.5 0.8 src/Kore/TopBottom.hs:45:1-49
unionWith Data.Map.Strict.Internal 1.5 0.9 src/Data/Map/Strict/Internal.hs:(990,1)-(996,35)
fmap Kore.Internal.Predicate 1.4 0.3 src/Kore/Internal/Predicate.hs:171:21-27
compare Kore.Rewrite.RewritingVariable 1.3 0.0 src/Kore/Rewrite/RewritingVariable.hs:75:25-27
addConditionWithReplacements Kore.Internal.SideCondition 1.3 1.1 src/Kore/Internal/SideCondition.hs:(310,1)-(333,29)
liftSimplifier Kore.Simplify.Simplify 1.3 2.0 src/Kore/Simplify/Simplify.hs:192:5-42
second Data.Generics.Internal.Profunctor.Lens 1.2 3.1 src/Data/Generics/Internal/Profunctor/Lens.hs:(72,1)-(73,53)
repIso Data.Generics.Internal.Profunctor.Iso 1.2 2.7 src/Data/Generics/Internal/Profunctor/Iso.hs:38:1-20
first Data.Generics.Internal.Profunctor.Lens 1.1 2.7 src/Data/Generics/Internal/Profunctor/Lens.hs:(67,1)-(68,53)
substitute Kore.Internal.TermLike.TermLike 1.1 1.6 src/Kore/Internal/TermLike/TermLike.hs:(871,5)-(969,57)
project Kore.Internal.Predicate 1.1 4.3 src/Kore/Internal/Predicate.hs:(325,5)-(327,67)
hashWithSalt1 Data.Hashable.Class 1.1 0.2 Data/Hashable/Class.hs:271:1-45
foldr Kore.Internal.MultiAnd 1.0 2.4 src/Kore/Internal/MultiAnd.hs:80:36-43
simplify Kore.Simplify.Predicate 1.0 1.1 src/Kore/Simplify/Predicate.hs:(115,1)-(188,48)
attemptEquation Kore.Equation.Application 1.0 1.1 src/Kore/Equation/Application.hs:(125,1)-(216,38)
pure SMT 0.9 1.2 src/SMT.hs:512:10-20
insert Data.Set.Internal 0.6 1.2 src/Data/Set/Internal.hs:(532,1)-(544,48)
matchWith Kore.Variables.Binding 0.5 1.3 src/Kore/Variables/Binding.hs:(106,1)-(108,44)
fmap Kore.Syntax.Application 0.5 1.1 src/Kore/Syntax/Application.hs:69:21-27
sendSExpr SMT.AST 0.5 1.8 src/SMT/AST.hs:(196,1)-(207,22)
alex_scan_tkn Kore.Parser.Lexer 0.5 1.4 dist/build/Kore/Parser/Lexer.hs:(891,1)-(924,67)
hPutStr Data.Text.IO 0.4 1.3 src/Data/Text/IO.hs:(182,1)-(193,56)
balanceR Data.Map.Internal 0.3 1.2 src/Data/Map/Internal.hs:(4139,1)-(4158,50)
alexGetByte Kore.Parser.Lexer 0.2 3.3 src/Kore/Parser/Lexer.x:(264,1)-(273,35)
verifySort Kore.Validate.SortVerifier 0.2 1.1 src/Kore/Validate/SortVerifier.hs:(29,1)-(62,27)

@jberthold
Copy link
Member

@treeowl ^^^ we have an automerge bot that reads this label and merges master into PR branches that are ready (i.e., does more than github's auto-merge - it also has some degree of work queue management to avoid build storms).

@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-sum-to-n.sh -0.000005 0
test/regression-evm/test-dsvalue-peek-pass-rough.sh -0.000112 0.002259
test/regression-evm/test-flipper-addu48u48-fail-rough.sh 0.000006 -0.017247
test/regression-evm/test-lemmas.sh 0.000007 0
test/regression-evm/test-totalSupply.sh 0.000002 0
test/regression-evm/test-functional.sh 0.000035 0
test/regression-evm/test-storagevar03.sh 0.000004 0
test/regression-wasm/test-wrc20.sh -0.247636 -0.212491
test/regression-wasm/test-locals.sh -0.007120 0.026404
test/regression-wasm/test-memory.sh -0.031841 0.021816
test/regression-wasm/test-loops.sh -0.060561 0.025502
test/regression-wasm/test-simple-arithmetic.sh -0.011469 0.021309

@treeowl
Copy link
Contributor Author

treeowl commented Nov 22, 2022

Aha, okay. I'll use that in the future. I was waiting for @ana-pantilie before pulling the lever on this one.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

5 participants