CN: Race solvers

[dc-mak]

There are a few axes on which to race:

• Incremental vs non-incremental solver
• CVC5 vs Z3
• (Potentially) derived constraints vs minimal constraints

This seems like a good fit: https://github.com/ocaml-multicore/eio?tab=readme-ov-file#racing, although it would commit us to OCaml 5 (but avoid wrapping all the solver code in a monad).

Note: racing an incremental solver with other ones will naturally bring up some concurrency query-to-query, because the process will be the same, so cancelling queries may need to lock and clean up appropriately.

There is also an inherent racy-ness that the solver might return an answer after cancel is sent, in which case the incremental solver will be accidentally closed would need to be restarted with the correct context before the next query.

[bcpierce00]

Is it bad to commit to OCaml 5 at this point?

[PeterSewell]

I'd be happy committing to OCaml 5 - it's surely ok intra-VERSE. Getting industry folk to install any OCaml can be problematic, but I don't know any reason why 5 should be worse than 4.n ?

…

On Tue, 17 Dec 2024 at 15:56, Benjamin Pierce ***@***.***> wrote: Is it bad to commit to OCaml 5 at this point? — Reply to this email directly, view it on GitHub <#770 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFMZZUMR4FFXRVCWAIQFDT2GBCSHAVCNFSM6AAAAABTYPCMB6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDKNBYHA2DINRUGE> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[cp526]

Some linux distributions will have OCaml versions older than that pre-installed, so dependency on a newer OCaml will require an extra installation step for those users, but I don't think that should stop us if there's a good reason (such as the above).

[podhrmic]

FWIW I doubt that any industry partners will be installing OCaml natively, most likely mean of deployment seem to be a Docker image (see GaloisInc/VERSE-Toolchain#48). So as long as it can be installed and packaged in a Docker image, the specific version does not matter.

[yav]

One other interesting consideration is that it is unclear how useful the incremental solvers are in a setup where we race solvers, because the slower solvers would presumably be killed, and have to start over anyway, so they wouldn't really benefit from preserving their internal state.

[PeterSewell]

while we're developing, one might well want to try running both to completion in any case, to gather meaningful statistics - but report the first quickly back to the user

…

On Tue, 7 Jan 2025 at 18:38, Iavor S. Diatchki ***@***.***> wrote: One other interesting consideration is that it is unclear how useful the incremental solvers are in a setup where we race solvers, because the slower solvers would presumably be killed, and have to start over anyway, so they wouldn't really benefit from preserving their internal state. — Reply to this email directly, view it on GitHub <#770 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFMZZU3CYUG4YQIOG7DHFL2JQNLHAVCNFSM6AAAAABTYPCMB6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDKNZVHE4DGNBWGQ> . You are receiving this because you commented.Message ID: ***@***.***>

[cp526]

RE incremental solvers: we previously had a setup where we ran an incremental solver with quick timeout (e.g. 0.2s), followed by a non-incremental solver on timeout. The timeout for the incremental solver was a Z3 configuration option rather than an external "kill", meaning we didn't have the problem @yav describes.

I think we'll want to try a setup that

• has a single incremental solver (either z3 or cvc5, as per command line option), with small timeout, and
• when that times out, runs non-incremental z3 and cvc5 concurrently.

In James's graphs ( https://rems-project.github.io/cerberus/dev/bench/ ) one can see that the different solvers compare quite differently on different C code examples (let alone individual solver queries, presumably). So being able to race cvc5 and z3 seems like a low-hanging fruit for getting some (much needed) performance improvements.