Use parallel prover branch #520
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…everification/kontrol into noah/parallel-integration
rv-jenkins
pushed a commit
to runtimeverification/k
that referenced
this pull request
May 2, 2024
### Additions: - Adds `ParallelProver`, which uses `ProverPool` to handle a `ThreadPoolExecutor` that creates a new prover for each new thread used (based on `KoreServerPool`) - `ParallelProver.parallel_advance_proof` executes a single proof in parallel. - Requires parameter `create_prover: Callable[[], Prover[P, PS, SR]]` to know how to create a fresh `Prover`. - User is responsible for making sure this function produces `Provers` which are independent, i.e. don't refer to the same `KoreClient`, etc. (Although they can/should send requests to the same server). - Reworks `APRProofStep` to no longer contain a proof reference, but instead only immutable data. - Moves the prior loops counting and zero depth bound checking to the `get_steps` stage, because they require whole-KCFG knowledge - Adds an example of how to use parallel proving in `test_all_path_reachability_prove_parallel`. - Adds a test `long-branches` in `imp-simple-spec` intended for profiling parallelization. ### Remaining issues: - ~~Adds an `id()` abstract method to `ProofStep`, to be able to differentiate steps (TODO this might be able to be removed now if we can enforce `ProofStep` being a hashable dataclass)~~ - Saves the `port` as a field in `KoreClient`. This can probably be removed or improved somehow. I'm just using it downstream to get the port being used by a `Prover` in order to generate fresh `Prover`s with the same port, when we don't have prior access to that port, i.e. `KoreServer` was allowed to choose its own port. The port is already accessible through `KoreClient`, but you have to access private vars several layers deep. - ~~Adds `kcfg_semantics` as parameter to `get_steps`, because I haven't been able to find a way to separate the prior loops counting algorithm into two parts, one with `kcfg` and one with `same_loop`, without breaking the prior loop caching. This is not ideal, because `kcfg_explore` probably shouldn't even be in `Prover`, just subclasses of `Prover` that deal with `KCFG`s.~~ - ~~To actually get the benefit of parallelization, you need to set `GHC='-N[threads]'` so the single shared `KoreServer` can start its own threads to deal with requests in parallel. This should probably be automated, but I'm not sure how best to do that.~~ - Perhaps a better design than passing around a `create_prover` function would be to figure out all relevant parameters for doing this and passing them to `ParallelProver()`. - ~~Maybe move parameters from `parallel_advance_proof` to `ParallelProver.__init__()`~~ - The function passing design currently also makes it so that we aren't using the contextmanager features of `KoreServer`, so ~~the KoreServers probably aren't getting closed properly~~. - I would like others to check my work re. thread safety. ### Tested on kevm and kontrol: - runtimeverification/evm-semantics#2400 - runtimeverification/kontrol#520 --------- Co-authored-by: Palina Tolmach <[email protected]>
Closed
tothtamas28
approved these changes
May 10, 2024
…Server directly to more easily get the port
ehildenb
approved these changes
May 10, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Use parallel prover branch evm-semantics#2400
Parallel proof exploration k#4256
Enables single-proof parallelism on foundry_prove, which makes
parallel_advance_proofthe default on the kontrol test suite and thekontrol proveCLI.To use, include the
--max-frontier-parallel Noption withkontrol proveto use up to N worker threads to advance independent proof branches in parallel.To streamline the creation of a
create_kcfg_explorefunction to pass to KEVM'srun_prover, useskore_serverin_run_cfg_groupinstead oflegacy_explore(so we can get access to the server's port instead of having to copy the port of the client buried deep within theKCFGExplore.To clean up the logic of choosing between starting a new KoreServer and using the port of a KoreServer that was already started elsewhere, introduces
OptionalKoreServerand 2 subclasses for each case that each yield the server port and handle closing the underlying server (if applicable).