Mehrfachgewinde Z3?

Question

Ich arbeite an einem Python-Projekt, bei dem ich derzeit versuche, die Dinge auf schreckliche Weise zu beschleunigen: Ich habe meine Z3-Solver eingerichtet, dann verzweige ich den Prozess und lasse Z3 die Lösung im Kind-Prozess ausführen übergeben Sie eine Pickle-fähige Darstellung des Modells zurück zum Eltern.

Das funktioniert gut und stellt die erste Stufe von dem, was ich versuche, dar: der Elternprozess ist jetzt nicht mehr CPU-gebunden. Der nächste Schritt besteht darin, den übergeordneten Thread zu multi-threading-fähig zu machen, sodass wir mehrere Z3-Solver parallel lösen können.

Ich bin mir ziemlich sicher, dass ich alle gleichzeitigen Zugriffe von Z3 in der Setup-Phase mutexed habe, und nur ein Thread sollte Z3 zu jeder Zeit berühren. Trotzdem bekomme ich in libz3.so zufällige segfaults. Es ist wichtig an dieser Stelle darauf hinzuweisen, dass es nicht immer der selbe Thread ist, der Z3 berührt - das gleiche Objekt (nicht die Solver selbst, sondern die Ausdrücke) könnte von verschiedenen Threads zu unterschiedlichen Zeiten bearbeitet werden.

Meine Frage ist, ist es möglich, Z3 Multi-Thread? Es gibt eine kurze Notiz hier (http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html), die sagt: "Es ist nicht sicher, auf Z3-Objekte aus mehreren Threads zuzugreifen.", Was ich meine Frage beantworten würde, aber ich hoffe, dass es bedeutet zu sagen, dass man sollte Zugriff auf Z3 von mehreren Threads gleichzeitig. Eine andere Ressource (Again: Installing Z3 + Python on Windows) sagt, von Leonardo selbst, dass "Z3 lokalen lokalen Speicher verwendet", was, denke ich, dieses ganze Unternehmen versenken würde, aber a) diese Antwort ist von 2012, also haben sich vielleicht die Dinge geändert und b) vielleicht es verwendet thread-lokalen Speicher für einige nicht verwandte Sachen?

Wie auch immer, ist Multithreading Z3 möglich (aus Python)? Ich würde es hassen, die Setup-Phase in die Child-Prozesse schieben zu müssen ...

Answer 1

Z3 verwendet tatsächlich Thread lokalen Speicher, aber soweit ich sehen kann, gibt es nur einen Punkt im Code, wo es tut So (um zu verfolgen, wie viel Speicher jeder Thread verwendet; in memory_manager.cpp), aber das sollte nicht für die Symptome verantwortlich sein, die Sie sehen.

Z3 sollte sich in einer Multi-Thread-Einstellung gut verhalten, wenn jeder Thread ausschließlich sein eigenes Kontextobjekt (Z3_context oder in der Python-Klasse Context) verwendet. Dies bedeutet, dass jedes Objekt, das durch einen der Kontext erzeugt wird, in keiner Weise mit irgendeinem der anderen Kontext interagieren kann; Wenn dies erforderlich ist, müssen alle Objekte zuerst von einem Kontext zu einem anderen übersetzt werden, z. in Python über Funktionen wie translate (...) in der Klasse ASTRef.

Das heißt, es gibt sicherlich noch einige Fehler zu beheben. Mein erstes Ziel beim Betrachten zufälliger Segfaults wäre der Garbage Collector, weil er möglicherweise nicht gut mit Z3s Referenzzählung interagiert (was bei anderen APIs der Fall ist). Es gibt auch einen bekannten Fehler, der ausgelöst wird, wenn viele Context-Objekte gleichzeitig erstellt werden (auf meiner Todo-Liste ...)