多线程Z3? [英] Multi-threaded Z3?

问题描述

我正在处理一个 Python 项目，我目前正在尝试以一些可怕的方式加快速度:我设置了 Z3 求解器，然后我分叉了进程，并让 Z3 在子进程中执行求解并将模型的可腌制表示传回父级.

I'm working on a Python project, where I'm currently trying to speed things up in some horrible ways: I set up my Z3 solvers, then I fork the process, and have Z3 perform the solve in the child process and pass a pickle-able representation of the model back to the parent.

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

This works great, and represents the first stage of what I'm trying to do: the parent process is now no longer CPU-bound. The next step is to multi-thread the parent, so that we can solve multiple Z3 solvers in parallel.

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

I'm pretty sure I've mutexed away any concurrent accesses of Z3 in the setup phase, and only one thread should be touching Z3 at any one time. However, despite this, I'm getting random segfaults in libz3.so. It's important to note, at this point, that it's not always the same thread that touches Z3 -- the same object (not the solvers themselves, but the expressions) might be handled by different threads at different times.

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

My question is, is it possible to multi-thread Z3? There is a brief note here (http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html) saying "It is not safe to access Z3 objects from multiple threads.", which I guess would answer my question, but I'm holding out hope that it means to say that one shouldn't access Z3 from multiple threads simultaneously. Another resource (Again: Installing Z3 + Python on Windows) states, from Leonardo himself, that "Z3 uses thread local storage", which, I guess, would sink this whole undertaking, but a) that answer is from 2012, so maybe things have changed, and b) maybe it uses thread-local storage for some unrelated stuff?

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

Anyways, is multi-threading Z3 possible (from Python)? I'd hate to have to push the setup phase into the child processes...

推荐答案

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

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

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

Z3 should behave nicely in a multi-threaded setting, if every thread strictly uses only it's own context object (Z3_context, or in Python class Context). This means that any object created through one of the Context's can not in any way interact with any of the other Context's; if that is required, all objects have to be translated from one Context to another first, e.g. in Python via functions like translate(...) in class ASTRef.

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

That said, there surely are some bugs left to fix. My first target when seeing random segfaults would be the garbage collector, because it might not interact nicely with Z3's reference counting (which is the case in other APIs). There is also a known bug that's triggered when many Context objects are created at the same time (on my todo list though...)

这篇关于多线程Z3?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！