diff options
Diffstat (limited to 'stm/spawned.ml')
-rw-r--r-- | stm/spawned.ml | 86 |
1 files changed, 86 insertions, 0 deletions
diff --git a/stm/spawned.ml b/stm/spawned.ml new file mode 100644 index 00000000..18159288 --- /dev/null +++ b/stm/spawned.ml @@ -0,0 +1,86 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +open Spawn + +let pr_err s = Printf.eprintf "(Spawned,%d) %s\n%!" (Unix.getpid ()) s +let prerr_endline s = if !Flags.debug then begin pr_err s end else () + +type chandescr = AnonPipe | Socket of string * int + +let handshake cin cout = + try + match input_value cin with + | Hello(v, pid) when v = proto_version -> + prerr_endline (Printf.sprintf "Handshake with %d OK" pid); + output_value cout (Hello (proto_version,Unix.getpid ())); flush cout + | _ -> raise (Failure "handshake protocol") + with + | Failure s | Invalid_argument s | Sys_error s -> + pr_err ("Handshake failed: " ^ s); raise (Failure "handshake") + | End_of_file -> + pr_err "Handshake failed: End_of_file"; raise (Failure "handshake") + +let open_bin_connection h p = + let open Unix in + let cin, cout = open_connection (ADDR_INET (inet_addr_of_string h,p)) in + set_binary_mode_in cin true; + set_binary_mode_out cout true; + let cin = CThread.prepare_in_channel_for_thread_friendly_io cin in + cin, cout + +let controller h p = + prerr_endline "starting controller thread"; + let main () = + let ic, oc = open_bin_connection h p in + let rec loop () = + try + match CThread.thread_friendly_input_value ic with + | Hello _ -> prerr_endline "internal protocol error"; exit 1 + | ReqDie -> prerr_endline "death sentence received"; exit 0 + | ReqStats -> + output_value oc (RespStats (Gc.quick_stat ())); flush oc; loop () + with + | e -> + prerr_endline ("control channel broken: " ^ Printexc.to_string e); + exit 1 in + loop () in + ignore(Thread.create main ()) + +let main_channel = ref None +let control_channel = ref None + +let channels = ref None + +let init_channels () = + if !channels <> None then Errors.anomaly(Pp.str "init_channels called twice"); + let () = match !main_channel with + | None -> () + | Some (Socket(mh,mp)) -> + channels := Some (open_bin_connection mh mp); + | Some AnonPipe -> + let stdin = Unix.in_channel_of_descr (Unix.dup Unix.stdin) in + let stdout = Unix.out_channel_of_descr (Unix.dup Unix.stdout) in + Unix.dup2 Unix.stderr Unix.stdout; + set_binary_mode_in stdin true; + set_binary_mode_out stdout true; + let stdin = CThread.prepare_in_channel_for_thread_friendly_io stdin in + channels := Some (stdin, stdout); + in + match !control_channel with + | None -> () + | Some (Socket (ch, cp)) -> + controller ch cp + | Some AnonPipe -> + Errors.anomaly (Pp.str "control channel cannot be a pipe") + +let get_channels () = + match !channels with + | None -> Errors.anomaly(Pp.str "init_channels not called") + | Some(ic, oc) -> ic, oc + |