diff options
Diffstat (limited to 'stm/workerPool.mli')
-rw-r--r-- | stm/workerPool.mli | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/stm/workerPool.mli b/stm/workerPool.mli new file mode 100644 index 00000000..f46303b5 --- /dev/null +++ b/stm/workerPool.mli @@ -0,0 +1,46 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type worker_id = string + +type 'a cpanel = { + exit : unit -> unit; (* called by manager to exit instead of Thread.exit *) + cancelled : unit -> bool; (* manager checks for a request of termination *) + extra : 'a; (* extra stuff to pass to the manager *) +} + +module type PoolModel = sig + (* this shall come from a Spawn.* model *) + type process + val spawn : int -> worker_id * process * CThread.thread_ic * out_channel + + (* this defines the main loop of the manager *) + type extra + val manager : + extra cpanel -> worker_id * process * CThread.thread_ic * out_channel -> unit +end + +module Make(Model : PoolModel) : sig + + type pool + + val create : Model.extra -> size:int -> pool + + val is_empty : pool -> bool + val n_workers : pool -> int + + (* cancel signal *) + val cancel : worker_id -> pool -> unit + val cancel_all : pool -> unit + (* camcel signal + true removal, the pool is empty afterward *) + val destroy : pool -> unit + + (* The worker should call this function *) + val worker_handshake : CThread.thread_ic -> out_channel -> unit + +end |