пока параметр parallel_enable
по-прежнему приводит к тому, что эта функция работает в однопоточном режиме и блокирует основной поток
Я думаю, вы неправильно это поняли. Запуск z3 в параллельном режиме означает, что вы вызываете его из одного потока Python, а затем он порождает несколько потоков уровня ОС для себя, выполняя работу, очищая потоки и возвращая результат для вас. Он не позволяет чудесным образом запускать Python без GIL.
С точки зрения Python, он все равно выполняет одну вещь за раз, и одна вещь делает вызов z3. И он держит GIL на все время. Поэтому, если вы видите, что более одного ядра / потока ЦП используется во время выполнения вычислений, это является эффектом параллельного режима z3, внутренне разветвляющегося на несколько потоков.
Есть еще одна вещь, освобождающая GIL, например, чтоблокировать операции ввода / вывода. Это не происходит по волшебству, для этого есть пара вызовов:
PyThreadState * PyEval_SaveThread ()
Снять глобальную блокировку интерпретатора (если она была создана)) и сбросить состояние потока на NULL
, возвращая предыдущее состояние потока (которое не равно NULL). Если блокировка была создана, текущий поток должен ее получить.
void PyEval_RestoreThread (PyThreadState * tstate)
Получить глобальную блокировку интерпретатора (если она была создана) иустановите состояние потока на tstate , которое не должно быть NULL
. Если блокировка была создана, текущий поток не должен был ее получить, в противном случае возникает взаимоблокировка.
Это вызовы C, поэтому они доступны для разработчиков расширений. Когда разработчики знают, что код будет работать долго, без необходимости доступа к внутренним компонентам Python, можно использовать PyEval_SaveThread()
, а затем Python сможет продолжить работу с другими потоками Python. И когда долго, что бы ни было сделано, поток может заново представиться и подать заявку на GIL, используя PyEval_RestoreThread()
.
Но эти вещи случаются, только если разработчики заставляют их происходить. А с z3 это может быть не так.
Чтобы дать прямой ответ на ваш вопрос: нет, код Python не может освободить GIL и сохранить его освобожденным, поскольку GIL - это блокировка, которую должен содержать поток Pythonкогда это продолжается. Поэтому всякий раз, когда Python возвращает «инструкцию», GIL снова удерживается.
Видимо, каким-то образом мне удалось не включить ссылку, которую я хотел, поэтому они находятся на странице https://docs.python.org/3/c-api/init.html#thread-state-and-the-global-interpreter-lock (ив связанном параграфе обсуждается то, что я кратко суммировал).
Z3 является открытым исходным кодом (https://github.com/Z3Prover/z3), и исходный код не содержит ни PyEval_SaveThread
, ни последовательности символов-оберток Py_BEGIN_ALLOW_THREADS
.
Но у него есть параллельный пример Python, кстати. https://github.com/Z3Prover/z3/blob/master/examples/python/parallel.py, с
from multiprocessing.pool import ThreadPool
Так что я бы предположил, что это может быть проверенои работает с multiprocessing
.