diff options
| -rw-r--r-- | lib/spawn.ml | 31 | ||||
| -rw-r--r-- | lib/spawn.mli | 13 | ||||
| -rw-r--r-- | stm/asyncTaskQueue.ml | 25 | ||||
| -rw-r--r-- | stm/vi_checking.ml | 10 | ||||
| -rw-r--r-- | tools/fake_ide.ml | 4 |
5 files changed, 22 insertions, 61 deletions
diff --git a/lib/spawn.ml b/lib/spawn.ml index 802867e12..a8791ecb3 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -24,14 +24,11 @@ module type Control = sig val wait : handle -> Unix.process_status val unixpid : handle -> int val uid : handle -> string + val is_alive : handle -> bool - val kill_if : handle -> sec:int -> (unit -> bool) -> unit end -module type Timer = sig - - val add_timeout : sec:int -> (unit -> bool) -> unit -end +module type Empty = sig end module type MainLoopModel = sig type async_chan @@ -43,8 +40,6 @@ module type MainLoopModel = sig val read_all : async_chan -> string val async_chan_of_file : Unix.file_descr -> async_chan val async_chan_of_socket : Unix.file_descr -> async_chan - - include Timer end (* Common code *) @@ -164,6 +159,7 @@ type process = { type callback = ML.condition list -> read_all:(unit -> string) -> bool type handle = process +let is_alive p = p.alive let uid { pid; } = string_of_int pid let unixpid { pid; } = pid @@ -209,15 +205,6 @@ let stats { oob_req; oob_resp; alive } = flush oob_req; input_value oob_resp -let kill_if p ~sec test = - ML.add_timeout ~sec (fun () -> - if not p.alive then false - else if test () then begin - prerr_endline ("death condition for " ^ uid p ^ " is true"); - kill p; - false - end else true) - let rec wait p = try snd (Unix.waitpid [] p.pid) with @@ -226,7 +213,7 @@ let rec wait p = end -module Sync(T : Timer) = struct +module Sync(T : Empty) = struct type process = { cin : in_channel; @@ -244,6 +231,7 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ()) prog args = spawn_with_control prefer_sock env prog args in { cin; cout; pid; oob_resp; oob_req; alive = true }, cin, cout +let is_alive p = p.alive let uid { pid; } = string_of_int pid let unixpid { pid = pid; } = pid @@ -263,15 +251,6 @@ let stats { oob_req; oob_resp; alive } = flush oob_req; let RespStats g = input_value oob_resp in g -let kill_if p ~sec test = - T.add_timeout ~sec (fun () -> - if not p.alive then false - else if test () then begin - prerr_endline ("death condition for " ^ uid p ^ " is true"); - kill p; - false - end else true) - let wait { pid = unixpid } = try snd (Unix.waitpid [] unixpid) with Unix.Unix_error _ -> Unix.WEXITED 0o400 diff --git a/lib/spawn.mli b/lib/spawn.mli index 1554e0a1e..b4f615c89 100644 --- a/lib/spawn.mli +++ b/lib/spawn.mli @@ -30,16 +30,11 @@ module type Control = sig (* What is used in debug messages *) val uid : handle -> string - (* Installs a callback, called every [sec] seconds. If the returned value - * is true the process is killed *) - val kill_if : handle -> sec:int -> (unit -> bool) -> unit + val is_alive : handle -> bool end (* Abstraction to work with both threads and main loop models *) -module type Timer = sig - - val add_timeout : sec:int -> (unit -> bool) -> unit -end +module type Empty = sig end module type MainLoopModel = sig type async_chan @@ -51,8 +46,6 @@ module type MainLoopModel = sig val read_all : async_chan -> string val async_chan_of_file : Unix.file_descr -> async_chan val async_chan_of_socket : Unix.file_descr -> async_chan - - include Timer end (* spawn a process and read its output asynchronously *) @@ -71,7 +64,7 @@ module Async(ML : MainLoopModel) : sig end (* spawn a process and read its output synchronously *) -module Sync(T : Timer) : sig +module Sync(T : Empty) : sig type process val spawn : diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 917de9b52..0c40db4dc 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -108,15 +108,7 @@ module Make(T : Task) = struct let report_status ?(id = !Flags.async_proofs_worker_id) s = Pp.feedback ~state_id:Stateid.initial (Feedback.WorkerStatus(id, s)) - module Worker = Spawn.Sync(struct - let add_timeout ~sec f = - ignore(Thread.create (fun () -> - while true do - Unix.sleep sec; - if not (f ()) then Thread.exit () - done) - ()) - end) + module Worker = Spawn.Sync(struct end) module Model = struct @@ -181,10 +173,17 @@ module Make(T : Task) = struct CList.init 10 (fun _ -> Universes.new_univ_level (Global.current_dirpath ())) in - Worker.kill_if proc ~sec:1 (fun () -> - let stop = cancelled () || !(!expiration_date) in - if stop then (stop_waiting := true; TQueue.signal_destruction queue); - stop); + let rec kill_if () = + if not (Worker.is_alive proc) then () + else if cancelled () || !(!expiration_date) then + let () = stop_waiting := true in + let () = TQueue.signal_destruction queue in + Worker.kill proc + else + let () = Unix.sleep 1 in + kill_if () + in + let _ = Thread.create kill_if () in try while true do report_status ~id "Idle"; diff --git a/stm/vi_checking.ml b/stm/vi_checking.ml index cb6e60136..925a2a89e 100644 --- a/stm/vi_checking.ml +++ b/stm/vi_checking.ml @@ -14,15 +14,7 @@ let check_vi (ts,f) = Stm.set_compilation_hints long_f_dot_v; List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts -module Worker = Spawn.Sync(struct - let add_timeout ~sec f = - ignore(Thread.create (fun () -> - while true do - Unix.sleep sec; - if not (f ()) then Thread.exit () - done) - ()) -end) +module Worker = Spawn.Sync(struct end) module IntOT = struct type t = int diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index df114d059..47782db08 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -289,9 +289,7 @@ let usage () = (Filename.basename Sys.argv.(0)) (Parser.print grammar)) -module Coqide = Spawn.Sync(struct - let add_timeout ~sec:_ _ = () -end) +module Coqide = Spawn.Sync(struct end) let main = Sys.set_signal Sys.sigpipe |