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

2 files changed, 12 insertions, 5 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");
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
index 5ee2cf99c..9cd651f4a 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -10,10 +10,11 @@
 
 type 'a t
 val create : unit -> 'a t
-val pop : ?picky:('a -> bool) -> 'a t -> 'a
+val pop : ?picky:('a -> bool) -> ?destroy:bool ref -> 'a t -> 'a
 val push : 'a t -> 'a -> unit
 val set_order : 'a t -> ('a -> 'a -> int) -> unit
 val wait_until_n_are_waiting_and_queue_empty : int -> 'a t -> unit
+val signal_destruction : 'a t -> unit
 
 (* Non destructive *)
 val wait_until_n_are_waiting_then_snapshot : int -> 'a t -> 'a list