Multithreaded Z3?

Question

I am working on a Python project where I am currently trying to speed things up with some terrible ways: I configured my Z3 solvers, then I unlocked the process and executed the Z3 solution in the child process and pass the model model view to the parent.

This works great and represents the first step of what I'm trying to do: the parent process is now no longer connected to the CPU. The next step is the multithreading of the parent element, so that we can solve several Z3 solvers in parallel.

I am sure that I have mutual access to Z3 at the setup stage, and only one thread should touch Z3 at any time. However, despite this, I get random segfaults in libz3.so. It is important to note that at the moment this is not always the same thread that concerns Z3 - the same object (not the solvers themselves, but the expressions) can be processed by different threads at different times.

My question is: is multithreaded Z3 possible? Here is a brief note ( http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html ): "It is unsafe to access Z3 objects from multiple threads", which, I think, will answer my question is, but I hope this means saying that you cannot access Z3 from multiple threads at the same time. Another resource ( Again: installing Z3 + Python on Windows ) claims that Leonardo himself says that "Z3 uses local thread storage", which, I think, would lose all this but a) that the answer is from 2012, so maybe everything has changed, and b) maybe it uses local storage for some unrelated material?

Anyway, maybe multi-threaded Z3 (from Python)? I would not want to push the installation phase to child processes ...

Answer 1

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

Z3 should behave well in multi-threaded configuration if each thread strictly uses only its own context object (Z3_context or in the context of the Python class). This means that any object created through one of the Context cannot in any way interact with any other Context; if necessary, all objects must first be moved from one context to another, for example. in Python using functions such as translate (...) in the ASTRef class.

However, some errors are probably fixed. My first goal, when you see random segfaults, will be a garbage collector because it can interact poorly with Z3 link counting (which is the case in other APIs). There is also a known bug that fires when many context objects are created at the same time (in my task list, though ...)