z3 - 多线程Z3？

Question

我正在做一个 Python 项目，我目前正试图以一些可怕的方式加快速度:我设置了我的 Z3 求解器，然后我 fork 了这个过程，让 Z3 在子进程中执行求解并通过一个模型的pickle-able表示回到父级。

这很好用，代表了我正在尝试做的第一阶段:父进程现在不再受 CPU 限制。下一步是对父级进行多线程处理，以便我们可以并行求解多个 Z3 求解器。

我很确定我已经在设置阶段互斥了 Z3 的任何并发访问，并且在任何时候都应该只有一个线程接触 Z3。然而，尽管如此，我还是在 libz3.so 中遇到了随机段错误。重要的是要注意，在这一点上，接触 Z3 的线程并不总是相同的——同一个对象(不是求解器本身，而是表达式)可能在不同的时间由不同的线程处理。

我的问题是，是否可以多线程 Z3？这里有一个简短的说明( http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html )说“从多个线程访问 Z3 对象是不安全的。”，我想这会回答我的问题，但我希望这意味着说一个人应该不能同时从多个线程访问 Z3。另一个资源 ( Again: Installing Z3 + Python on Windows ) 来自 Leonardo 本人，指出“Z3 使用线程本地存储”，我想这会使整个项目陷入困境，但是 a) 答案是从 2012 年开始的，所以也许事情已经改变了，b ) 也许它使用线程本地存储来存储一些不相关的东西？

无论如何，多线程 Z3 是否可能(来自 Python)？我不想将设置阶段插入子进程......

Answer 1

Z3 确实使用了线程本地存储，但据我所知，代码中只剩下一点(跟踪每个线程使用了多少内存；在 memory_manager.cpp 中)，但这不应该对你看到的症状负责。

如果每个线程严格只使用它自己的上下文对象(Z3_context，或在 Python 类上下文中)，Z3 应该在多线程设置中表现良好。这意味着通过其中一个上下文创建的任何对象都不能以任何方式与任何其他上下文进行交互；如果需要，必须首先将所有对象从一个上下文转换为另一个上下文，例如在 Python 中，通过 ASTRef 类中的 translate(...) 等函数。

也就是说，肯定还有一些错误需要修复。我看到随机段错误时的第一个目标是垃圾收集器，因为它可能无法与 Z3 的引用计数很好地交互(在其他 API 中就是这种情况)。还有一个已知的错误会在同时创建多个 Context 对象时触发(尽管在我的待办事项列表中...)