Multi-threaded Z3?

Question

I'm working on a Python project, where I'm currently trying to speed things up in some horrible ways: I set up my Z3 solvers, then I fork the process, and have Z3 perform the solve in the child process and pass a pickle-able representation of the model back to the parent.

This works great, and represents the first stage of what I'm trying to do: the parent process is now no longer CPU-bound. The next step is to multi-thread the parent, so that we can solve multiple Z3 solvers in parallel.

I'm pretty sure I've mutexed away any concurrent accesses of Z3 in the setup phase, and only one thread should be touching Z3 at any one time. However, despite this, I'm getting random segfaults in libz3.so. It's important to note, at this point, that it's not always the same thread that touches Z3 -- the same object (not the solvers themselves, but the expressions) might be handled by different threads at different times.

My question is, is it possible to multi-thread Z3? There is a brief note here (http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html) saying "It is not safe to access Z3 objects from multiple threads.", which I guess would answer my question, but I'm holding out hope that it means to say that one shouldn't access Z3 from multiple threads simultaneously. Another resource (Again: Installing Z3 + Python on Windows) states, from Leonardo himself, that "Z3 uses thread local storage", which, I guess, would sink this whole undertaking, but a) that answer is from 2012, so maybe things have changed, and b) maybe it uses thread-local storage for some unrelated stuff?

Anyways, is multi-threading Z3 possible (from Python)? I'd hate to have to push the setup phase into the child processes...

Unleavened

Answer 1

Z3 does indeed use thread local storage, but as far as I can see, there is only one point left in the code where it does so (to track how much memory each thread is using; in memory_manager.cpp), but that should not be responsible for the symptoms you see.

Z3 should behave nicely in a multi-threaded setting, if every thread strictly uses only it's own context object (Z3_context, or in Python class Context). This means that any object created through one of the Context's can not in any way interact with any of the other Context's; if that is required, all objects have to be translated from one Context to another first, e.g. in Python via functions like translate(...) in class ASTRef.

That said, there surely are some bugs left to fix. My first target when seeing random segfaults would be the garbage collector, because it might not interact nicely with Z3's reference counting (which is the case in other APIs). There is also a known bug that's triggered when many Context objects are created at the same time (on my todo list though...)

Clymer

Ah, that makes sense. Thanks for your help! I was leaking contexts across threads. – Unleavened

It is a common pattern to work on an objects on a single thread at a time, but to share it between threads. That makes thread local storage very dangerous. Example: Have a shared Context and only call Z3 in a locked region. – Author

@Christoph Wintersteiger: "There is also a known bug that's triggered when many Context objects are created at the same time (on my todo list though...)" -- Is that solved? I am trying to multithread the creation of z3 objects in my program but whenever I run the parallelization on too many formulae at the time I receive an WindowsError exception about access violation that does not make a lot of sense to me but could be related to your statement. – Perron

@ec-m: I don't know. We fixed some issues at the time, but recently there were a couple new bug reports of a similar flavour. Make sure you create Context objects sequentially and call *_translate functions sequentially before starting any threads too. In any case, please submit a complete example to our issue tracker, otherwise this type of issue is un-debuggable. – Clymer