多线程 Z3？

Question

我正在进行一个Python项目，在其中试图以一些可怕的方式加快速度：我设置了我的Z3求解器，然后分叉进程，并让Z3在子进程中执行求解并将模型的可选表示传递回父进程。

这很有效，也代表我正在尝试的第一阶段：父进程现在不再被CPU限制。下一步是多线程化父进程，以便我们可以并行解决多个Z3求解器。

我相当确定我已经在设置阶段互斥地访问了任何Z3，并且在任何时候只有一个线程应该触及Z3。但是，尽管如此，我仍然会在libz3.so中遇到随机的segfaults。需要注意的是，在这一点上，不总是同一个线程触及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）也许它只是为了一些无关的东西而使用线程本地存储？无论如何，从Python多线程使用Z3是否可行？我不想把设置阶段推到子进程中...

- Zardus

Answer 1

Z3确实使用了线程本地存储，但据我所见，代码中只剩下一个点在使用它（用于跟踪每个线程使用的内存量，在memory_manager.cpp中），但这不应该导致您看到的症状。

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

话虽如此，肯定还有一些需要修复的错误。当看到随机段错误时，我的第一个目标是垃圾收集器，因为它可能与Z3的引用计数不良互动（这在其他API中也是如此）。还有一个已知的错误，在同时创建许多上下文对象时会触发（尽管在我的待办事项列表中...）

- Christoph Wintersteiger

---

啊，这很有道理。谢谢你的帮助！我在线程之间泄漏了上下文。 - Zardus

在单个线程上处理对象，但在多个线程之间共享它是一种常见的模式。这使得线程本地存储非常危险。例如：拥有一个共享的上下文，并仅在锁定区域中调用Z3。 - usr

@Christoph Wintersteiger：“还有一个已知的错误，当同时创建许多上下文对象时会触发（尽管在我的待办事项列表中...）”--这个问题解决了吗？我正在尝试在程序中多线程创建z3对象，但每当我在太多公式上运行并行化时，我会收到一个关于访问冲突的WindowsError异常，这对我来说没有太多意义，但可能与您的陈述有关。 - ec-m

@ec-m：我不知道。我们当时解决了一些问题，但最近又出现了几个类似的错误报告。请确保按顺序创建上下文对象并在启动任何线程之前按顺序调用*_translate函数。无论如何，请将完整的示例提交到我们的问题跟踪器中，否则这种类型的问题是无法调试的。 - Christoph Wintersteiger