多线程Z3？

Question

我正在研究一个Python项目,我正在尝试以一些可怕的方式加快速度:我设置了Z3求解器,然后我分叉了这个过程,让Z3在子进程中执行求解并传递一个将模型的可挑剔表示返回到父级.

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

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

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

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

Answer 1

Z3确实确实使用了线程本地存储，但是据我所知，它只在其中保留了一点（以跟踪每个线程正在使用多少内存；在memory_manager.cpp中），但是那不应该对您看到的症状负责。

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

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