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

clean up but dangerous race condition is still present in the worker. an example:

Browse source 
1. Manager decides worker’s lease is stale.
  2. It records/sends lease cancel.
  3. Worker finishes naturally before observing
  4. Worker releases/discards old lease.
  5. The lease-cancel counter is still sitting on the worker limit.
  6. Later, a naked m.inc() check sees that stale cancel and treats it as global cancellation.
This commit is contained in:
Ilana Shapiro 2026-06-16 21:50:52 -07:00
parent e88cac2fe1
commit b5a3d4fcb0
1 changed files with 7 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/solver/parallel_tactical2.cpp
View file

@ -243,8 +243,8 @@ class parallel_solver {
auto const& lease = m_worker_leases[id]; auto const& lease = m_worker_leases[id];
if (lease.leased_node && !lease.cancel_signaled && if (lease.leased_node && !lease.cancel_signaled &&
m_search_tree.is_lease_canceled(lease.leased_node)) { m_search_tree.is_lease_canceled(lease.leased_node)) {
p.m_workers[id]->cancel_lease();
m_worker_leases[id].cancel_signaled = true; m_worker_leases[id].cancel_signaled = true;
p.m_workers[id]->cancel_lease();
} }
} }
} }
@ -481,13 +481,6 @@ class parallel_solver {
cancel_background_threads(); 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, void set_unsat(ast_translation& l2g,
expr_ref_vector const& core) { expr_ref_vector const& core) {
std::scoped_lock lock(mux); std::scoped_lock lock(mux);
@ -727,15 +720,15 @@ class parallel_solver {
if (m_state != state::is_running || !lease.leased_node || worker_id >= m_worker_leases.size()) if (m_state != state::is_running || !lease.leased_node || worker_id >= m_worker_leases.size())
return false; return false;
auto& stored = m_worker_leases[worker_id]; auto& stored_lease = m_worker_leases[worker_id];
if (stored.leased_node != lease.leased_node) if (stored_lease.leased_node != lease.leased_node)
return false; return false;
if (!m_search_tree.is_lease_canceled(stored.leased_node)) if (!m_search_tree.is_lease_canceled(stored_lease.leased_node))
return false; return false;
cancel_signaled = stored.cancel_signaled; cancel_signaled = stored_lease.cancel_signaled;
release_lease_unlocked(worker_id, stored.leased_node); release_lease_unlocked(worker_id, stored_lease.leased_node);
return true; return true;
} }
@ -1196,7 +1189,6 @@ class parallel_solver {
// Is this ensured? I am not sure. // Is this ensured? I am not sure.
if (!m.inc()) { if (!m.inc()) {
b.set_canceled(); b.set_canceled();
// b.notify_cv_waiters();
return; return;
} }
@ -1515,7 +1507,6 @@ class parallel_solver {
while (true) { while (true) {
if (!m.inc()) { if (!m.inc()) {
b.set_canceled(); b.set_canceled();
// b.notify_cv_waiters();
return; return;
} }
if (canceled()) if (canceled())
@ -1843,7 +1834,6 @@ class parallel_solver {
b.publish_minimized_core(m_l2g, asms, source, original_size, minimized); b.publish_minimized_core(m_l2g, asms, source, original_size, minimized);
} }
b.set_canceled(); b.set_canceled();
// b.notify_cv_waiters();
} }
void cancel() { void cancel() {