Многопоточный Z3?

Question

Я работаю над проектом Python, где в настоящее время я пытаюсь ускорить работу с некоторыми ужасными способами: я настроил свои решатели Z3, затем я разблокировал процесс и выполнил Z3 решение в дочернем процессе и передать образцовое представление модели для родителя.

Это отлично работает и представляет собой первый этап того, что я пытаюсь сделать: родительский процесс теперь больше не связан с ЦП. Следующим шагом будет многопоточность родителя, так что мы сможем решить несколько решателей Z3 параллельно.

Я уверен, что у меня есть взаимный доступ к Z3 на этапе настройки, и только один поток должен касаться Z3 в любой момент времени. Однако, несмотря на это, я получаю случайные segfaults в libz3.so. Важно отметить, что на данный момент не всегда тот же самый поток, который касается Z3 - тот же объект (а не сами решатели, но выражения) могут обрабатываться разными потоками в разное время.

Мой вопрос: возможно ли многопоточное Z3? Здесь содержится краткая заметка (http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html): «Невозможно получить доступ к объектам Z3 из нескольких потоков», что, я думаю, ответит на мой вопрос, но я надеюсь, что это означает, чтобы сказать, что нужно 't получить доступ к Z3 из нескольких потоков одновременно. Другой ресурс (Again: Installing Z3 + Python on Windows) утверждает, что сам «Леонардо» «Z3 использует локальное хранилище потоков», которое, я думаю, опустило бы все это, но а) ответ с 2012 года, поэтому, возможно, все изменилось, и б) возможно он использует поточное локальное хранилище для некоторых несвязанных вещей?

В любом случае, возможно многопоточное Z3 (от Python)? Мне бы очень хотелось, чтобы вы надавили фазу установки на дочерние процессы ...

Answer 1

Z3 действительно использует локальное хранилище потоков, но, насколько я вижу, в коде есть только одна точка, в которой он работает поэтому (чтобы отслеживать, сколько памяти использует каждый поток, в памяти_manager.cpp), но это не должно отвечать за симптомы, которые вы видите.

Z3 должен вести себя хорошо в многопоточной настройке, если каждая строка строго использует только собственный объект контекста (Z3_context или в контексте класса Python). Это означает, что любой объект, созданный через один из контекстов, никак не может взаимодействовать с каким-либо другим контекстом; если это необходимо, все объекты сначала должны быть переведены из одного контекста в другой, например. в Python с помощью таких функций, как translate (...) в классе ASTRef.

Это, конечно, есть некоторые ошибки, которые нужно исправить. Моя первая цель, когда вы видите случайные segfaults, будет сборщиком мусора, потому что она может плохо взаимодействовать с подсчетом ссылок Z3 (что имеет место в других API). Существует также известная ошибка, которая срабатывает, когда много объектов контекста создаются одновременно (в моем списке задач, хотя ...)