TQueue: a way to unblock threads begin destroyed waiting on pop

1 files changed, 10 insertions, 4 deletions

diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index 00213b8a2..834f93681 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -60,24 +60,30 @@ let create () = {
   release = false;
 }
 
-let pop ?(picky=(fun _ -> true))
+let pop ?(picky=(fun _ -> true)) ?(destroy=ref false)
   ({ queue = q; lock = m; cond = c; cond_waiting = cn } as tq)
 =
-  if tq.release then raise BeingDestroyed;
   Mutex.lock m;
-  while not (PriorityQueue.exists picky q) do
+  if tq.release then (Mutex.unlock m; raise BeingDestroyed);
+  while not (PriorityQueue.exists picky q || !destroy) do
     tq.nwaiting <- tq.nwaiting + 1;
     Condition.broadcast cn;
     Condition.wait c m;
     tq.nwaiting <- tq.nwaiting - 1;
-    if tq.release then (Mutex.unlock m; raise BeingDestroyed)
+    if tq.release || !destroy then (Mutex.unlock m; raise BeingDestroyed)
   done;
+  if !destroy then (Mutex.unlock m; raise BeingDestroyed);
   let x = PriorityQueue.pop ~picky q in
   Condition.signal c;
   Condition.signal cn;
   Mutex.unlock m;
   x
 
+let signal_destruction { lock = m; cond = c } =
+  Mutex.lock m;
+  Condition.broadcast c;
+  Mutex.unlock m
+
 let push { queue = q; lock = m; cond = c; release } x =
   if release then Errors.anomaly(Pp.str
     "TQueue.push while being destroyed! Only 1 producer/destroyer allowed");