#7418 - circumvent use of timer threads to make WASM integration of z…

…3 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.
Z3Prover · Nov 21, 2024 · 71bad71 · 71bad71
1 parent 94f0aff
commit 71bad71
Show file tree

Hide file tree

Showing 8 changed files with 124 additions and 31 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -25,11 +25,12 @@ Revision History:
 */
 template<typename T>
 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
@@ -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<uint64_t>::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
diff --git 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 <atomic>
 
 void initialize_rlimit();
@@ -29,16 +30,38 @@ void finalize_rlimit();
 */
 
 class reslimit {
-    std::atomic<unsigned> m_cancel;
-    bool            m_suspend;
-    uint64_t        m_count;
-    uint64_t        m_limit;
-    svector<uint64_t> m_limits;
-    ptr_vector<reslimit> m_children;
+    std::atomic<unsigned> m_cancel = 0;
+    bool                  m_suspend = false;
+    uint64_t              m_count = 0;
+    uint64_t              m_limit = std::numeric_limits<uint64_t>::max();
+#ifdef POLLING_TIMER
+    timer                 m_timer;
+    unsigned              m_timeout_ms = 0;
+    unsigned              m_num_timers = 0;
+#endif
+    svector<uint64_t>     m_limits;
+    ptr_vector<reslimit>  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
@@ -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 <atomic>
 #include <chrono>
 #include <climits>
@@ -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<cancel_eh<reslimit>*>(eh);
+    if (r) {
+        r->t().set_timeout(ms);
+        r->set_auto_cancel();
+        return;
+    }
+#endif
     workers.lock();
     if (available_workers.empty()) {
         // start new thead