[DRAFT] Add benchmarking with Solidity examples

[siraben]

Description

This PR adds various benchmarking tests to hevm so that we can get an idea of how well we perform over time. For example, we can process the CSV to see how time spent in each benchmark changed after the mutable memory PR #318.

Let me know what changes I need to make, I made some things on the fly based on other parts of the codebase I read, so it may not be the most idiomatic for hevm.

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[msooseth]

Hi,

Thanks! I have two thoughts/questions:

• What is "(ps)(ps)"? Sorry, this is not self-explanatory to me 😢
• I think n is the number of iterations/calls/etc, and in these benchmarks we don't call Expr. simplify or the SMT solver. If we do things right in HEVM, the vast majority of the time should be spent in the SMT solver (and some in formula simplification). Is the metric generated by this tool trying to check what time is being spent in expression generation as opposed to spending it on e.g. Expr.simplify and the SMT solver?

In general, loops are not considered very good practice in Ethereum smart contracts, if I understand correctly. Do you think such a benchmark suite could possibly drive us towards optimizing for some cases that are not considered good practice? Or do you think improving these would have a wider positive effect? (i.e. well beyond loops) I am not sure, so I'm curious.

We have lately been putting some effort into this benchmarking suite: https://github.com/eth-sc-comp/benchmarks It's for comparing performance of different symbolic execution frameworks. It's far from complete and has only a limited number of examples. Perhaps some of your examples could be added, as a so-called "synthetic benchmark", i.e. not a real-world use-case? Note that this is an end-to-end performance test suite, i.e. may actually not be good at what you are trying to achieve, i.e. a more nuanced, focussed understanding of performance characteristics for specific uses-cases.

What do you think?

[siraben]

• What is "(ps)(ps)"? Sorry, this is not self-explanatory to me 😢

Ah this is a typo because the graphs are automatically generated. I'll fix this in the script I have locally!

• I think n is the number of iterations/calls/etc, and in these benchmarks we don't call Expr. simplify or the SMT solver. If we do things right in HEVM, the vast majority of the time should be spent in the SMT solver (and some in formula simplification). Is the metric generated by this tool trying to check what time is being spent in expression generation as opposed to spending it on e.g. Expr.simplify and the SMT solver?

Yes, n is the number of iterations or calls and so on. The metric generated by this tool is the time it takes to run the bytecode in the VM. So this does not measure anything related to SMT solving or Expr simplification

In general, loops are not considered very good practice in Ethereum smart contracts, if I understand correctly. Do you think such a benchmark suite could possibly drive us towards optimizing for some cases that are not considered good practice? Or do you think improving these would have a wider positive effect? (i.e. well beyond loops) I am not sure, so I'm curious.

Yes, we are never going to encounter loops this extensive in smart contracts. The purpose of such a benchmark is to obtain reliable information about long term behavior of HEVM. This can impact things like Echidna where the running of the VM takes up a lot of time.

cc @arcz for further discussion/review.

[d-xo]

Apologies for the delay. This looks awesome. The only thing I'm not sure about is why this needs to be a separate benchmarks binary instead of being included in the existing bench.hs?

[siraben]

I wasn't sure if you still wanted to use bench.hs, this program runs a more specialized suite of tests and is intended to be separate, but if you wish it could replace bench.hs.

[d-xo]

Is there any reason we can't keep the existing benchmarks in bench.hs and extend it with the ones in bench-perf.hs?

[msooseth]

Hi @siraben ,

Unfortunately this PR getting a bit stale :( I'm afraid it'll get very hard to merge eventually. Could you maybe answer @d-xo 's question so we can try to move this forward a bit? :) I wanna make sure we can make a decision on this soon so we don't have too many stale PRs around :) Thanks a lot in advance,

Mate

[siraben]

Hi all, yes I plan to continue working on this to get it merged. @d-xo I think it could be a separate benchmark suite than the existing one, since that one seems to be testing solver parallelization rather than raw VM performance as this one tries to do.