runtimeverification / evm-semantics

K Semantics of the Ethereum Virtual Machine (EVM)
BSD 3-Clause "New" or "Revised" License
509 stars 144 forks source link

WordStack optimizations #2632

Closed PetarMax closed 1 month ago

PetarMax commented 1 month ago

This PR introduces some optimizations that should allows us to manipulate word stacks more efficiently..

ehildenb commented 1 month ago

We really need some performance metrics posted here, both for Haskell and LLVM backend.

PetarMax commented 1 month ago

What would be the best way to get the metrics? For the LLVM backend, I guess the conformance test suite.

geo2a commented 1 month ago

@PetarMax regarding the performance metrics for the Haskell backend: please ask @anvacaru, I remember that he has adapted our Nix-based performance measurement script to vary the version of KEVM instead of HB. This thould get tou a table comparing KEVM master vs branch, while keeping the K and HB versions fixed.

PetarMax commented 1 month ago

Just to say regarding concrete execution and the LLVM backend - the moment that we have anything symbolic in the word stack, we cannot use the LLVM backend to compute anything over it, even if it doesn't depend on the symbolicness (say, length), and so any tail recursion optiimisations will only work for purely concrete word stacks.

anvacaru commented 1 month ago

Yes, I put something together from the Haskell Backend's test-performance-kevm.sh script.

I would run this profile-kevm script for both branches I'm interested in.

export KEVM_VERSION=master; profile-kevm
export KEVM_VERSION=wordstack-optimizations; profile-kevm

then I would use the compare_logs.py logfile_1 logfile_2 to generate the table with the time values.

I will give it a go in the background and post the results here.

anvacaru commented 1 month ago

It seems like these optimizations are causing a slowdown. @PetarMax can you confirm this?

Test master-1bd8e09de time wordstack-optimizations-3801e920c time (master-1bd8e09de/wordstack-optimizations-3801e920c) time
examples/sum-to-n-spec.k 91.79 103.43 0.8874601179541719
mcd/end-subuu-pass-spec.k 55.36 60.03 0.9222055638847243
mcd-structured/end-subuu-pass-spec.k 55.54 59.61 0.9317228652910585
erc20/ds/transferFrom-failure-1-b-spec.k 122.0 130.18 0.937163926870487
mcd-structured/dai-adduu-fail-rough-spec.k 48.6 51.55 0.9427740058195927
kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k 63.9 67.69 0.9440094548677795
erc20/ds/transferFrom-failure-1-c-spec.k 99.87 105.54 0.9462762933484935
mcd/dai-adduu-fail-rough-spec.k 48.6 51.33 0.9468147282291058
benchmarks/functional-spec.k 357.99 376.78 0.9501300493656777
erc20/ds/transferFrom-failure-2-c-spec.k 47.24 49.7 0.9505030181086519
mcd-structured/flipper-addu48u48-fail-rough-spec.k 48.03 50.49 0.9512774806892453
kontrol/test-emitcontracttest-testexpectemitcheckemitter-0-spec.k 47.64 50.05 0.951848151848152
mcd/flipper-addu48u48-fail-rough-spec.k 47.99 50.36 0.9529388403494837
erc20/ds/balanceOf-spec.k 46.33 48.55 0.9542739443872297
mcd-structured/functional-spec.k 324.39 339.38 0.9558312216394602
benchmarks/storagevar00-spec.k 42.9 44.76 0.9584450402144772
kontrol/test-arithmetictest-test_wmul_weakly_increasing_positive-uint256-uint256-0-spec.k 67.85 70.71 0.9595531042285391
benchmarks/overflow00-overflow-spec.k 43.72 45.55 0.9598243688254665
mcd-structured/cat-exhaustiveness-spec.k 104.35 108.7 0.9599816007359705
benchmarks/ecrecover00-sigvalid-spec.k 53.29 55.48 0.9605263157894737
mcd-structured/flopper-tick-pass-rough-spec.k 83.28 86.64 0.961218836565097
kontrol/test-countertest-testincrement-0-spec.k 85.3 88.7 0.9616685456595264
examples/solidity-code-spec.md 105.59 109.78 0.9618327564219348
kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k 63.52 66.04 0.9618413082980012
kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k 46.77 48.54 0.9635352286773795
benchmarks/requires01-a0le0-spec.k 43.32 44.95 0.9637374860956618
mcd/functional-spec.k 548.15 568.02 0.9650188373648815
mcd-structured/flopper-file-pass-rough-spec.k 17.9 17.28 1.0358796296296295
mcd/flopper-dent-guy-same-pass-rough-spec.k 641.56 610.61 1.0506870179001326
TOTAL 3452.77 3560.43 0.9697620792994105