VC checking in parallel #1247
VC checking in parallel #1247
Conversation
| // For some reasons, the synthesized copy method lacks default parameters... | ||
| val simplifiedVC = (vc.copy()(condition = simplifiedCondition, fid = vc.fid, kind = vc.kind, satisfiability = vc.satisfiability): VC).setPos(vc) |
There was a problem hiding this comment.
Is the copy method default arguments issue still there in the latest Scala versions?
| @@ -350,7 +359,8 @@ trait VerificationChecker { self => | |||
|
|
|||
| object VerificationChecker { | |||
| // number of verified VCs (incremented when a VC is verified) | |||
| var verified: Int = 0 | |||
| // it may be accessed concurrently, and is hence defined as an atomic integer. | |||
| val verified: AtomicInteger = new AtomicInteger(0) | |||
| // total number of VCs (we add to that counter when entering `checkVCs`) | |||
| // this is cumulative across different subprograms (for `SplitCallBack`) | |||
| var total: Int = 0 | |||
There was a problem hiding this comment.
total and startedVerification are probably also concurrent because the SplitCallback runs verification of sub-programs in parallel.
There was a problem hiding this comment.
Ah that's right! I'll make them atomic as well
| // If parallelism is not explicitly enabled, we fallback to eager evaluation | ||
| // (even on a thread pool of a single thread, it seems that the VCs won't necessarily be sequentially processed). | ||
| if (nParallel.exists(_ > 1)) Future(processVC(vc)) |
There was a problem hiding this comment.
Why do we fallback to no parallelism when it's not explicitly enabled? It seems strange to have a different behavior here to the default.
There was a problem hiding this comment.
I have remarked that the default configuration creates a thread pool with the number of logical cores; in my experience, I got better results (less spurious timeouts) by explicitly setting the -Dparallel to the number of physical cores, and only when using a single solver (the portfolio solver seems to run all of its underlying solvers in parallel, causing competition for CPU)
|
Yes, especially on benchmarks where we can get away by using a single solver :) |
mario-bucev
force-pushed
the
parallel-vcs
branch
from
3c54c65 to
8fbe5cd
Compare
|
@samarion : it's marked as approved, but do you want to have a quick look at the final changes? |
The VCs were actually not checked in parallel due to the use of
Future.successful(eager) instead ofFuture.apply(maybe on purpose?).It also enables parallelism back for macOS (as it seems the problem was caused by Z3Prover/z3#1080, which is now addressed)