diff options
Diffstat (limited to 'stm/workerPool.mli')
| -rw-r--r-- | stm/workerPool.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/stm/workerPool.mli b/stm/workerPool.mli index d55b35c28..4e5512a4b 100644 --- a/stm/workerPool.mli +++ b/stm/workerPool.mli @@ -19,11 +19,15 @@ type spawn = in_channel * out_channel * Worker.process val init : - size:int -> manager:(cancel:bool ref -> worker_id -> spawn -> unit) -> + size:int -> + manager:(cancel:bool ref -> die:bool ref -> worker_id -> spawn -> unit) -> (int -> worker_id) -> unit +val destroy : unit -> unit + val is_empty : unit -> bool val n_workers : unit -> int val cancel : worker_id -> unit +val cancel_all : unit -> unit (* The worker should call this function *) val worker_handshake : in_channel -> out_channel -> unit |