Z3 Context Thread Safety Question

[toolCHAINZ]

This is sort of a follow-up to #4762. I've been working on the Rust z3 bindings and have been playing with a structured way to allow usages of the Rust API in multi-threaded scenarios (see prove-rs/z3.rs#404). From this investigation, I have a question about the thread-safety of the z3 context.

Background (feel free to skip)

My multi-threading strategy is this:

• Contexts can never be moved to other threads or referenced by other threads
• Asts, Solvers, Models, etc, may also never be moved or referenced across threads (I'm going to say Ast for the rest of this, but I mean any of these types that isn't a Context).
• Asts may be wrapped in a special SendableHandle structure:
  • By construction, this structure translates the Ast for a new Context, owned by the SendableHandle. No other code is able to see this Context.
  • After the translate is done, this Context is kept around for the lifetime of the SendableHandle, and no further declarations are made inside it.
• SendableHandle can be moved to another thread and then have its contents unwrapped and translated into an Ast associated with a Context owned by the receiving thread through a call to recover(&ctx).

This paradigm introduces some overhead, as Asts must be translated twice, and there's an extra Context construction/destruction every time something needs to move across threads, but it ensures that no Ast is ever accessed from a different thread than the Context it is associated with, without relying on rust-side atomics or mutexes.

So, my question comes because when I originally thought of this, I was thinking that the soundness of this approach required that SendableHandle could be moved to a thread but never referenced across threads. As an experiment I tried loosening these requirements and allowing references across threads. Much to my surprise, this worked.

TLDR

So, my question is about the safety of the following pattern of interactions with the Z3 context. If I:

• Allocate a Context
• Define some Ast/Solver/etc in it
• Make ABSOLUTELY SURE that nothing can ever touch that Context again outside of using it as the source of Z3_translate/Z3_solver_translate/etc calls.

Is it then safe to access the Context from other threads without synchronization?

[NikolajBjorner]

It isn't thread safe because z3_translate and related increment and decrement reference counts on ast nodes from the source context.
It uses the reference counts in order to maintain a cache when translating the same terms repeatedly. The source nodes have to be valid within the cache.
Reference counts are not thread safe (they are not atomic).
The safe approach is to use the "broker" as you describe.

I think you want to weigh the overhead of the broker against overhead of solving. Solving should be several orders of magnitude higher time and space overhead than replicating the ast nodes from the input. If ast node overhead is higher, then I am not sure it is useful to use threads in the first place.

I use a broker in the local search solver to allow two threads to communicate information without being blocked on each other.
For other thread uses, I initialize copies in a main thread and then effectively transfer ownership to worker threads. If they synchronize on shared state I use a lock with thread contention becoming part of the cost equation.

[toolCHAINZ]

This is very helpful thank you!

Yeah, I was worried about the overhead of the broker setup. I haven't attempted to profile it on a real-world workload, but in some small synthetic tests it was an order of magnitude less than time spent in solve so that's promising.

In light of what you said, I will plan to use a mutex inside the broker if I go through with exposing it across threads. Thanks again!