Commit 8159c0d7 authored by Andrei Paskevich's avatar Andrei Paskevich

Call_provers: simplify API

Call_provers:

- drop closures "pre_prover_call" and "post_prover_call". They were
  intended to be used for synchronous interaction with provers from
  multiple threads. This is now responsibility of the proof server:
  (a) any Call_prover.call_on_[file|buffer] submits the proof task
      immediately to the server;
  (b) all proof results are handled in the working Why3 thread.

- Call_provers.query_call returns a tri-state "prover_update" type
  which can be one of: "ProverStarted" (returned after the proof
  server informs Why3 that a prover was started), "ProverFinished"
  (returned after the proof server returns the prover result), and
  "NoUpdates" (returned when the proof server has not sent any new
  updates concerning the proof task in question).

    IMPORTANT: query_call does not maintain the state of a given
  prover call. In a normal use case, "ProverFinished" is returned
  _exactly_ once, and "ProverStarted" _at_most_ once (never for
  an editor call or when rapidly overwritten by "ProverFinished").

    TODO: extend the proof server protocol and implementation to
  send "ProverStarted" events back to Why3.
parent 8445e30c
......@@ -96,7 +96,7 @@ let result1 : Call_provers.prover_result =
Call_provers.wait_on_call
(Driver.prove_task ~limit:Call_provers.empty_limit
~command:alt_ergo.Whyconf.command
alt_ergo_driver task1 ()) ()
alt_ergo_driver task1)
(* prints Alt-Ergo answer *)
let () = printf "@[On task 1, alt-ergo answers %a@."
......@@ -106,7 +106,7 @@ let result2 : Call_provers.prover_result =
Call_provers.wait_on_call
(Driver.prove_task ~command:alt_ergo.Whyconf.command
~limit:{Call_provers.empty_limit with Call_provers.limit_time = 10}
alt_ergo_driver task2 ()) ()
alt_ergo_driver task2)
let () = printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
Call_provers.print_prover_answer result1.Call_provers.pr_answer
......@@ -144,7 +144,7 @@ let result3 =
Call_provers.wait_on_call
(Driver.prove_task ~limit:Call_provers.empty_limit
~command:alt_ergo.Whyconf.command
alt_ergo_driver task3 ()) ()
alt_ergo_driver task3)
let () = printf "@[On task 3, alt-ergo answers %a@."
Call_provers.print_prover_result result3
......@@ -174,7 +174,7 @@ let result4 =
Call_provers.wait_on_call
(Driver.prove_task ~limit:Call_provers.empty_limit
~command:alt_ergo.Whyconf.command
alt_ergo_driver task4 ()) ()
alt_ergo_driver task4)
let () = printf "@[On task 4, alt-ergo answers %a@."
Call_provers.print_prover_result result4
......
......@@ -1308,8 +1308,8 @@ let why3tac ?(timelimit=timelimit) s gl =
if debug then Format.printf "@[%a@]@\n---@." (Driver.print_task drv) !task;
let limit =
{ Call_provers.empty_limit with Call_provers.limit_time = timelimit } in
let call = Driver.prove_task ~command ~limit drv !task () in
wait_on_call call ()
let call = Driver.prove_task ~command ~limit drv !task in
wait_on_call call
with
| NotFO ->
if debug then Printexc.print_backtrace stderr; flush stderr;
......
......@@ -311,18 +311,12 @@ let handle_answer answer =
let wait_for_server_result ~blocking =
List.map handle_answer (Prove_client.read_answers ~blocking)
type post_prover_call = unit -> prover_result
type prover_call =
| ServerCall of server_id
| EditorCall of (Unix.process_status -> post_prover_call) * int
type pre_prover_call = unit -> prover_call
let result_buffer : (server_id, prover_result) Hashtbl.t = Hashtbl.create 17
| EditorCall of int
let call_on_file ~command ~limit ~res_parser ~printer_mapping
?(inplace=false) fin () =
?(inplace=false) fin =
let id = gen_id () in
let cmd, use_stdin, on_timelimit =
actualcommand ~cleanup:true ~inplace command limit fin in
......@@ -341,30 +335,51 @@ let call_on_file ~command ~limit ~res_parser ~printer_mapping
~cmd;
ServerCall id
let get_new_results ~blocking =
List.iter (fun (id, r) -> Hashtbl.add result_buffer id r)
type prover_update =
| NoUpdates
| ProverStarted
| ProverFinished of prover_result
let result_buffer : (server_id, prover_update) Hashtbl.t = Hashtbl.create 17
let get_new_results ~blocking = (* TODO: handle ProverStarted events *)
List.iter (fun (id, r) -> Hashtbl.add result_buffer id (ProverFinished r))
(wait_for_server_result ~blocking)
let query_result_buffer id =
try let r = Hashtbl.find result_buffer id in
Hashtbl.remove result_buffer id; r
with Not_found -> NoUpdates
let editor_result ret = {
pr_answer = Unknown ("", None);
pr_status = ret;
pr_output = "";
pr_time = 0.0;
pr_steps = 0;
pr_model = Model_parser.default_model;
}
let query_call = function
| ServerCall id ->
begin try
get_new_results ~blocking:false;
Some (let r = Hashtbl.find result_buffer id in (fun () -> r))
with Not_found -> None end
| EditorCall (call, pid) ->
get_new_results ~blocking:false;
query_result_buffer id
| EditorCall pid ->
let pid, ret = Unix.waitpid [Unix.WNOHANG] pid in
if pid = 0 then None else Some (call ret)
if pid = 0 then NoUpdates else
ProverFinished (editor_result ret)
let rec wait_on_call = function
| ServerCall id as pc ->
begin try
let r = Hashtbl.find result_buffer id in (fun () -> r)
with Not_found ->
get_new_results ~blocking:true;
wait_on_call pc
begin match query_result_buffer id with
| ProverFinished r -> r
| _ ->
get_new_results ~blocking:true;
wait_on_call pc
end
| EditorCall (call, pid) ->
let _, ret = Unix.waitpid [] pid in call ret
| EditorCall pid ->
let _, ret = Unix.waitpid [] pid in
editor_result ret
let call_on_buffer ~command ~limit ~res_parser ~filename ~printer_mapping
?(inplace=false) buffer =
......@@ -385,20 +400,8 @@ let call_editor ~command fin =
Debug.dprintf debug "@[<hov 2>Call_provers: editor command is: %a@]@."
(Pp.print_list Pp.space pp_print_string) command;
let argarray = Array.of_list command in
fun () ->
let fd_in =
if use_stdin then Unix.openfile fin [Unix.O_RDONLY] 0 else Unix.stdin in
let pid = Unix.create_process exec argarray fd_in Unix.stdout Unix.stderr in
if use_stdin then Unix.close fd_in;
let call = fun ret ->
let r =
{ pr_answer = Unknown ("", None);
pr_status = ret;
pr_output = "";
pr_time = 0.0;
pr_steps = 0;
pr_model = Model_parser.default_model;
} in
(fun () -> r)
in
EditorCall (call, pid)
let fd_in =
if use_stdin then Unix.openfile fin [Unix.O_RDONLY] 0 else Unix.stdin in
let pid = Unix.create_process exec argarray fd_in Unix.stdout Unix.stderr in
if use_stdin then Unix.close fd_in;
EditorCall pid
......@@ -109,21 +109,15 @@ type prover_result_parser = {
*)
(** {2 Functions for calling external provers} *)
type prover_call
(** Type that represents a single prover run *)
type pre_prover_call = unit -> prover_call
(** Thread-safe closure that launches the prover *)
type post_prover_call = unit -> prover_result
(** Thread-unsafe closure that interprets the prover's results *)
type resource_limit =
{
limit_time : int;
limit_mem : int;
limit_steps : int;
}
type resource_limit = {
limit_time : int;
limit_mem : int;
limit_steps : int;
}
(* represents the three ways a prover run can be limited: in time, memory
and/or steps *)
......@@ -136,7 +130,7 @@ val limit_max : resource_limit -> resource_limit -> resource_limit
(* return the limit object whose components represent the maximum of the
corresponding components of the arguments *)
val call_editor : command : string -> string -> pre_prover_call
val call_editor : command : string -> string -> prover_call
val call_on_file :
command : string ->
......@@ -144,7 +138,7 @@ val call_on_file :
res_parser : prover_result_parser ->
printer_mapping : Printer.printer_mapping ->
?inplace : bool ->
string -> pre_prover_call
string -> prover_call
val call_on_buffer :
command : string ->
......@@ -153,7 +147,7 @@ val call_on_buffer :
filename : string ->
printer_mapping : Printer.printer_mapping ->
?inplace : bool ->
Buffer.t -> pre_prover_call
Buffer.t -> prover_call
(** Call a prover on the task printed in the {!type: Buffer.t} given.
@param limit : set the available time limit (def. 0 : unlimited), memory
......@@ -164,8 +158,14 @@ val call_on_buffer :
@param filename : the suffix of the proof task's file, if the prover
doesn't accept stdin. *)
val query_call : prover_call -> post_prover_call option
(** non-blocking function that checks if the prover has finished. *)
type prover_update =
| NoUpdates
| ProverStarted
| ProverFinished of prover_result
val query_call : prover_call -> prover_update
(** non-blocking function that reports any new updates
from the server related to a given prover call. *)
val wait_on_call : prover_call -> post_prover_call
val wait_on_call : prover_call -> prover_result
(** blocking function that waits until the prover finishes. *)
......@@ -40,7 +40,7 @@ val call_on_buffer :
?inplace : bool ->
filename : string ->
printer_mapping : Printer.printer_mapping ->
driver -> Buffer.t -> Call_provers.pre_prover_call
driver -> Buffer.t -> Call_provers.prover_call
val print_task :
......@@ -59,7 +59,7 @@ val prove_task :
?cntexample : bool ->
?old : string ->
?inplace : bool ->
driver -> Task.task -> Call_provers.pre_prover_call
driver -> Task.task -> Call_provers.prover_call
(** Split the previous function in two simpler functions *)
val prepare_task : cntexample:bool -> driver -> Task.task -> Task.task
......@@ -73,7 +73,7 @@ val prove_task_prepared :
limit : Call_provers.resource_limit ->
?old : string ->
?inplace : bool ->
driver -> Task.task -> Call_provers.pre_prover_call
driver -> Task.task -> Call_provers.prover_call
(** Traverse all metas from a driver *)
......
......@@ -100,9 +100,7 @@ type t =
mutable running_check : (unit -> bool) list;
(** proof attempt that wait some available action slot *)
proof_attempts_queue :
((proof_attempt_status -> unit) *
(unit -> Call_provers.prover_call))
Queue.t;
((proof_attempt_status -> unit) * Call_provers.prover_call) Queue.t;
(** timeout handler state *)
mutable timeout_handler_activated : bool;
mutable timeout_handler_running : bool;
......@@ -147,9 +145,10 @@ let timeout_handler t =
match c with
| Check_prover(callback,call) ->
(match Call_provers.query_call call with
| None -> c::acc
| Some post ->
let res = post () in callback (Done res);
| Call_provers.NoUpdates
| Call_provers.ProverStarted -> c::acc
| Call_provers.ProverFinished res ->
callback (Done res);
acc)
| Any_timeout callback ->
let b = callback () in
......@@ -160,10 +159,9 @@ let timeout_handler t =
let l =
if List.length l < t.maximum_running_proofs then
begin try
let (callback,pre_call) = Queue.pop t.proof_attempts_queue in
let (callback,call) = Queue.pop t.proof_attempts_queue in
callback Running;
Debug.dprintf debug "[Sched] proof attempts started@.";
let call = pre_call () in
(Check_prover(callback,call))::l
with Queue.Empty -> l
end
......@@ -216,11 +214,11 @@ let idle_handler t =
old,inplace,command,driver,callback,goal) ->
begin
try
let pre_call =
let call =
Driver.prove_task ?old ~cntexample ~inplace ~command
~limit driver goal
in
Queue.push (callback,pre_call) t.proof_attempts_queue;
Queue.push (callback,call) t.proof_attempts_queue;
run_timeout_handler t
with e when not (Debug.test_flag Debug.stack_trace) ->
Format.eprintf
......@@ -292,9 +290,9 @@ let schedule_proof_attempt ~cntexample ~limit ?old ~inplace
let schedule_edition t command filename callback =
Debug.dprintf debug "[Sched] Scheduling an edition@.";
let precall = Call_provers.call_editor ~command filename in
let call = Call_provers.call_editor ~command filename in
callback Running;
t.running_proofs <- (Check_prover(callback, precall ())) :: t.running_proofs;
t.running_proofs <- (Check_prover(callback, call)) :: t.running_proofs;
run_timeout_handler t
let schedule_delayed_action t callback =
......
......@@ -285,7 +285,7 @@ let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
| None, Some command ->
let call =
Driver.prove_task ~command ~limit ~cntexample:!opt_cntexmp drv task in
let res = Call_provers.wait_on_call (call ()) () in
let res = Call_provers.wait_on_call call in
printf "%s %s %s : %a@." fname tname
(task_goal task).Decl.pr_name.Ident.id_string
Call_provers.print_prover_result res
......
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