Multithreading using Bitwuzla (and others)

[cloerkes]

Hi, I would like to enable multithreading in JavaSMT. I have seen the "Multithreading Support" table on the mainpage, but it is not clear to me how to actually tell Java-SMT to use more than one thread. This brings up the following questions:

• Is there a way to configure JavaSMT so that the underlying solver (e.g., Bitwuzla with its -j / --nthreads option) runs with multiple threads?
• Does JavaSMT itself support such solver-specific multithreading options?
• If this is not supported, is it possible (and safe) to “multithread” JavaSMT on the Java side, e.g., by using multiple Java threads with separate solver instances?

Thanks in advance!

[kfriedberger]

Hi @cloerkes

Thanks for your interest in JavaSMT. Three question, three answers:

1. JavaSMT provides a way to set specific solver-dependent options, in most cases as "solver.SOLVERNAME.furtherOptions". Please see https://sosy-lab.github.io/java-smt/ConfigurationOptions.txt for the corresponding format and option name. JavaSMT gives such options directly to the library. If there is an option like NTHREADS, you can specify it as setOption("solver.bitwuzla.furtherOptions", "NTHREADS=4"). We do not test the consequence of any option, as this is beyond our capabilities and depends on the solver and used query.

2. No, JavaSMT itself does not provide any self-implemented option for multi-threaded query solving. We actually provide the other way: synchronous / sequentialized access from multiple threads to a single solver instance. However, that feature is rarely used.

3. In theory, JavaSMT is implemented in a way that allows multiple Java threads, however, it depends on the specific solver's capabilities, see table here:
   -- parallel usage of independent solver contexts (and thus completely independent provers) is supported by most solvers,
   -- parallel usage of independent provers within the same context is an issue for most solvers.
   There is some grey area, where either our documentation is outdated (can happen 😄) or for some solvers parallel usage will work up to a certain degree, e.g., formula solving (the hard part) works, but formula creation (the simple part) does not, or vise versa.

[cloerkes]

Thank you very much for the detailed answer! I will try and play around with the different possibilities.

[daniel-raffler]

* Is there a way to configure JavaSMT so that the underlying solver (e.g., Bitwuzla with its `-j / --nthreads` option) runs with multiple threads?

I think Bitwuzla only supports parallel solving when CryptoMiniSat is used as SAT backend. Here is what it says in the release notes:

Added option -j/--nthreads for configuring multi-threading. Currently,
multi-threading is only supported on the SAT solver level, and only when
CryptoMiniSat is configured as the back end SAT solver. Else, configuring
this option it is a noop.

Currently we only seem to support Cadical as backend. However, it should be possible to include the other SAT backends in a future release