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

WIP: Check valid jump dests on demand #2112

Closed
wants to merge 27 commits into from

Conversation

RaoulSchaffranek
Copy link
Member

Don't merge. I'm just profiling.

@palinatolmach palinatolmach force-pushed the raoul/is-valid-jump-dest branch from 4366bef to 171ff97 Compare May 17, 2024 09:24
@palinatolmach
Copy link
Contributor

I've brought the PR up to date since constructors with symbolic parameters are needed for the engagement: runtimeverification/kontrol#451.

Some considerations regarding JUMPDEST calculation from a discussion with @ehildenb in October:

  • precomputing valid jump dests ahead of time was actually done to speed up the verification — the corresponding claims are fully concrete and should be sent to the concrete LLVM backend which is supposed to be fast; so two things to check here are 1) if we're using the booster, and 2) if this ahead-of-time validity checking is indeed using LLVM backend and, if not, why
  • not pre-computing JUMPDESTs might slow the execution down if there’s a lot of loop unrolling, so it’d be good to include some loop-containing code in profiling
  • conformance tests can also help measure the potential speedup and determine if we’re indeed executing the relevant parts concretely
  • one reason why the execution might take a long time is that a set of valid JUMPDESTs is a large tree (and the bigger the bytecode, the larger the tree gets, probably); so, in the Haskell Backend, every simplification includes walking this large tree, and one of the potential optimizations is perhaps saving some relevant information for the backend instead of having it walk through the tree every time

@ehildenb
Copy link
Member

Subsumed by: #2471

Re-open if still relevant.

@ehildenb ehildenb closed this Jun 12, 2024
@ehildenb ehildenb deleted the raoul/is-valid-jump-dest branch June 12, 2024 15:53
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.

5 participants