Make performance improving options default #1963

palinatolmach · 2023-07-24T11:05:26Z

This PR fixes #1958, which is aimed to improve the default observable performance of KEVM by making the following set of flags/optimizations the default:

Setting default --max-depth to 25000 (instead of 1000)
Using --no-break-on-calls by default
Using --use-booster by default
Using infinite gas by default; implemented based on Allow setting infinite gas in foundry test #1524. With regards to the conversation in Use infinite gas by default #1520, this PR also adds a cheatcode setGas(uint256) that sets gas to the provided value; the PR also adds a test for setGas.
~~Using --no-implication-every-block by default~~
(requires further investigation, as using it by default breaks 79182a0149fceb6cd86e2ca420e4afb4032fdb144618f53b819e3edbfa47a1bb proof in nix build --extra-experimental-features 'nix-command flakes' --print-build-logs .#kevm-test)

In this configuration, the execution of kevm foundry-prove on the MiniVat test takes ~170s instead of ~250s as before.

kevm-pyk/src/kevm_pyk/foundry.py

include/kframework/foundry.md

kevm-pyk/src/kevm_pyk/foundry.py

ehildenb · 2023-07-26T16:11:21Z

I still prefer unbounded loops by default, following the principle taht @d-xo mentioned of "be as sound as possible, and let users make it simpler if wanted".

But not having that, I would also suggest having a loud warning on passed proofs if any nodes are passed because they are bounded, something like "Proof passed, but NNN nodes were loop-depth bounded at MMM iterations, re-run with --unbounded-loops for full verification."

include/kframework/foundry.md

palinatolmach · 2023-08-01T12:32:47Z

@anvacaru @tothtamas28 @ehildenb Can I ask for your opinion on making --with-llvm-backend default in foundry-kompile in dde26c8? I realized that with the booster enabled by default, we should also generate the llvm library (otherwise everyone would have to debug the no interpreter.dylib error), but I didn't want to enable it for kompile in general, beyond the Foundry integration — at least, until we migrate all proofs (including normal Haskell, not just Foundry ones) to use booster, as @ehildenb suggested.

palinatolmach · 2023-08-04T11:25:13Z

Update on using --with-llvm-library in kevm foundry-kompile by default (and not having it on by default for kevm kompile), as implemented in a8b0126:

The option --with-llvm-library is inherited as part of kompile_args in pyk, which we don't want to modify;
Introducing foundry_kompile.set_defaults(llvm_library=True) to re-set the default value foundry_kompile options overrides the default value for all subparsers (i.e., for kevm kompile, which is then also ran with --with-llvm-library by default)
As a way around this, I added separate --with-llvm-library and --no-llvm-library options to both kevm_kompile_args and foundry_kompile_args; the first overrides the --with-llvm-library option inherited from the parent kompile_args: a8b0126. For that, I added conflict_handler='resolve' argument to the initialization of both subparsers.
(Strangely enough, adding an overriding --with-llvm-library option and conflict_handler='resolve' to just one subparser, foundry_kompile_args, messes up this option in kevm_kompile_args).

github-actions · 2023-08-15T16:36:13Z

Workflow Telemetry - Test PR / Build and Test KEVM Foundry proofs

Workflow telemetry for commit 86d56c8824aa19cf0b1f7643158401801ef83f83
You can access workflow job details here

Step Trace

gantt
	title Build and Test KEVM Foundry proofs
	dateFormat x
	axisFormat %H:%M:%S
	Set up job : milestone, 1692116333000, 1692116341000
	Set up runner : 1692116341000, 1692116342000
	Workflow Telemetry : 1692116342000, 1692116342000
	Check out code : 1692116343000, 1692116358000
	Set up Docker : 1692116358000, 1692116368000
	Build kevm-pyk : 1692116368000, 1692116386000
	Build Foundry : 1692116387000, 1692116451000
	Foundry Prove : crit, 1692116451000, 1692117368000
	Tear down Docker : 1692117368000, 1692117369000
	Post Check out code : 1692117369000, 1692117369000

CPU Metrics

Memory Metrics

IO Metrics

	Read	Write
Network I/O
Disk I/O

github-actions · 2023-08-15T19:12:37Z

Workflow Telemetry - Test PR / Build and Test KEVM Foundry proofs (booster)

Workflow telemetry for commit 86d56c8824aa19cf0b1f7643158401801ef83f83
You can access workflow job details here

Step Trace

gantt
	title Build and Test KEVM Foundry proofs (booster)
	dateFormat x
	axisFormat %H:%M:%S
	Set up job : milestone, 1692115938000, 1692115941000
	Set up runner : 1692115941000, 1692115942000
	Workflow Telemetry : 1692115943000, 1692115943000
	Check out code : 1692115943000, 1692115951000
	Set up Docker : 1692115951000, 1692116343000
	Build kevm-pyk : 1692116344000, 1692116363000
	Build blockchain-k-plugin-deps : 1692116363000, 1692116363000
	Build Foundry : 1692116363000, 1692116399000
	Foundry Prove : 1692116399000, 1692126748000
	Tear down Docker : 1692126750000, 1692126750000
	Post Check out code : 1692126751000, 1692126751000

CPU Metrics

Memory Metrics

IO Metrics

	Read	Write
Network I/O
Disk I/O

github-actions · 2023-08-15T23:14:02Z

Workflow Telemetry - Test PR / Build and Test KEVM Foundry proofs

Workflow telemetry for commit 86d56c8824aa19cf0b1f7643158401801ef83f83
You can access workflow job details here

Step Trace

gantt
	title Build and Test KEVM Foundry proofs
	dateFormat x
	axisFormat %H:%M:%S
	Set up job : milestone, 1692132227000, 1692132235000
	Set up runner : 1692132235000, 1692132236000
	Workflow Telemetry : 1692132236000, 1692132236000
	Check out code : 1692132237000, 1692132244000
	Set up Docker : 1692132244000, 1692132277000
	Build kevm-pyk : 1692132278000, 1692132303000
	Build Foundry : 1692132303000, 1692132330000
	Foundry Prove : 1692132330000, 1692141236000
	Tear down Docker : 1692141237000, 1692141237000
	Post Check out code : 1692141237000, 1692141237000

CPU Metrics

Memory Metrics

IO Metrics

	Read	Write
Network I/O
Disk I/O

github-actions · 2023-08-16T02:59:42Z

Workflow Telemetry - Test PR / Build and Test KEVM Foundry proofs (booster)

Workflow telemetry for commit c394094dcd48cc4b0c6746e86833174592d33e8b
You can access workflow job details here

Step Trace

gantt
	title Build and Test KEVM Foundry proofs (booster)
	dateFormat x
	axisFormat %H:%M:%S
	Set up job : milestone, 1692154211000, 1692154219000
	Set up runner : 1692154219000, 1692154220000
	Workflow Telemetry : 1692154221000, 1692154221000
	Check out code : 1692154221000, 1692154236000
	Set up Docker : 1692154236000, 1692154280000
	Build kevm-pyk : 1692154280000, 1692154303000
	Build blockchain-k-plugin-deps : 1692154304000, 1692154600000
	Build Foundry : 1692154601000, 1692154645000
	Foundry Prove : 1692154645000, 1692154776000
	Tear down Docker : 1692154777000, 1692154777000
	Post Check out code : 1692154777000, 1692154777000

CPU Metrics

Memory Metrics

IO Metrics

	Read	Write
Network I/O
Disk I/O

github-actions · 2023-08-16T02:59:42Z

Workflow Telemetry - Test PR / Build and Test KEVM Foundry proofs

Workflow telemetry for commit c394094dcd48cc4b0c6746e86833174592d33e8b
You can access workflow job details here

Step Trace

gantt
	title Build and Test KEVM Foundry proofs
	dateFormat x
	axisFormat %H:%M:%S
	Set up job : milestone, 1692154212000, 1692154215000
	Set up runner : 1692154215000, 1692154216000
	Workflow Telemetry : 1692154216000, 1692154216000
	Check out code : 1692154216000, 1692154226000
	Set up Docker : 1692154227000, 1692154413000
	Build kevm-pyk : 1692154414000, 1692154433000
	Build Foundry : 1692154433000, 1692154479000
	Foundry Prove : 1692154479000, 1692154776000
	Tear down Docker : 1692154776000, 1692154777000
	Post Check out code : 1692154777000, 1692154777000

CPU Metrics

Memory Metrics

IO Metrics

	Read	Write
Network I/O
Disk I/O

github-actions · 2023-08-16T03:29:44Z

Workflow Telemetry - Test PR / Build and Test KEVM Foundry proofs

Workflow telemetry for commit 33f83d19df41545e1499453c0b9e1776a5517664
You can access workflow job details here

Step Trace

gantt
	title Build and Test KEVM Foundry proofs
	dateFormat x
	axisFormat %H:%M:%S
	Set up job : milestone, 1692154899000, 1692154904000
	Set up runner : 1692154904000, 1692154905000
	Workflow Telemetry : 1692154905000, 1692154905000
	Check out code : 1692154905000, 1692154916000
	Set up Docker : 1692154916000, 1692155125000
	Build kevm-pyk : 1692155125000, 1692155145000
	Build Foundry : 1692155145000, 1692155192000
	Foundry Prove : crit, 1692155192000, 1692156579000
	Tear down Docker : 1692156580000, 1692156580000
	Post Check out code : 1692156580000, 1692156580000

CPU Metrics

Memory Metrics

IO Metrics

	Read	Write
Network I/O
Disk I/O

github-actions · 2023-08-16T05:31:55Z

Workflow Telemetry - Test PR / Build and Test KEVM Foundry proofs (booster)

Workflow telemetry for commit 33f83d19df41545e1499453c0b9e1776a5517664
You can access workflow job details here

Step Trace

gantt
	title Build and Test KEVM Foundry proofs (booster)
	dateFormat x
	axisFormat %H:%M:%S
	Set up job : milestone, 1692154900000, 1692154904000
	Set up runner : 1692154904000, 1692154905000
	Workflow Telemetry : 1692154905000, 1692154905000
	Check out code : 1692154905000, 1692154914000
	Set up Docker : 1692154914000, 1692155313000
	Build kevm-pyk : 1692155314000, 1692155331000
	Build blockchain-k-plugin-deps : 1692155332000, 1692155607000
	Build Foundry : 1692155607000, 1692155653000
	Foundry Prove : 1692155653000, 1692163909000
	Tear down Docker : 1692163909000, 1692163909000
	Post Check out code : 1692163910000, 1692163910000

CPU Metrics

Memory Metrics

IO Metrics

	Read	Write
Network I/O
Disk I/O

palinatolmach · 2023-08-23T07:46:28Z

Closing this PR since it introduces performance issues and doesn't pass CI. I'll split the changes suggested here into several smaller PRs.

palinatolmach force-pushed the optimized-defaults branch from e394d83 to 5291cd3 Compare July 24, 2023 19:03

palinatolmach requested review from ehildenb and tothtamas28 July 24, 2023 19:04

palinatolmach marked this pull request as ready for review July 24, 2023 19:25

palinatolmach self-assigned this Jul 24, 2023

anvacaru reviewed Jul 25, 2023

View reviewed changes

kevm-pyk/src/kevm_pyk/foundry.py Outdated Show resolved Hide resolved

anvacaru reviewed Jul 25, 2023

View reviewed changes

include/kframework/foundry.md Outdated Show resolved Hide resolved

palinatolmach force-pushed the optimized-defaults branch 2 times, most recently from b433541 to f2c6005 Compare July 26, 2023 07:20

tothtamas28 reviewed Jul 26, 2023

View reviewed changes

kevm-pyk/src/kevm_pyk/foundry.py Outdated Show resolved Hide resolved

palinatolmach force-pushed the optimized-defaults branch from 8c39eb9 to 9aeb0ca Compare July 26, 2023 11:57

tothtamas28 reviewed Jul 26, 2023

View reviewed changes

kevm-pyk/src/kevm_pyk/foundry.py Outdated Show resolved Hide resolved

palinatolmach force-pushed the optimized-defaults branch from 38239de to a78900e Compare July 26, 2023 13:22

ehildenb approved these changes Jul 26, 2023

View reviewed changes

ehildenb reviewed Jul 26, 2023

View reviewed changes

include/kframework/foundry.md Show resolved Hide resolved

palinatolmach mentioned this pull request Jul 26, 2023

Show warning on proofs with loop-depth bounded nodes #1973

Open

ehildenb added the automerge label Jul 26, 2023

palinatolmach force-pushed the optimized-defaults branch 3 times, most recently from 2030505 to 5005a30 Compare July 30, 2023 13:17

palinatolmach force-pushed the optimized-defaults branch 5 times, most recently from 5aa6d26 to dde26c8 Compare August 3, 2023 12:17

palinatolmach requested a review from tothtamas28 August 3, 2023 12:23

palinatolmach force-pushed the optimized-defaults branch from dde26c8 to a8b0126 Compare August 4, 2023 09:57

devops and others added 10 commits August 14, 2023 05:30

Set Version: 1.0.257

8dffbce

Increase max_iterations in resume_proof test

b958e59

Merge branch 'master' into optimized-defaults

6f3d5ac

Set Version: 1.0.258

6966ad3

Merge branch 'master' into optimized-defaults

ee074ef

Set Version: 1.0.259

e87d7e5

Merge branch 'master' into optimized-defaults

a7d1b8f

Set Version: 1.0.260

119c8a1

Merge branch 'master' into optimized-defaults

46951da

Set Version: 1.0.261

0c6bbe5

palinatolmach removed the automerge label Aug 15, 2023

Add telemetry to failing Foundry tests

86d56c8

palinatolmach force-pushed the optimized-defaults branch from d5e3587 to 86d56c8 Compare August 15, 2023 16:10

palinatolmach and others added 3 commits August 16, 2023 10:48

Merge branch 'master' into optimized-defaults

cfe6d66

Set Version: 1.0.262

c394094

Set default max-depth to 25000

33f83d1

palinatolmach and others added 4 commits August 20, 2023 17:15

Merge branch 'master' into optimized-defaults

0ab2d1a

Set Version: 1.0.268

f765090

Remove telemetry, rollback the timeout change

b9e271f

Experiment: revert max-depth ,no-break-on-call

17e2a31

palinatolmach closed this Aug 23, 2023

palinatolmach mentioned this pull request Aug 23, 2023

Make performance improving options default #1958

Closed

4 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Make performance improving options default #1963

Make performance improving options default #1963

palinatolmach commented Jul 24, 2023 •

edited

Loading

ehildenb commented Jul 26, 2023

palinatolmach commented Aug 1, 2023 •

edited

Loading

palinatolmach commented Aug 4, 2023 •

edited

Loading

github-actions bot commented Aug 15, 2023

github-actions bot commented Aug 15, 2023

github-actions bot commented Aug 15, 2023

github-actions bot commented Aug 16, 2023

github-actions bot commented Aug 16, 2023

github-actions bot commented Aug 16, 2023

github-actions bot commented Aug 16, 2023

palinatolmach commented Aug 23, 2023

Make performance improving options default #1963

Make performance improving options default #1963

Conversation

palinatolmach commented Jul 24, 2023 • edited Loading

ehildenb commented Jul 26, 2023

palinatolmach commented Aug 1, 2023 • edited Loading

palinatolmach commented Aug 4, 2023 • edited Loading

github-actions bot commented Aug 15, 2023

Workflow Telemetry - Test PR / Build and Test KEVM Foundry proofs

Step Trace

CPU Metrics

Memory Metrics

IO Metrics

github-actions bot commented Aug 15, 2023

Workflow Telemetry - Test PR / Build and Test KEVM Foundry proofs (booster)

Step Trace

CPU Metrics

Memory Metrics

IO Metrics

github-actions bot commented Aug 15, 2023

Workflow Telemetry - Test PR / Build and Test KEVM Foundry proofs

Step Trace

CPU Metrics

Memory Metrics

IO Metrics

github-actions bot commented Aug 16, 2023

Workflow Telemetry - Test PR / Build and Test KEVM Foundry proofs (booster)

Step Trace

CPU Metrics

Memory Metrics

IO Metrics

github-actions bot commented Aug 16, 2023

Workflow Telemetry - Test PR / Build and Test KEVM Foundry proofs

Step Trace

CPU Metrics

Memory Metrics

IO Metrics

github-actions bot commented Aug 16, 2023

Workflow Telemetry - Test PR / Build and Test KEVM Foundry proofs

Step Trace

CPU Metrics

Memory Metrics

IO Metrics

github-actions bot commented Aug 16, 2023

Workflow Telemetry - Test PR / Build and Test KEVM Foundry proofs (booster)

Step Trace

CPU Metrics

Memory Metrics

IO Metrics

palinatolmach commented Aug 23, 2023

palinatolmach commented Jul 24, 2023 •

edited

Loading

palinatolmach commented Aug 1, 2023 •

edited

Loading

palinatolmach commented Aug 4, 2023 •

edited

Loading