Commit 5cc897ae authored by Andrei Paskevich's avatar Andrei Paskevich

remove OS-specific calls from Call_provers

parent 1c63f3d8
......@@ -204,17 +204,14 @@ let wait_terminate_unix () =
match jobserver with
| Makeproto.Sequential -> ()
| Makeproto.Parallel pipe ->
let rec reclaim_proc ((pid,_) as res_waitpid) =
let (cp,callback) = Hint.find called_provers pid in
let rec reclaim_proc (pid,ret) =
let (pc,callback) = Hint.find called_provers pid in
Hint.remove called_provers pid;
begin match Call_provers.query_call ~res_waitpid cp with
| None -> assert false
| Some res -> callback (res ()) end;
if not (Hint.is_empty called_provers)
then wait ()
callback (Call_provers.post_wait_call pc ret ());
if not (Hint.is_empty called_provers) then wait ()
and wait () =
Makeproto.release_worker pipe;
let res_waitpid = Call_provers.wait_all () in
let res_waitpid = Unix.wait () in
Makeproto.wait_worker pipe;
reclaim_proc res_waitpid
in
......
......@@ -118,9 +118,12 @@ let debug = Debug.register_info_flag "call_prover"
type res_waitpid = int * Unix.process_status
type post_prover_call = unit -> prover_result
type prover_call =
{ call: ?res_waitpid:res_waitpid -> Unix.wait_flag list -> post_prover_call;
pid: int}
type prover_call = {
call : Unix.process_status -> post_prover_call;
pid : int
}
type pre_prover_call = unit -> prover_call
let save f = f ^ ".save"
......@@ -168,13 +171,7 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
Unix.close fd_in;
close_out cout;
let call = fun ?res_waitpid wait_flags ->
(* TODO? check that we haven't given the result earlier *)
let res,ret =
match res_waitpid with
| Some ((res,_) as res_waitpid) when pid = res -> res_waitpid
| _ -> Unix.waitpid wait_flags pid in
if res = 0 then raise Exit;
let call = fun ret ->
let time = Unix.gettimeofday () -. time in
let cout = open_in fout in
let out = Sysutil.channel_contents cout in
......@@ -207,8 +204,9 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
{ pr_answer = ans;
pr_status = ret;
pr_output = out;
pr_time = time } in
{call = call; pid = pid}
pr_time = time }
in
{ call = call; pid = pid }
let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
~regexps ~timeregexps ~exitcodes ~filename
......@@ -224,17 +222,13 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
call_on_file ~command ~timelimit ~memlimit
~regexps ~timeregexps ~exitcodes ~cleanup:true ~inplace fin
let query_call ?res_waitpid call =
try Some (call.call ?res_waitpid [Unix.WNOHANG]) with Exit -> None
let wait_on_call ?res_waitpid call = call.call ?res_waitpid []
let query_call pc =
let pid, ret = Unix.waitpid [Unix.WNOHANG] pc.pid in
if pid = 0 then None else Some (pc.call ret)
let query_wait_all wait_flags =
let res,_ as res_waitpid = Unix.waitpid wait_flags 0 in
if res = 0 then raise Exit;
res_waitpid
let wait_on_call pc =
let _, ret = Unix.waitpid [] pc.pid in pc.call ret
let query_all () = try Some (query_wait_all [Unix.WNOHANG]) with Exit -> None
let wait_all () = query_wait_all []
let post_wait_call pc ret = pc.call ret
let prover_call_pid pc = pc.pid
......@@ -59,9 +59,6 @@ val timeregexp : string -> timeregexp
(** Converts a regular expression with special markers '%h','%m',
'%s','%i' (for milliseconds) into a value of type [timeregexp] *)
type res_waitpid = int * Unix.process_status
(** pid of a process that stopped and its status *)
type prover_call
(** Type that represents a single prover run *)
......@@ -115,24 +112,16 @@ val call_on_buffer :
@param filename : the suffix of the proof task's file, if the prover
doesn't accept stdin. *)
val query_call :
?res_waitpid:res_waitpid -> prover_call -> post_prover_call option
val query_call : prover_call -> post_prover_call option
(** Thread-safe non-blocking function that checks if the prover
has finished. *)
val wait_on_call :
?res_waitpid:res_waitpid -> prover_call -> post_prover_call
val wait_on_call : prover_call -> post_prover_call
(** Thread-safe blocking function that waits until the prover finishes. *)
val query_all : unit -> res_waitpid option
(** Just a wrapper around Unix.wait_pid with the same flag than query_call
Don't work on Win32
*)
val wait_all : unit -> res_waitpid
(** Just a wrapper around Unix.wait_pid with the same flag than wait_on_call
Don't work on Win32
*)
val post_wait_call : prover_call -> Unix.process_status -> post_prover_call
(** Thread-safe non-blocking function that should be called when the
prover's exit status was obtained from a prior call of Unix.waitpid *)
val prover_call_pid : prover_call -> int
(** return the pid of the prover *)
(** Return the pid of the prover *)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment