From 5c8cbaea3aeee70e136164c905a2e03dc0b7e079 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Tue, 16 Jun 2026 20:15:10 -0700 Subject: [PATCH] Handle cancellation for parallel leases --- src/smt/smt_parallel.cpp | 57 +++++++++++++++++++++++-------- src/smt/smt_parallel.h | 3 +- src/solver/parallel_tactical2.cpp | 48 +++++++++++++++++++------- 3 files changed, 81 insertions(+), 27 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index b28d7d2d0..5497d7ec0 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -80,6 +80,7 @@ namespace smt { try { if (!m.inc()) { b.set_canceled(); + // b.notify_cv_waiters; return; } res = m_sls->check(); @@ -227,7 +228,8 @@ namespace smt { bb_candidates.reset(); } if (!m.inc()) - b.set_canceled(); + b.set_canceled(); + // b.notify_cv_waiters; } lbool parallel::backbones_worker::probe_literal(bool_var v, expr *e, bool is_retry) { @@ -397,6 +399,7 @@ namespace smt { if (!m.inc()) { b.set_canceled(); + // b.notify_cv_waiters; return; } if (canceled()) @@ -524,6 +527,7 @@ namespace smt { } if (!m.inc()) b.set_canceled(); + // b.notify_cv_waiters; } void parallel::backbones_worker::cancel() { @@ -752,6 +756,7 @@ namespace smt { b.publish_minimized_core(m_l2g, asms, source, original_size, minimized); } b.set_canceled(); + // b.notify_cv_waiters; } void parallel::worker::run() { @@ -773,21 +778,29 @@ namespace smt { if (m_config.m_global_backbones) { bb_candidates local_candidates = find_backbone_candidates(); b.collect_backbone_candidates(m_l2g, local_candidates); - if (!m.inc()) + if (!m.inc()) { + b.set_canceled(); + // b.notify_cv_waiters; break; + } } lbool r = check_cube(cube); - if (b.lease_canceled(lease)) { + bool cancel_signaled = false; + if (b.release_canceled_lease(id, lease, cancel_signaled)) { LOG_WORKER(1, " abandoning canceled lease\n"); lease = {}; - m.limit().dec_cancel(); + if (cancel_signaled) + m.limit().dec_cancel(); continue; } - if (!m.inc()) + if (!m.inc()) { + b.set_canceled(); + // b.notify_cv_waiters; break; + } switch (r) { case l_undef: { @@ -846,8 +859,11 @@ namespace smt { if (m_config.m_share_units) share_units(); } - if (!m.inc()) + if (!m.inc()) { b.set_canceled(); + // b.notify_cv_waiters; + return; + } } parallel::worker::worker(unsigned id, parallel &p, expr_ref_vector const &_asms) @@ -1448,9 +1464,22 @@ namespace smt { release_lease_unlocked(worker_id, lease.leased_node); } - bool parallel::batch_manager::lease_canceled(node_lease const &lease) { + bool parallel::batch_manager::release_canceled_lease(unsigned worker_id, node_lease const &lease, bool& cancel_signaled) { std::scoped_lock lock(mux); - return m_state == state::is_running && m_search_tree.is_lease_canceled(lease.leased_node); + cancel_signaled = false; + if (m_state != state::is_running || !lease.leased_node || worker_id >= m_worker_leases.size()) + return false; + + auto& stored = m_worker_leases[worker_id]; + if (stored.leased_node != lease.leased_node) + return false; + + if (!m_search_tree.is_lease_canceled(stored.leased_node)) + return false; + + cancel_signaled = stored.cancel_signaled; + release_lease_unlocked(worker_id, stored.leased_node); + return true; } void parallel::batch_manager::collect_clause(ast_translation &l2g, unsigned source_worker_id, expr *clause) { @@ -1700,6 +1729,12 @@ namespace smt { cancel_background_threads(); } + // void parallel::batch_manager::notify_cv_waiters { + // std::scoped_lock lock(mux); + // m_bb_cv.notify_all(); + // m_core_min_cv.notify_all(); + // } + void parallel::batch_manager::set_exception(unsigned error_code) { std::scoped_lock lock(mux); IF_VERBOSE(1, verbose_stream() << "Batch manager setting exception code: " << error_code << ".\n"); @@ -1876,20 +1911,14 @@ namespace smt { auto safe_run = [&](auto* w) { try { w->run(); - if (w->limit().is_canceled()) - m_batch_manager.set_canceled(); } catch (z3_error& err) { if (!w->limit().is_canceled()) m_batch_manager.set_exception(err.error_code()); - else - m_batch_manager.set_canceled(); } catch (z3_exception& ex) { if (!w->limit().is_canceled() && !is_cancellation_exception(ex.what())) m_batch_manager.set_exception(ex.what()); - else - m_batch_manager.set_canceled(); } }; diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index f1ebfcd0c..2e0632aed 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -191,6 +191,7 @@ namespace smt { void set_exception(std::string const& msg); void set_exception(unsigned error_code); void set_canceled(); + void notify_cv_waiters(); void collect_statistics(::statistics& st) const; void collect_backbone_candidates(ast_translation& l2g, bb_candidates& bb_candidates); @@ -220,7 +221,7 @@ namespace smt { unsigned original_core_size, expr_ref_vector const& minimized_core); void try_split(ast_translation& l2g, unsigned worker_id, node_lease const& lease, expr* atom, unsigned effort); void release_lease(unsigned worker_id, node_lease const& lease); - bool lease_canceled(node_lease const& lease); + bool release_canceled_lease(unsigned worker_id, node_lease const& lease, bool& cancel_signaled); void collect_clause(ast_translation& l2g, unsigned source_worker_id, expr* clause); expr_ref_vector return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id); diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index c7eddb4d8..de87f33da 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -474,13 +474,20 @@ class parallel_solver { cancel_background_threads(); } - void set_cancel() { + void set_canceled() { std::scoped_lock lock(mux); if (m_state != state::is_running) return; cancel_background_threads(); } + // CODE IS LOCKED WHEN WE ADD THIS FUNCTION -- NEED TO FIX + // void notify_cv_waiters() { + // std::scoped_lock lock(mux); + // m_bb_cv.notify_all(); + // m_core_min_cv.notify_all(); + // } + void set_unsat(ast_translation& l2g, expr_ref_vector const& core) { std::scoped_lock lock(mux); @@ -714,10 +721,22 @@ class parallel_solver { release_lease_unlocked(worker_id, lease.leased_node); } - bool lease_canceled(node_lease const& lease) { + bool release_canceled_lease(unsigned worker_id, node_lease const& lease, bool& cancel_signaled) { std::scoped_lock lock(mux); - return m_state == state::is_running && - m_search_tree.is_lease_canceled(lease.leased_node); + cancel_signaled = false; + if (m_state != state::is_running || !lease.leased_node || worker_id >= m_worker_leases.size()) + return false; + + auto& stored = m_worker_leases[worker_id]; + if (stored.leased_node != lease.leased_node) + return false; + + if (!m_search_tree.is_lease_canceled(stored.leased_node)) + return false; + + cancel_signaled = stored.cancel_signaled; + release_lease_unlocked(worker_id, stored.leased_node); + return true; } void collect_clause(ast_translation& l2g, @@ -1164,17 +1183,20 @@ class parallel_solver { } lbool r = check_cube(cube); - if (b.lease_canceled(lease)) { + bool cancel_signaled = false; + if (b.release_canceled_lease(id, lease, cancel_signaled)) { LOG_WORKER(1, " abandoning canceled lease\n"); lease = {}; - m.limit().dec_cancel(); + if (cancel_signaled) + m.limit().dec_cancel(); continue; } // NSB - at this point it shouldn't be possible to call inc_cancel. // Is this ensured? I am not sure. if (!m.inc()) { - b.set_cancel(); + b.set_canceled(); + // b.notify_cv_waiters(); return; } @@ -1492,7 +1514,8 @@ class parallel_solver { while (true) { if (!m.inc()) { - b.set_cancel(); + b.set_canceled(); + // b.notify_cv_waiters(); return; } if (canceled()) @@ -1819,7 +1842,8 @@ class parallel_solver { if (minimized.size() < original_size) b.publish_minimized_core(m_l2g, asms, source, original_size, minimized); } - b.set_cancel(); + b.set_canceled(); + // b.notify_cv_waiters(); } void cancel() { @@ -1930,19 +1954,19 @@ public: try { run_fn(); if (lim.is_canceled()) - m_batch_manager.set_cancel(); + m_batch_manager.set_canceled(); } catch (z3_error &err) { IF_VERBOSE(0, verbose_stream() << "Exception in parallel solver: " << err.what() << "\n"); if (!lim.is_canceled()) m_batch_manager.set_exception(err.error_code()); else - m_batch_manager.set_cancel(); + m_batch_manager.set_canceled(); } catch (z3_exception &ex) { IF_VERBOSE(0, verbose_stream() << "Exception in parallel solver: " << ex.what() << "\n"); if (!lim.is_canceled() && !is_cancellation_exception(ex.what())) m_batch_manager.set_exception(ex.what()); else - m_batch_manager.set_cancel(); + m_batch_manager.set_canceled(); } };