From e88cac2fe1177b9cd2f899efe97a26825f387e44 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Tue, 16 Jun 2026 21:37:11 -0700 Subject: [PATCH] restore smt_parallel to old/original version so we have a consistent baseline (even though it still includes newer bugs we've identified) --- src/smt/smt_parallel.cpp | 145 +++++++++++---------------------------- src/smt/smt_parallel.h | 12 ++-- 2 files changed, 48 insertions(+), 109 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 5497d7ec0..fdad743e3 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -25,7 +25,7 @@ Author: #include "smt/smt_parallel.h" #include "smt/smt_lookahead.h" #include "solver/solver_preprocess.h" -#include "solver/parallel_params.hpp" +#include "params/smt_parallel_params.hpp" #include #include @@ -78,11 +78,8 @@ namespace smt { lbool res = l_undef; try { - if (!m.inc()) { - b.set_canceled(); - // b.notify_cv_waiters; + if (!m.inc()) return; - } res = m_sls->check(); } catch (z3_exception &ex) { // Cancellation is normal in portfolio mode @@ -183,9 +180,8 @@ namespace smt { for (expr* lit : bb_candidate_lits) { if (is_retry && b.has_new_backbone_candidates(bb_candidate_epoch)) break; - if (!m.inc() || canceled()) + if (!m.inc() || canceled()) break; - expr* atom = lit; m.is_not(lit, atom); @@ -222,14 +218,11 @@ namespace smt { } if (!m.inc()) - break; + return; if (!canceled()) b.cancel_current_backbone_batch(); bb_candidates.reset(); } - if (!m.inc()) - b.set_canceled(); - // b.notify_cv_waiters; } lbool parallel::backbones_worker::probe_literal(bool_var v, expr *e, bool is_retry) { @@ -397,11 +390,8 @@ namespace smt { while (true) { - if (!m.inc()) { - b.set_canceled(); - // b.notify_cv_waiters; + if (!m.inc()) return; - } if (canceled()) break; @@ -525,9 +515,6 @@ namespace smt { bb_curr_batch_candidates.reset(); } - if (!m.inc()) - b.set_canceled(); - // b.notify_cv_waiters; } void parallel::backbones_worker::cancel() { @@ -755,8 +742,6 @@ namespace smt { if (minimized.size() < original_size) b.publish_minimized_core(m_l2g, asms, source, original_size, minimized); } - b.set_canceled(); - // b.notify_cv_waiters; } void parallel::worker::run() { @@ -778,29 +763,21 @@ 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()) { - b.set_canceled(); - // b.notify_cv_waiters; - break; - } + if (!m.inc()) + return; } lbool r = check_cube(cube); - bool cancel_signaled = false; - if (b.release_canceled_lease(id, lease, cancel_signaled)) { + if (b.lease_canceled(lease)) { LOG_WORKER(1, " abandoning canceled lease\n"); lease = {}; - if (cancel_signaled) - m.limit().dec_cancel(); + m.limit().dec_cancel(); continue; } - if (!m.inc()) { - b.set_canceled(); - // b.notify_cv_waiters; - break; - } + if (!m.inc()) + return; switch (r) { case l_undef: { @@ -859,11 +836,6 @@ namespace smt { if (m_config.m_share_units) share_units(); } - if (!m.inc()) { - b.set_canceled(); - // b.notify_cv_waiters; - return; - } } parallel::worker::worker(unsigned id, parallel &p, expr_ref_vector const &_asms) @@ -882,10 +854,10 @@ namespace smt { m_num_initial_atoms = ctx->get_num_bool_vars(); ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged - parallel_params pp(p.ctx.get_params()); - m_config.m_inprocessing = false; - m_config.m_global_backbones = pp.num_bb_threads() > 0; - m_config.m_local_backbones = false; + smt_parallel_params pp(p.ctx.m_params); + m_config.m_inprocessing = pp.inprocessing(); + m_config.m_global_backbones = pp.num_global_bb_batch_threads() > 0 || pp.num_global_bb_fl_threads() > 0; + m_config.m_local_backbones = pp.local_backbones(); m_config.m_core_minimize = pp.core_minimize(); m_config.m_ablate_backtracking = pp.ablate_backtracking(); @@ -916,7 +888,9 @@ namespace smt { m_shared_units_prefix = ctx->assigned_literals().size(); m_num_initial_atoms = ctx->get_num_bool_vars(); ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged - m_use_failed_literal_test = false; // true failed literal mode, false for Janota chunking algorithm + + smt_parallel_params pp(p.ctx.m_params); + m_use_failed_literal_test = pp.num_global_bb_fl_threads() > 0; } parallel::bb_candidates parallel::worker::find_backbone_candidates(unsigned k) { @@ -1206,13 +1180,14 @@ namespace smt { unsigned best_idx = select_best_core_min_job_unlocked(); m_core_min_jobs.swap(best_idx, m_core_min_jobs.size() - 1); - scoped_ptr job = m_core_min_jobs.detach_back(); + core_min_job* job = m_core_min_jobs.detach_back(); m_core_min_jobs.pop_back(); SASSERT(job); source = job->source; core.reset(); for (expr* c : job->core) core.push_back(g2l(c)); + dealloc(job); return source != nullptr; } @@ -1384,7 +1359,7 @@ namespace smt { if (!is_highest_ancestor) continue; - targets.push_back({ t }); + targets.push_back({t}); } } @@ -1464,22 +1439,9 @@ namespace smt { release_lease_unlocked(worker_id, lease.leased_node); } - bool parallel::batch_manager::release_canceled_lease(unsigned worker_id, node_lease const &lease, bool& cancel_signaled) { + bool parallel::batch_manager::lease_canceled(node_lease const &lease) { std::scoped_lock lock(mux); - 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; + return m_state == state::is_running && m_search_tree.is_lease_canceled(lease.leased_node); } void parallel::batch_manager::collect_clause(ast_translation &l2g, unsigned source_worker_id, expr *clause) { @@ -1722,19 +1684,6 @@ namespace smt { cancel_background_threads(); } - void parallel::batch_manager::set_canceled() { - std::scoped_lock lock(mux); - if (m_state != state::is_running) - return; - 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"); @@ -1830,7 +1779,7 @@ namespace smt { m_worker_leases.reset(); m_worker_leases.resize(p.m_workers.size()); - parallel_params pp(p.ctx.get_params()); + smt_parallel_params pp(p.ctx.m_params); m_ablate_backtracking = pp.ablate_backtracking(); } @@ -1845,18 +1794,18 @@ namespace smt { } lbool parallel::operator()(expr_ref_vector const &asms) { - params_ref const& params = ctx.get_params(); - parallel_params pp(params); - unsigned num_global_bb_batch_threads = pp.num_bb_threads(); + smt_parallel_params pp(ctx.m_params); + unsigned num_global_bb_batch_threads = pp.num_global_bb_batch_threads(); if (num_global_bb_batch_threads > 2) - throw default_exception("parallel.num_bb_threads must be 0, 1, or 2"); + throw default_exception("smt_parallel.num_global_bb_batch_threads must be 0, 1, or 2"); unsigned num_workers = std::min((unsigned)std::thread::hardware_concurrency(), ctx.get_fparams().m_threads); - unsigned num_sls_threads = 0; - bool core_minimize = pp.core_minimize(); - if (pp.ablate_backtracking()) - core_minimize = false; - unsigned num_core_min_threads = (core_minimize ? 1 : 0); - unsigned num_global_bb_fl_threads = 0; + unsigned num_sls_threads = (pp.sls() ? 1 : 0); + unsigned num_core_min_threads = (pp.core_minimize() ? 1 : 0); + unsigned num_global_bb_fl_threads = pp.num_global_bb_fl_threads(); + if (num_global_bb_fl_threads > 2) + throw default_exception("smt_parallel.num_global_bb_fl_threads must be 0, 1, or 2"); + if (num_global_bb_fl_threads > 0 && num_global_bb_batch_threads > 0) + throw default_exception("smt_parallel.num_global_bb_fl_threads and smt_parallel.num_global_bb_batch_threads cannot both be enabled"); unsigned num_global_bb_threads = num_global_bb_fl_threads > 0 ? num_global_bb_fl_threads : num_global_bb_batch_threads; unsigned total_threads = num_workers + num_sls_threads + num_core_min_threads + num_global_bb_threads; @@ -1892,7 +1841,7 @@ namespace smt { m_sls_worker = alloc(sls_worker, *this); sl.push_child(&(m_sls_worker->limit())); } - if (num_core_min_threads == 1) { + if (pp.core_minimize()) { m_core_minimizer_worker = alloc(core_minimizer_worker, *this, asms); sl.push_child(&(m_core_minimizer_worker->limit())); } @@ -1908,31 +1857,17 @@ namespace smt { m_batch_manager.initialize(num_global_bb_threads); - auto safe_run = [&](auto* w) { - try { - w->run(); - } - catch (z3_error& err) { - if (!w->limit().is_canceled()) - m_batch_manager.set_exception(err.error_code()); - } - catch (z3_exception& ex) { - if (!w->limit().is_canceled() && !is_cancellation_exception(ex.what())) - m_batch_manager.set_exception(ex.what()); - } - }; - // Launch threads vector threads(total_threads); unsigned thread_idx = 0; for (auto* w : m_workers) - threads[thread_idx++] = std::thread([&, w]() { safe_run(w); }); + threads[thread_idx++] = std::thread([&, w]() { w->run(); }); if (m_sls_worker) - threads[thread_idx++] = std::thread([&]() { safe_run(m_sls_worker.get()); }); + threads[thread_idx++] = std::thread([&]() { m_sls_worker->run(); }); if (m_core_minimizer_worker) - threads[thread_idx++] = std::thread([&]() { safe_run(m_core_minimizer_worker.get()); }); + threads[thread_idx++] = std::thread([&]() { m_core_minimizer_worker->run(); }); for (auto* w : m_global_backbones_workers) - threads[thread_idx++] = std::thread([&, w]() { safe_run(w); }); + threads[thread_idx++] = std::thread([&, w]() { w->run(); }); // Wait for all threads to finish @@ -1953,4 +1888,4 @@ namespace smt { } } // namespace smt -#endif +#endif \ No newline at end of file diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 2e0632aed..d756782d7 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -64,6 +64,12 @@ namespace smt { struct node_lease { node* leased_node = nullptr; + // Cancellation generation counter for this node/subtree. + // Incremented when the node is closed; used to signal that all + // workers holding leases on this node (or its descendants) + // must abandon work immediately. + unsigned cancel_epoch = 0; + // Guards against multiple inc_cancel() calls for the same lease. // Set when cancel_lease() is signaled; cleared when a new lease is assigned. bool cancel_signaled = false; @@ -190,8 +196,6 @@ namespace smt { void set_sat(ast_translation& l2g, model& m); 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); @@ -221,7 +225,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 release_canceled_lease(unsigned worker_id, node_lease const& lease, bool& cancel_signaled); + bool lease_canceled(node_lease const& lease); 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); @@ -422,4 +426,4 @@ namespace smt { lbool operator()(expr_ref_vector const& asms); }; -} +} \ No newline at end of file