From 7dba9d3f3ce62246b9d8562d2818c63ba37b206e Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 21 Jul 2014 10:03:04 +0200
Subject: 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).
---
 stm/asyncTaskQueue.mli | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'stm/asyncTaskQueue.mli')

diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index e01479d30b..ddbb28457d 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -18,8 +18,8 @@ module type Task = sig
   val extra_env : unit -> string array
 
   (* run by the master, on a thread *)
-  val request_of_task : task -> request option
-  val use_response : task -> response -> [ `Die | `Stay | `StayReset ]
+  val request_of_task : [ `Fresh | `Old ] -> task -> request option
+  val use_response : task -> response -> [ `Stay | `StayReset ]
   val on_marshal_error : string -> task -> unit
   val on_slave_death : task option -> [ `Exit of int | `Stay ]
   val on_task_cancellation_or_expiration : task option -> unit
@@ -40,6 +40,10 @@ module Make(T : Task) : sig
 
   (* Number of workers, 0 = lazy local *)
   val init : int -> unit
+  val destroy : unit -> unit
+
+  val with_n_workers :
+    int -> (join:(unit -> unit) -> cancel_all:(unit -> unit) -> 'a) -> 'a
 
   val n_workers : unit -> int
 
@@ -47,6 +51,7 @@ module Make(T : Task) : sig
 
   (* blocking function that waits for the task queue to be empty *)
   val join : unit -> unit
+  val cancel_all : unit -> unit
 
   (* slave process main loop *)
   val slave_main_loop : (unit -> unit) -> unit
@@ -54,7 +59,7 @@ module Make(T : Task) : sig
   
   val cancel_worker : string -> unit
 
-  val reorder_tasks : (T.task -> T.task -> int) -> unit
+  val set_order : (T.task -> T.task -> int) -> unit
 
   val dump : unit -> T.task list
 
-- 
cgit v1.2.3