- 
                Notifications
    You must be signed in to change notification settings 
- Fork 2
Parallel prover implementation for APRProofs #727
base: master
Are you sure you want to change the base?
Conversation
…fication/pyk into noah/parallel-prover
…fication/pyk into noah/parallel-prover
…r, and strengthen type signatures
…erification/pyk into noah/apr-proof-parallel
|  | ||
| @abstractmethod | ||
| def exec(self) -> U: | ||
| def exec(self, data: D) -> U: | 
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
My understanding is that data is fixed for a given run of prove_parallel. What's the advantage of providing data as an argument to exec and not in __init__ of the Prover implementation?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, it is now fixed, but I'm still using at as a way to only pass in large objects to the worker threads once at the beginning. With the way you suggest is there a different way exec could get access to the data?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Prover instantiates ProofStep, so if Prover has access to data, then it can also pass it to ProofStep during instantiation. The exec method then reads data from its instance.
…erification/pyk into noah/apr-proof-parallel
…erification/pyk into noah/apr-proof-parallel
ParallelAPRProverandParallelAPRBMCProver, which implementParallelProverinterface for APR and APRBMC proofsProcessData, implemented byAPRProcessData, for passing in data into a process at the beginning and sharing data within the same process, but between different tasksprove_parallelAPRProver,APRProof, andAPRProcessDataBlocked on runtimeverification/hs-backend-booster#383Blocked on runtimeverification/evm-semantics#2272