Support for concurrent solvers

[dylanmc]

Since we support many solvers (thanks to SBV), and each has its sweet spot of the kinds of problems it can solve, we should be able to support the concurrent execution of multiple solvers.

The point of this feature is to support for following use-cases:

1. accept the answer of the fastest solver and kill all others, to make the tool feel more efficient,
2. wait for an answer from all solvers to double-check (or triple- etc.) the result, and possibly
3. use an appropriate solver for a given verification (certain solvers at better at some problems than others), and finally
4. use a fast solver for the verification and a slower solver (or a second run of the same solver) to emit a certificate.

The first two "seem easy", the latter might be interesting research projects.

[LeventErkok]

This is a great idea. One that I pondered and was inclined to implement several times, but never got around to. May I humbly suggest you guys implement this for SBV directly, and then inherit backwards.

Note that the "Why" platform already has a similar capability. (http://why3.lri.fr/)

Point 3: Unlikely one can decide which will be better ahead of time, as most differences will be very solver specific, including the choice of the random-seed.

Point 4: The word "certificate" has a certain meaning in these circles, and it's better not to conflate the terms here. Some solvers (z3 in particular) can generate proof traces which can (in theory) be independently checked in a separate theorem prover (say Isabelle). There's some work on this already: http://research.microsoft.com/en-us/people/nbjorner/iwil08.pdf

But this is really a whole can of worms, and maybe it's more a job for the SAW suite of tools, potentially.

[kiniry]

I think that this is straightforward enough to aim for 2.1, given I wrote the same thing for another verification system years ago and it is supported by the likes of Why3. @brianhuffman, push back if that's not the case.

[LeventErkok]

I've just added a new set of API to SBV that should simplify this: https://github.com/LeventErkok/sbv/commit/72c98c6a4b287985d3adf83a389712bc4f32c95c

Added are:

• proveWithAny/proveWithAll
• satWithAny/satWithAll
• allSatWithAny/allSatWithAll
• sbvAvailableSolvers

The Any versions allow running a bunch of solvers, taking the result of the first one, and killing the others. The All versions return all the results from all the solvers, as they are produced. The final function sbvAvailableSolvers returns the list of solvers that are available on a users system.

With these in tow, implementing concurrent solver calls should be easy. The issue is of course how you present it back to the user in a meaningful way; or provide some sort of feedback to the user which solver has been running, how long, etc. More like how why3 handled this issue back in the day, with a snippy GUI and such. That would be an overkill for Cryptol, but the user should at least get an indication as to which solver finished first, etc.

I have tested these to a fair degree; but asynchronous programming is notoriously tricky to get right. If you play around with them and find any issues, file a ticket! Or, better yet; fix it and push to SBV.

[atomb]

This is now partially implemented (commit 92e7f1b783932b3cf73807ca899f98dda1fe2a96). The prover any now runs all available solvers, returning the result from the first to finish (using satWithAny and proveWithAny).

I've been considering implementing another prover, all, which uses satWithAll and proveWithAll behind the scenes. The key design question: should it 1) return all results separately, or 2) compare them all to make sure they agree and then either a) return that single result or b) give an error message if they're different.

Points (3) and (4) from the original issue comment are trickier. We don't currently have any heuristics for deciding what solver might work best in a particular case (thought I expect there exist some heuristics that might frequently work well).

[LeventErkok]

Cool.. One gotcha though: If you start using a solver that did nothing but just reported "Unknown" it'd always win the proveAny race, and thus would be hardly useful. Maybe the right thing to do is to proveAll, and walk through the results and return the first one that's not an error/unknown result.

I don't think this is a major issue, but something to keep in mind.

[atomb]

Perhaps it would make sense to modify the behavior of proveAny so that it discarded early Unknown (and error) results, and only returned one of those two values if all provers either returned Unknown or failed. Because it's still nice to get the result from the fastest one when it is definitive, and kill off the rest.

[LeventErkok]

@atomb: Sure, maybe proveAny should take a "predicate" to see what results are acceptable.

For Cryptol, however, I don't think this'll be necessary: No Cryptol generated SBV proof goal will have alternating quantifiers, and also it'll always be restricted to the QF_BV logic. So, other than "timeout" related issues, solvers should always return SAT/UNSAT for those queries.

If you hit an "UNKNOWN" case, I'd like to see that!

[atomb]

Point 1 from the bullet list above is done (though handling results other than SAT and UNSAT as in the above comments isn't yet in place), so I'm going to close it. The other three bullets are part of other tickets (#118, #119, #120).