From b5a3d4fcb08dc70c1d9d8fd3edb91ae189a16910 Mon Sep 17 00:00:00 2001
From: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Date: Tue, 16 Jun 2026 21:50:52 -0700
Subject: [PATCH] =?UTF-8?q?clean=20up=20but=20dangerous=20race=20condition?=
 =?UTF-8?q?=20is=20still=20present=20in=20the=20worker.=20an=20example:=20?=
 =?UTF-8?q?=20=201.=20Manager=20decides=20worker=E2=80=99s=20lease=20is=20?=
 =?UTF-8?q?stale.=20=20=202.=20It=20records/sends=20lease=20cancel.=20=20?=
 =?UTF-8?q?=203.=20Worker=20finishes=20naturally=20before=20observing=20?=
 =?UTF-8?q?=20=204.=20Worker=20releases/discards=20old=20lease.=20=20=205.?=
 =?UTF-8?q?=20The=20lease-cancel=20counter=20is=20still=20sitting=20on=20t?=
 =?UTF-8?q?he=20worker=20limit.=20=20=206.=20Later,=20a=20naked=20m.inc()?=
 =?UTF-8?q?=20check=20sees=20that=20stale=20cancel=20and=20treats=20it=20a?=
 =?UTF-8?q?s=20global=20cancellation.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/solver/parallel_tactical2.cpp | 24 +++++++-----------------
 1 file changed, 7 insertions(+), 17 deletions(-)

diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp
index de87f33da..905adbbcd 100644
--- a/src/solver/parallel_tactical2.cpp
+++ b/src/solver/parallel_tactical2.cpp
@@ -243,8 +243,8 @@ class parallel_solver {
                 auto const& lease = m_worker_leases[id];
                 if (lease.leased_node && !lease.cancel_signaled &&
                     m_search_tree.is_lease_canceled(lease.leased_node)) {
-                    p.m_workers[id]->cancel_lease();
                     m_worker_leases[id].cancel_signaled = true;
+                    p.m_workers[id]->cancel_lease();
                 }
             }
         }
@@ -480,14 +480,7 @@ class parallel_solver {
                 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);
@@ -727,15 +720,15 @@ class parallel_solver {
             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)
+            auto& stored_lease = m_worker_leases[worker_id];
+            if (stored_lease.leased_node != lease.leased_node)
                 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;
 
-            cancel_signaled = stored.cancel_signaled;
-            release_lease_unlocked(worker_id, stored.leased_node);
+            cancel_signaled = stored_lease.cancel_signaled;
+            release_lease_unlocked(worker_id, stored_lease.leased_node);
             return true;
         }
 
@@ -1196,7 +1189,6 @@ class parallel_solver {
                 // Is this ensured? I am not sure.
                 if (!m.inc()) {
                     b.set_canceled();
-                    // b.notify_cv_waiters();
                     return;
                 }
 
@@ -1515,7 +1507,6 @@ class parallel_solver {
                     while (true) {
                         if (!m.inc()) {
                             b.set_canceled();
-                            // b.notify_cv_waiters();
                             return;
                         }
                         if (canceled())
@@ -1843,7 +1834,6 @@ class parallel_solver {
                     b.publish_minimized_core(m_l2g, asms, source, original_size, minimized);
             }
             b.set_canceled();
-            // b.notify_cv_waiters();
         }
 
         void cancel() {