From 71bad7159b1f821c61196b8a7c010f08a5119442 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 Nov 2024 11:20:05 -0800 Subject: [PATCH] #7418 - circumvent use of timer threads to make WASM integration of z3 easier The scoped_timer uses a std::therad. Spawning this thread fails in cases of WASM. Instead of adapting builds and using async features at the level of WASM and the client, we expose a specialized version of z3 that doesn't use threads at all, neither for solvers nor for timers. The tradeoff is that the periodic poll that checks for timeout directly queries the global clock each time. We characterize it as based on polling. --- CMakeLists.txt | 15 ++++++ README-CMake.md | 1 + src/api/python/setup.py | 4 +- src/tactic/portfolio/smt_strategic_solver.cpp | 25 +++++----- src/util/cancel_eh.h | 9 ++-- src/util/rlimit.cpp | 44 ++++++++++++++--- src/util/rlimit.h | 47 +++++++++++++++---- src/util/scoped_timer.cpp | 10 ++++ 8 files changed, 124 insertions(+), 31 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index cfd43571422..34f3caecdeb 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -254,6 +254,21 @@ else() message(STATUS "Thread-safe build") endif() + +################################################################################ +# Use polling based timeout. This avoids spawning threads for timer tasks +################################################################################ +option(Z3_POLLING_TIMER + "Use polling based timeout checks" + OFF +) +if (Z3_POLLING_TIMER) + list(APPEND Z3_COMPONENT_CXX_DEFINES "-DPOLLING_TIMER") + message(STATUS "Polling based timer") +endif() + + + ################################################################################ # FP math ################################################################################ diff --git a/README-CMake.md b/README-CMake.md index 9bfc2d9ef29..04773718614 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -310,6 +310,7 @@ The following useful options can be passed to CMake whilst configuring. * ``Z3_BUILD_TEST_EXECUTABLES`` - BOOL. If set to ``TRUE`` build the z3 test executables. Defaults to ``TRUE`` unless z3 is being built as a submodule in which case it defaults to ``FALSE``. * ``Z3_SAVE_CLANG_OPTIMIZATION_RECORDS`` - BOOL. If set to ``TRUE`` saves Clang optimization records by setting the compiler flag ``-fsave-optimization-record``. * ``Z3_SINGLE_THREADED`` - BOOL. If set to ``TRUE`` compiles Z3 for single threaded mode. +* ``Z3_POLLING_TIMER`` - BOOL. If set to ``TRUE`` compiles Z3 to use polling based timer instead of requiring a thread. This is useful for wasm builds and avoids spawning threads that interfere with how WASM is run. On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface. diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 6c826d478df..7b2ec6fbc9a 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -30,6 +30,7 @@ class LibError(Exception): IS_PYODIDE = 'PYODIDE_ROOT' in os.environ and os.environ.get('_PYTHON_HOST_PLATFORM', '').startswith('emscripten') + # determine where binaries are RELEASE_DIR = os.environ.get('PACKAGE_FROM_RELEASE', None) if RELEASE_DIR is None: @@ -133,7 +134,8 @@ def _configure_z3(): # Config options cmake_options = { # Config Options - 'Z3_SINGLE_THREADED' : IS_SINGLE_THREADED, + 'Z3_SINGLE_THREADED' : IS_SINGLE_THREADED, # avoid solving features that use threads + 'Z3_POLING_TIMER' : IS_SINGLE_THREADED, # avoid using timer threads 'Z3_BUILD_PYTHON_BINDINGS' : True, # Build Options 'CMAKE_BUILD_TYPE' : 'Release', diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 0f952e016d7..5257a70b539 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -20,6 +20,7 @@ Module Name: #include "cmd_context/cmd_context.h" #include "solver/combined_solver.h" #include "solver/tactic2solver.h" +#include "tactic/tactical.h" #include "tactic/smtlogics/qfbv_tactic.h" #include "tactic/smtlogics/qflia_tactic.h" #include "tactic/smtlogics/qfnia_tactic.h" @@ -67,27 +68,27 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const else if (logic=="QF_BV") return mk_qfbv_tactic(m, p); else if (logic=="QF_IDL") - return mk_qfidl_tactic(m, p); + return annotate_tactic("qfidl-tactic", mk_qfidl_tactic(m, p)); else if (logic=="QF_LIA") - return mk_qflia_tactic(m, p); + return annotate_tactic("qflia-tactic", mk_qflia_tactic(m, p)); else if (logic=="QF_LRA") - return mk_qflra_tactic(m, p); + return annotate_tactic("qflra-tactic", mk_qflra_tactic(m, p)); else if (logic=="QF_NIA") - return mk_qfnia_tactic(m, p); + return annotate_tactic("qfnia-tactic", mk_qfnia_tactic(m, p)); else if (logic=="QF_NRA") - return mk_qfnra_tactic(m, p); + return annotate_tactic("qfnra-tactic", mk_qfnra_tactic(m, p)); else if (logic=="QF_AUFLIA") - return mk_qfauflia_tactic(m, p); + return annotate_tactic("qfauflia-tactic", mk_qfauflia_tactic(m, p)); else if (logic=="QF_AUFBV") - return mk_qfaufbv_tactic(m, p); + return annotate_tactic("qfaufbv-tactic", mk_qfaufbv_tactic(m, p)); else if (logic=="QF_ABV") - return mk_qfaufbv_tactic(m, p); + return annotate_tactic("qfaufbv-tactic", mk_qfaufbv_tactic(m, p)); else if (logic=="QF_UFBV") - return mk_qfufbv_tactic(m, p); + return annotate_tactic("qfufbv-tactic", mk_qfufbv_tactic(m, p)); else if (logic=="AUFLIA") - return mk_auflia_tactic(m, p); + return annotate_tactic("auflia-tactic", mk_auflia_tactic(m, p)); else if (logic=="AUFLIRA") - return mk_auflira_tactic(m, p); + return annotate_tactic("auflira-tactic", mk_auflira_tactic(m, p)); else if (logic=="AUFNIRA") return mk_aufnira_tactic(m, p); else if (logic=="UFNIA") @@ -101,7 +102,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const else if (logic=="LIA") return mk_lia_tactic(m, p); else if (logic=="UFBV") - return mk_ufbv_tactic(m, p); + return annotate_tactic("ufbv", mk_ufbv_tactic(m, p)); else if (logic=="BV") return mk_ufbv_tactic(m, p); else if (logic=="QF_FP") diff --git a/src/util/cancel_eh.h b/src/util/cancel_eh.h index 5ccf31636e3..d609b957a6f 100644 --- a/src/util/cancel_eh.h +++ b/src/util/cancel_eh.h @@ -25,11 +25,12 @@ Revision History: */ template class cancel_eh : public event_handler { - bool m_canceled; + bool m_canceled = false; + bool m_auto_cancel = false; T & m_obj; public: - cancel_eh(T & o): m_canceled(false), m_obj(o) {} - ~cancel_eh() override { if (m_canceled) m_obj.dec_cancel(); } + cancel_eh(T & o): m_obj(o) {} + ~cancel_eh() override { if (m_canceled) m_obj.dec_cancel(); if (m_auto_cancel) m_obj.auto_cancel(); } void operator()(event_handler_caller_t caller_id) override { if (!m_canceled) { m_caller_id = caller_id; @@ -39,5 +40,7 @@ class cancel_eh : public event_handler { } bool canceled() const { return m_canceled; } void reset() { m_canceled = false; } + T& t() { return m_obj; } + void set_auto_cancel() { m_auto_cancel = true; } }; diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index ea2e68b311b..28656bc63f1 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -31,11 +31,7 @@ void finalize_rlimit() { DEALLOC_MUTEX(g_rlimit_mux); } -reslimit::reslimit(): - m_cancel(0), - m_suspend(false), - m_count(0), - m_limit(std::numeric_limits::max()) { +reslimit::reslimit() { } uint64_t reslimit::count() const { @@ -117,7 +113,7 @@ void reslimit::reset_cancel() { void reslimit::inc_cancel() { lock_guard lock(*g_rlimit_mux); - set_cancel(m_cancel+1); + set_cancel(m_cancel + 1); } void reslimit::dec_cancel() { @@ -133,3 +129,39 @@ void reslimit::set_cancel(unsigned f) { m_children[i]->set_cancel(f); } } + + + +#ifdef POLLING_TIMER +void reslimit::push_timeout(unsigned ms) { + m_num_timers++; + if (m_cancel > 0) { + ++m_cancel; + return; + } + if (m_timeout_ms != 0) { + double ms_taken = 1000 * m_timer.get_seconds(); + if (ms_taken > m_timeout_ms) + return; + if (m_timeout_ms - ms_taken < ms) + return; + } + m_timer = timer(); + m_timeout_ms = ms; +} + +void reslimit::inc_cancel(unsigned k) { + lock_guard lock(*g_rlimit_mux); + set_cancel(m_cancel + k); +} + +void reslimit::auto_cancel() { + --m_num_timers; + dec_cancel(); +} + +#else +void reslimit::auto_cancel() { + UNREACHABLE(); +} +#endif \ No newline at end of file diff --git a/src/util/rlimit.h b/src/util/rlimit.h index 59bd818a2cc..c8688e4e2bb 100644 --- a/src/util/rlimit.h +++ b/src/util/rlimit.h @@ -19,6 +19,7 @@ Revision History: #pragma once #include "util/vector.h" +#include "util/timer.h" #include void initialize_rlimit(); @@ -29,16 +30,38 @@ void finalize_rlimit(); */ class reslimit { - std::atomic m_cancel; - bool m_suspend; - uint64_t m_count; - uint64_t m_limit; - svector m_limits; - ptr_vector m_children; + std::atomic m_cancel = 0; + bool m_suspend = false; + uint64_t m_count = 0; + uint64_t m_limit = std::numeric_limits::max(); +#ifdef POLLING_TIMER + timer m_timer; + unsigned m_timeout_ms = 0; + unsigned m_num_timers = 0; +#endif + svector m_limits; + ptr_vector m_children; + void set_cancel(unsigned f); friend class scoped_suspend_rlimit; +#ifdef POLLING_TIMER + bool is_timeout() { return m_timer.ms_timeout(m_timeout_ms) && (inc_cancel(m_num_timers), pop_timeout(), true); } + void inc_cancel(unsigned k); +#else + inline bool is_timeout() { return false; } +#endif + +#ifdef POLLING_TIMER + + void pop_timeout() { + m_timeout_ms = 0; + } + + void push_timeout(unsigned ms); +#endif + public: reslimit(); void push(unsigned delta_limit); @@ -52,15 +75,21 @@ class reslimit { uint64_t count() const; void reset_count() { m_count = 0; } - bool suspended() const { return m_suspend; } - inline bool not_canceled() const { return (m_cancel == 0 && m_count <= m_limit) || m_suspend; } - inline bool is_canceled() const { return !not_canceled(); } +#ifdef POLLING_TIMER + void set_timeout(unsigned ms) { push_timeout(ms); } +#endif + bool suspended() const { return m_suspend; } + inline bool not_canceled() { + return m_suspend || (m_cancel == 0 && m_count <= m_limit && !is_timeout()); + } + inline bool is_canceled() { return !not_canceled(); } char const* get_cancel_msg() const; void cancel(); void reset_cancel(); void inc_cancel(); void dec_cancel(); + void auto_cancel(); }; class scoped_rlimit { diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index ce1b14a23bd..4a62b928059 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -22,6 +22,8 @@ Revision History: #include "util/scoped_timer.h" #include "util/mutex.h" #include "util/util.h" +#include "util/cancel_eh.h" +#include "util/rlimit.h" #include #include #include @@ -79,6 +81,14 @@ scoped_timer::scoped_timer(unsigned ms, event_handler * eh) { if (ms == 0 || ms == UINT_MAX) return; +#ifdef POLLING_TIMER + auto* r = dynamic_cast*>(eh); + if (r) { + r->t().set_timeout(ms); + r->set_auto_cancel(); + return; + } +#endif workers.lock(); if (available_workers.empty()) { // start new thead