diff options
| author | Pierre-Marie Pédrot | 2014-04-25 19:46:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-04-25 21:17:11 +0200 |
| commit | 8330f5cfd6a332df10fc806b0c0bdab6e0abe8e7 (patch) | |
| tree | 56ab646154a576454a1ee34ad1cc0a8c6e7a70fe /lib/workerPool.ml | |
| parent | 9e36fa1e7460d256a4f9f37571764f79050688e2 (diff) | |
Adding a stm/ folder, as asked during last workgroup. It was essentially moving
files around. A bunch of files from lib/ that were only used in the STM were
moved, as well as part of toplevel/ related to the STM.
Diffstat (limited to 'lib/workerPool.ml')
| -rw-r--r-- | lib/workerPool.ml | 73 |
1 files changed, 0 insertions, 73 deletions
diff --git a/lib/workerPool.ml b/lib/workerPool.ml deleted file mode 100644 index fcae4f20d6..0000000000 --- a/lib/workerPool.ml +++ /dev/null @@ -1,73 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -module Make(Worker : sig - type process - val spawn : - ?prefer_sock:bool -> ?env:string array -> string -> string array -> - process * in_channel * out_channel -end) = struct - -type worker_id = int -type spawn = - args:string array -> env:string array -> unit -> - in_channel * out_channel * Worker.process - -let slave_managers = ref None - -let n_workers () = match !slave_managers with - | None -> 0 - | Some managers -> Array.length managers -let is_empty () = !slave_managers = None - -let magic_no = 17 - -let master_handshake worker_id ic oc = - try - Marshal.to_channel oc magic_no []; flush oc; - let n = (Marshal.from_channel ic : int) in - if n <> magic_no then begin - Printf.eprintf "Handshake with %d failed: protocol mismatch\n" worker_id; - exit 1; - end - with e when Errors.noncritical e -> - Printf.eprintf "Handshake with %d failed: %s\n" - worker_id (Printexc.to_string e); - exit 1 - -let respawn n ~args ~env () = - let proc, ic, oc = Worker.spawn ~env Sys.argv.(0) args in - master_handshake n ic oc; - ic, oc, proc - -let init ~size:n ~manager:manage_slave = - slave_managers := Some - (Array.init n (fun x -> - let cancel = ref false in - cancel, Thread.create (manage_slave ~cancel (x+1)) (respawn (x+1)))) - -let cancel n = - match !slave_managers with - | None -> () - | Some a -> - let switch, _ = a.(n) in - switch := true - -let worker_handshake slave_ic slave_oc = - try - let v = (Marshal.from_channel slave_ic : int) in - if v <> magic_no then begin - prerr_endline "Handshake failed: protocol mismatch\n"; - exit 1; - end; - Marshal.to_channel slave_oc v []; flush slave_oc; - with e when Errors.noncritical e -> - prerr_endline ("Handshake failed: " ^ Printexc.to_string e); - exit 1 - -end |
