STM: new "par:" goal selector, like "all:" but in parallel

par: distributes the goals among a number of workers given
by -async-proofs-tac-j (defaults to 2).

1 files changed, 18 insertions, 1 deletions

diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index e4b9d382d..9d3553c36 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -42,23 +42,29 @@ type 'a t = {
   cond : Condition.t;
   mutable nwaiting : int;
   cond_waiting : Condition.t;
+  mutable release : bool;
 }
 
+exception BeingDestroyed
+
 let create () = {
   queue = PriorityQueue.create ();
   lock = Mutex.create ();
   cond = Condition.create ();
   nwaiting = 0;
   cond_waiting = Condition.create ();
+  release = false;
 }
 
 let pop ({ queue = q; lock = m; cond = c; cond_waiting = cn } as tq) =
+  if tq.release then raise BeingDestroyed;
   Mutex.lock m;
   while PriorityQueue.is_empty q do
     tq.nwaiting <- tq.nwaiting + 1;
     Condition.signal cn;
     Condition.wait c m;
     tq.nwaiting <- tq.nwaiting - 1;
+    if tq.release then (Mutex.unlock m; raise BeingDestroyed)
   done;
   let x = PriorityQueue.pop q in
   Condition.signal c;
@@ -66,7 +72,9 @@ let pop ({ queue = q; lock = m; cond = c; cond_waiting = cn } as tq) =
   Mutex.unlock m;
   x
 
-let push { queue = q; lock = m; cond = c } x =
+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");
   Mutex.lock m;
   PriorityQueue.push x q;
   Condition.signal c;
@@ -79,6 +87,15 @@ let clear { queue = q; lock = m; cond = c } =
 
 let is_empty { queue = q } = PriorityQueue.is_empty q
 
+let destroy tq =
+  tq.release <- true;
+  while tq.nwaiting > 0 do
+    Mutex.lock tq.lock;
+    Condition.signal tq.cond;
+    Mutex.unlock tq.lock;
+  done;
+  tq.release <- false
+
 let wait_until_n_are_waiting_and_queue_empty j tq =
   Mutex.lock tq.lock;
   while not (PriorityQueue.is_empty tq.queue) || tq.nwaiting < j do