CVC4 and Multiple Threads?

[evmaus]

Hey:

For our use case, we wind up needing to use multiple copies of an SMT solver in order to hit the throughput that we want. Is this scenario supported by CVC4? We're creating an SMTEngine per thread right now (and not sharing any data between them)--is that the best way to go about this?

I ask because we're running into an issue with CVC4 where there's a potential data race in smtEngine::setDefaults() uncovered by Thread Sanitizer (TSAN).

The relevant stack trace is: WARNING: ThreadSanitizer: data race (pid=2750) Write of size 4 at 0x7fb9095a2760 by thread T1735:

0 CVC4::SmtEngine::setDefaults() third_party/cvc4/src/smt/smt_engine.cpp

CVC4/CVC4#1 CVC4::SmtEngine::finishInit() third_party/cvc4/src/smt/smt_engine.cpp:939:3 
CVC4/CVC4#2 CVC4::SmtEngine::finalOptionsAreSet() third_party/cvc4/src/smt/smt_engine.cpp:1010:3 
CVC4/CVC4#3 CVC4::SmtEngine::push() third_party/cvc4/src/smt/smt_engine.cpp:5301:3 

This is using a copy of CVC4 from a few weeks ago.

At first glance, the data race looks /potentially/ harmless (a default option getting set twice), but could have some odd behavior if multiple SMT engines have slightly different options set.

Thanks, Everett Maus

[4tXJ7f]

Thank you for your interest in CVC4, @evmaus. If you are not sharing any data between the different instances, it should be safe to create one ExprManager and one SmtEngine per thread. The ExprManager cannot be shared between threads because it is not thread safe (which is likely why you get this warning because the options are attached to the ExprManager). If you would like to use the same expressions in multiple solvers, you can use Expr::exportTo() to export an expression to a different ExprManager. We are working towards a better API that hopefully makes your use case a bit easier but it will take us a while to get there.

Please let us know if you encounter other issues.

[evmaus]

From checking our code, we should be creating an ExprManager and SmtEngine per thread.

Am I reading setDefaults() incorrectly? It seems to modify static global variables in the options:: namespace; e.g. the structs declared in src/options/bv_options.cpp.

[4tXJ7f]

Sorry, about the late reply. I think that you are correct. We should make sure that we don't store options in global variables. I will take a look.

[evmaus]

Hey all!

So we wound up continuing to have issues around the threading for the various things in the options namespace with our version of CVC4.

In order to fix that & to ensure the great TSAN deities were happy (and to ensure we didn't have any issues caused by them), we wound up moving them to a thread_local scope.

We'd be happy to contribute a fix to the code generation that creates those options to ensure they're generated in a thread_local way for all users, if that's something you all would be interested in accepting--thoughts?

Thanks, Everett Maus

[4tXJ7f]

Thanks for looking into this. We've discussed the issue during today's meeting and we have decided that it would be great to have your fix as a short term solution. We are planning to do some refactoring of the options s.t. the fix shouldn't be necessary in the future but it is better to have a temporary solution for now.

[evmaus]

Sounds great--I'll work on that fix sometime in the next week or so.

[ajreynol]

Options are now stored local to solvers. This issue can be closed.