Efficient solver initialization by cloning

[fpoli]

@utaal mentioned me that the Z3 API has a way to clone a solver. The method seems to be Solver::translate. For the Silicon parallelization it might be more efficient to clone a solver when branching, instead of initializing a new solver from scratch (loading the prelude and all the assumptions coming from the path verified until that point). I'm not sure how easy/hard this is in the current architecture of Silicon.

[marcoeilers]

I had looked at this and thought it didn't do what we need in a concurrent setting, but I'll have another look.

[fpoli]

The thread-safety conditions are discussed in this issue and in this commit. I hope they are still up-to-date.

[marcoeilers]

The problem is basically this:
We'd need to clone the solver before executing the then or else branch. However, at that point we don't know if we're going to execute the else branch in parallel (that depends on the availability of a free worker), so we'd likely clone many solvers that then never get used, which would cause some amount of overhead.

So we'll have to just try that out to see if it's worth it. I'll put it on my to do list.

[jcp19]

If the overhead is actually high, we could try to use some sort of copy-on-write mechanism

[fpoli]

We'd need to clone the solver before executing the then or else branch.

If the decision to parallelize happens after the branching point, it might be that cloning the solver and popping a few states (to go back to the state before the branch) is still faster than re-loading a solver from scratch.

[marcoeilers]

We'd need to clone the solver before executing the then or else branch.

If the decision to parallelize happens after the branching point, it might be that cloning the solver and popping a few states (to go back to the state before the branch) is still faster than re-loading a solver from scratch.

If I understand you correctly, you're saying we could clone the solver later, while the then-branch is potentially already being verified (and then pop some asserts to remove whatever we added while verifying the then-branch)? That would mean accessing the solver from two threads at the same time; I'm pretty sure we'd get segfaults left and right.

[fpoli]

If I understand you correctly, you're saying we could clone the solver later, while the then-branch is potentially already being verified (and then pop some asserts to remove whatever we added while verifying the then-branch)? That would mean accessing the solver from two threads at the same time; I'm pretty sure we'd get segfaults left and right.

No, sorry, it was some confusion on my side regarding how Silicon internally works. I wanted to suggest that the solver can be cloned when queueing a verification task, but I now understand that because of work-stealing when queueing it's not known wether the task will be executed in parallel or not.

[marcoeilers]

Right.

It might still be worth it of course, I'll definitely try it.

[marcoeilers]

I tried it.

Apparently, cloning solvers is not supported when using push/pop (I get the error translation of contexts is only supported at base level). See Z3Prover/z3#556.

[marcoeilers]

Another update: I made a branch with a Silicon version that doesn't use push/pop at all (meilers_solver_clone_pure_sc) when assertionMode sc is chosen. There the solver cloning works, but overall it's much slower than what we currently have.