mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 07:06:28 +00:00
Code Activity

Handle cancellation for parallel leases

Browse source
This commit is contained in:
Ilana Shapiro 2026-06-16 20:15:10 -07:00
parent c10e7c2a6f
commit 5c8cbaea3a
3 changed files with 81 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

57
src/smt/smt_parallel.cpp
View file

@ -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();
}
};

3
src/smt/smt_parallel.h
View file

@ -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);

48
src/solver/parallel_tactical2.cpp
View file

@ -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();
}
};