Skip to content

SMT retry logic changes in Kore #3860

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 5 commits into from
May 20, 2024
Merged

SMT retry logic changes in Kore #3860

merged 5 commits into from
May 20, 2024

Conversation

geo2a
Copy link
Contributor

@geo2a geo2a commented May 14, 2024 •
edited
Loading

Fixes #3859

  • if a query returns unknown, do not retry with the same timeout, use double the timeout. Scale further timeouts quadratically, rather than linearly.
  • do not retry when applying simplifications
  • add context logs for unknown predicates

@geo2a geo2a force-pushed the georgy/smt-retries branch from bc25955 to 40c912b Compare May 14, 2024 07:28
@geo2a
Copy link
Contributor Author

geo2a commented May 14, 2024 •
edited
Loading

There's significant improvement in KEVM performance:

Test georgy-smt-retries time master-b27210141 time (georgy-smt-retries/master-b27210141) time
mcd/vat-addui-pass-spec.k 141.57 162.44 0.8715217926619059
mcd/functional-spec.k 580.06 657.19 0.8826366804120572
kontrol/test-countertest-testincrement-0-spec.k 103.36 116.56 0.8867536032944406
mcd/vat-subui-pass-rough-spec.k 124.06 139.68 0.8881729667812142
bihu/forwardToHotWallet-success-1-spec.k 61.53 69.12 0.8901909722222222
mcd/vat-subui-pass-spec.k 114.37 127.92 0.894074421513446
mcd/cat-exhaustiveness-spec.k 130.49 143.75 0.9077565217391305
mcd/flipper-bids-pass-rough-spec.k 93.07 102.15 0.911111111111111
bihu/forwardToHotWallet-failure-3-spec.k 83.46 91.44 0.9127296587926509
bihu/forwardToHotWallet-success-2-spec.k 55.04 60.1 0.9158069883527454
mcd/vat-subui-fail-rough-spec.k 75.76 82.53 0.9179692233127348
kontrol/test-owneruponlytest-testincrementasowner-0-spec.k 81.95 89.01 0.9206830693180541
mcd/end-subuu-pass-spec.k 69.24 75.0 0.9231999999999999
kontrol/test-storetest-testaccesses-0-spec.k 58.95 63.84 0.9234022556390977
erc20/ds/transferFrom-failure-1-c-spec.k 111.72 120.94 0.9237638498428973
erc20/ds/transferFrom-failure-1-b-spec.k 145.95 157.83 0.9247291389469681
mcd/vat-mului-pass-spec.k 116.2 125.57 0.9253802659870989
mcd/vat-muluu-pass-spec.k 120.33 129.52 0.929045707226683
kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k 80.28 86.38 0.9293818013429035
bihu/forwardToHotWallet-failure-4-spec.k 89.96 96.76 0.9297230260438196
erc20/ds/transferFrom-failure-2-a-spec.k 83.33 89.48 0.931269557443004
kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k 93.3 99.89 0.9340274301731905
kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k 66.35 70.86 0.936353372847869
benchmarks/overflow00-nooverflow-spec.k 53.85 57.49 0.9366846408070969
kontrol/test-allowchangestest-testallow_fail-0-spec.k 59.26 63.19 0.9378066149707233
bihu/forwardToHotWallet-failure-2-spec.k 76.69 81.62 0.9395981377113451
mcd/flipper-ttl-pass-spec.k 62.83 66.84 0.9400059844404547
mcd/dsvalue-peek-pass-rough-spec.k 66.39 70.56 0.9409013605442177
erc20/ds/allowance-spec.k 58.21 61.85 0.9411479385610347
kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k 91.81 97.5 0.9416410256410257
kontrol/test-arithmetictest-test_max1_broken-uint256-uint256-0-spec.k 55.77 59.11 0.9434951784807986
erc20/ds/transfer-failure-2-a-spec.k 81.47 86.34 0.9435950891823025
kontrol/test-arithmetictest-test_wmul_weakly_increasing_positive-uint256-uint256-0-spec.k 85.8 90.87 0.9442060085836909
kontrol/test-emitcontracttest-testexpectemitdonotcheckdata-0-spec.k 59.13 62.61 0.9444178246286536
functional/abi-spec.k 78.85 83.49 0.9444244819738891
benchmarks/requires01-a0le0-spec.k 56.16 59.27 0.9475282605027837
erc20/ds/approve-failure-spec.k 55.09 58.1 0.9481927710843374
kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k 67.19 70.86 0.9482077335591307
functional/evm-int-simplifications-spec.k 68.84 72.6 0.9482093663911847
mcd/vat-slip-pass-rough-spec.k 106.91 112.62 0.9492985260166933
benchmarks/storagevar02-overflow-spec.k 55.37 58.31 0.9495798319327731
erc20/ds/transfer-failure-1-b-spec.k 112.34 118.23 0.9501818489385097
kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k 61.02 64.21 0.9503192649120076
kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k 59.23 62.27 0.951180343664686
bihu/forwardToHotWallet-failure-1-spec.k 57.16 60.06 0.9517149517149516
mcd/dsvalue-read-pass-spec.k 72.26 75.92 0.951791359325606
mcd/dai-adduu-fail-rough-spec.k 59.71 62.63 0.9533769758901485
kontrol/test-arithmetictest-test_wdiv_rounding-uint256-uint256-0-spec.k 67.83 71.11 0.9538742792856139
erc20/ds/transfer-failure-1-a-spec.k 84.66 88.71 0.9543456205613798
erc20/hkg/transfer-success-2-spec.k 62.06 65.02 0.9544755459858506
examples/erc20-spec.md 201.76 211.36 0.9545798637395911
mcd/dstoken-approve-fail-rough-spec.k 109.04 114.21 0.9547325102880659
benchmarks/encode-keccak00-spec.k 62.97 65.91 0.9553937187073283
benchmarks/structarg01-spec.k 69.28 72.45 0.9562456866804693
benchmarks/bytes00-spec.k 62.63 65.46 0.9567674915979225
benchmarks/storagevar01-spec.k 54.92 57.31 0.9582969813296108
erc20/hkg/transfer-success-1-spec.k 65.77 68.63 0.9583272621302638
erc20/ds/transferFrom-failure-1-d-spec.k 59.31 61.84 0.9590879689521346
mcd/flopper-cage-pass-spec.k 68.74 71.63 0.959653776350691
examples/solidity-code-spec.md 131.84 137.37 0.9597437577345854
erc20/ds/transferFrom-success-1-spec.k 105.72 110.05 0.9606542480690595
benchmarks/overflow00-overflow-spec.k 53.46 55.61 0.9613378888689085
erc20/ds/totalSupply-spec.k 54.38 56.54 0.9617969579059074
erc20/ds/transfer-success-1-spec.k 86.75 90.19 0.9618582991462469
examples/storage-spec.md 131.24 136.41 0.9620995528187084
erc20/ds/transferFrom-failure-2-b-spec.k 106.14 110.22 0.9629831246597714
mcd/vat-move-diff-rough-spec.k 131.78 136.75 0.9636563071297989
erc20/hkg/allowance-spec.k 55.65 57.73 0.9639702061319938
benchmarks/ecrecover00-siginvalid-spec.k 65.18 67.61 0.9640585712172757
benchmarks/storagevar03-spec.k 56.17 58.22 0.9647887323943662
benchmarks/address00-spec.k 58.16 60.24 0.9654714475431606
benchmarks/staticarray00-spec.k 56.52 58.5 0.9661538461538463
TOTAL 6403.630000000002 6863.59 0.9329855075842237

@geo2a geo2a force-pushed the georgy/smt-retries branch 2 times, most recently from be67972 to e188f40 Compare May 15, 2024 14:52
@geo2a geo2a force-pushed the georgy/smt-retries branch from e188f40 to fe007a4 Compare May 15, 2024 14:58
@geo2a geo2a marked this pull request as ready for review May 17, 2024 09:42
goodlyrottenapple
goodlyrottenapple reviewed May 17, 2024
View reviewed changes
kore/src/Kore/Log/DecidePredicateUnknown.hs
oneLineDoc _ = "DecidePredicateUnknown"
oneLineDoc (DecidePredicateUnknown{message, predicates}) =
Pretty.hsep
[ Pretty.brackets "smt"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

can we put this in the oneLineContextDoc (probably once the json logging is merged)?

jberthold
jberthold reviewed May 19, 2024
View reviewed changes
kore/src/Kore/Rewrite/SMT/Evaluator.hs
Comment on lines +173 to +174
-- do not retry the query on Unknown if the use-case is "soft", i.e. applying simplifications
WarnDecidePredicateUnknown _ _ -> query
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So here is the reason for the speedup?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It appears so, yes.

jberthold
jberthold approved these changes May 20, 2024
View reviewed changes
Copy link
Member

@jberthold jberthold left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

...still not sure about the aggressive scaling.
We have seen people use --smt-retry-limit 10. With a default timeout of 125ms, that means the last retry uses a timeout of ~2 minutes, with --smt-timeout 1000 (again seen in the wild), it will use a timeout of ~16 minutes.
We can merge it and see what it does in the hands of users, though.

@rv-jenkins rv-jenkins merged commit f1d4ba6 into master May 20, 2024
7 checks passed
@rv-jenkins rv-jenkins deleted the georgy/smt-retries branch May 20, 2024 13:03
@geo2a geo2a mentioned this pull request May 21, 2024
Closed
@geo2a geo2a mentioned this pull request May 31, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jberthold jberthold jberthold approved these changes

@goodlyrottenapple goodlyrottenapple goodlyrottenapple approved these changes

@PetarMax PetarMax Awaiting requested review from PetarMax

Assignees
No one assigned
Labels
automerge
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Make SMT query retry logic more agressive
4 participants
@geo2a @jberthold @goodlyrottenapple @rv-jenkins