Commit 11aec6e2 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

remove Dbsync and Scheduler

parent 63c6f2c6
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Why
type prover_id = Db.prover_id
module Hprover = Db.Hprover
type transf_id = Db.transf_id
module Htransf = Db.Htransf
type file = Db.file
type theory = Db.theory
type goal = Db.goal
type proof_attempt = Db.proof_attempt
type transf = Db.transf
type proof_status = Db.proof_status
let m = Mutex.create ()
let mutex1 fn a1 =
Mutex.lock m;
try let res = fn a1 in Mutex.unlock m; res
with e -> Mutex.unlock m ; raise e
let mutex2 fn a1 a2 =
Mutex.lock m;
try let res = fn a1 a2 in Mutex.unlock m; res
with e -> Mutex.unlock m ; raise e
let mutex3 fn a1 a2 a3 =
Mutex.lock m;
try let res = fn a1 a2 a3 in Mutex.unlock m; res
with e -> Mutex.unlock m ; raise e
let prover_name pid = mutex1 Db.prover_name pid
let transf_name tid = mutex1 Db.transf_name tid
let status_and_time pa = mutex1 Db.status_and_time pa
let edited_as pa = mutex1 Db.edited_as pa
let goal_name g = mutex1 Db.goal_name g
let task_checksum g = mutex1 Db.task_checksum g
let external_proofs g = mutex1 Db.external_proofs g
let transformations g = mutex1 Db.transformations g
let subgoals tr = mutex1 Db.subgoals tr
let theory_name th = mutex1 Db.theory_name th
let goals th = mutex1 Db.goals th
let theories f = mutex1 Db.theories f
let init_base s = mutex1 Db.init_base s
let is_initialized u = mutex1 Db.is_initialized u
let db_name u = mutex1 Db.db_name u
let files u = mutex1 Db.files u
exception AlreadyExist
let prover_from_name s = mutex1 Db.prover_from_name s
let transf_from_name s = mutex1 Db.transf_from_name s
let add_proof_attempt g pid = mutex2 Db.add_proof_attempt g pid
let remove_proof_attempt pa = mutex1 Db.remove_proof_attempt pa
let set_obsolete pa = mutex1 Db.set_obsolete pa
let set_status pa ps t = mutex3 Db.set_status pa ps t
let set_edited_as pa s = mutex2 Db.set_edited_as pa s
let add_transformation g tid = mutex2 Db.add_transformation g tid
let remove_transformation tr = mutex1 Db.remove_transformation tr
let add_goal th s1 s2 = mutex3 Db.add_goal th s1 s2
let change_checksum g s = mutex2 Db.change_checksum g s
let add_subgoal tr s1 s2 = mutex3 Db.add_subgoal tr s1 s2
let add_theory f s = mutex2 Db.add_theory f s
let add_file s = mutex1 Db.add_file s
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Why
type prover_id = Db.prover_id
type transf_id = Db.transf_id
type file = Db.file
type theory = Db.theory
type goal = Db.goal
type proof_attempt = Db.proof_attempt
type transf = Db.transf
type proof_status = Db.proof_status
val prover_name : prover_id -> string
val transf_name : transf_id -> string
val status_and_time : proof_attempt -> proof_status * float * bool * string
val edited_as : proof_attempt -> string
val goal_name : goal -> string
val task_checksum : goal -> string (** checksum *)
val external_proofs: goal -> proof_attempt Db.Hprover.t
val transformations : goal -> transf Db.Htransf.t
val subgoals : transf -> goal Util.Mstr.t
val theory_name : theory -> string
val goals : theory -> goal Util.Mstr.t
val theories : file -> theory Util.Mstr.t
val init_base : string -> unit
val is_initialized : unit -> bool
val db_name : unit -> string
val files : unit -> (file * string) list
exception AlreadyExist
val prover_from_name : string -> prover_id
val transf_from_name : string -> transf_id
val add_proof_attempt : goal -> prover_id -> proof_attempt
val remove_proof_attempt : proof_attempt -> unit
val set_obsolete : proof_attempt -> unit
val set_status : proof_attempt -> proof_status -> float -> unit
val set_edited_as : proof_attempt -> string -> unit
val add_transformation : goal -> transf_id -> transf
val remove_transformation : transf -> unit
val add_goal : theory -> string -> string -> goal
val change_checksum: goal -> string -> unit
val add_subgoal : transf -> string -> string -> goal
val add_theory : file -> string -> theory
val add_file : string -> file
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Format
open Why
open Worker
(** max scheduled proofs / max running proofs *)
let coef_buf = 1
let async = ref (fun f () -> f ())
let debug = Debug.register_flag "scheduler"
type proof_attempt_status =
| Scheduled (** external proof attempt is scheduled *)
| Running (** external proof attempt is in progress *)
| Done of Call_provers.prover_result (** external proof done *)
| InternalFailure of exn (** external proof aborted by internal error *)
let print_pas fmt = function
| Scheduled -> fprintf fmt "Scheduled"
| Running -> fprintf fmt "Running"
| InternalFailure exn ->
fprintf fmt "InternalFailure %a" Exn_printer.exn_printer exn
| Done pr -> Call_provers.print_prover_result fmt pr
(**** queues of events to process ****)
type callback = proof_attempt_status -> unit
type attempt = bool * int * int * in_channel option * string * Driver.driver *
callback * Task.task
(* queue of external proof attempts *)
let prover_attempts_queue : attempt Queue.t = Queue.create ()
(* queue of proof editing tasks *)
let proof_edition_queue : (bool * string * string * Driver.driver *
(unit -> unit) * Task.task) Queue.t = Queue.create ()
type ('a,'b) doable = { callback : 'b -> unit;
argument : 'a;
funct : 'a -> 'b }
type exists_doable = { exists : 'a 'b. ('a,'b) doable -> unit }
type job =
| TaskL of (Task.task list -> unit) * Task.task list Trans.trans * Task.task
| Task of (Task.task -> unit) * Task.task Trans.trans * Task.task
| Do of (exists_doable -> unit)
(* queue of transformations *)
let transf_queue : job Queue.t = Queue.create ()
type answer =
| Prover_answer of callback * (unit -> Call_provers.prover_result)
| Editor_exited of (unit -> unit)
(* queue of prover answers *)
let answers_queue : answer Queue.t = Queue.create ()
(* number of scheduled external proofs *)
let scheduled_proofs = ref 0
let maximum_running_proofs = ref 2
(* they are protected by a lock *)
let queue_lock = Mutex.create ()
let queue_condition = Condition.create ()
(* number of running external proofs *)
let running_proofs = ref 0
(* it is protected by a lock *)
let running_lock = Mutex.create ()
let running_condition = Condition.create ()
let print_debug_nb_running () =
Debug.dprintf debug
"scheduled_proofs = %i; running_proofs = %i;@."
!scheduled_proofs !running_proofs
(***** handler of events *****)
(*** collect answers from provers or editors *)
let collect_answers () =
match Queue.pop answers_queue with
| Prover_answer (callback,r) ->
Mutex.unlock queue_lock;
let res = r () in
(*
eprintf
"[Why thread] Scheduler.event_handler: got prover answer@.";
*)
(* call GUI callback with argument [res] *)
!async (fun () -> callback (Done res)) ()
| Editor_exited callback ->
Mutex.unlock queue_lock;
!async callback ()
(**** apply transformations *)
let apply_transform () =
let k = Queue.pop transf_queue in
Mutex.unlock queue_lock;
Thread.yield ();
match k with
| TaskL (cb, tf, task) ->
let subtasks : Task.task list = Trans.apply tf task in
!async (fun () -> cb subtasks) ()
| Task (cb,tf, task) ->
let task = Trans.apply tf task in
!async (fun () -> cb task) ()
| Do e ->
let f d =
let r = d.funct d.argument in
!async (fun () -> d.callback r) () in
e {exists = f}
(**** edit proofs *)
let edit_proof () =
let (_debug,editor,file,driver,callback,goal) =
Queue.pop proof_edition_queue in
Mutex.unlock queue_lock;
let old =
if Sys.file_exists file
then
begin
let backup = file ^ ".bak" in
Sys.rename file backup;
Some(open_in backup)
end
else None
in
let ch = open_out file in
let fmt = formatter_of_out_channel ch in
Driver.print_task ?old driver fmt goal;
Util.option_iter close_in old;
close_out ch;
let (_ : Thread.t) = Thread.create
(fun () ->
let _ = Sys.command(editor ^ " " ^ file) in
Mutex.lock queue_lock;
Queue.push (Editor_exited callback) answers_queue ;
Condition.signal queue_condition;
Mutex.unlock queue_lock)
()
in ()
(* start new external proof attempt *)
(* since answers_queue and transf_queue are empty,
we are sure that both
prover_attempts_queue is non empty and
scheduled_proofs < maximum_running_proofs * coef_buf
*)
let new_external_proof =
let run_external (call_prover,callback) =
Mutex.lock queue_lock;
decr scheduled_proofs;
incr running_proofs;
print_debug_nb_running ();
Condition.signal queue_condition;
Mutex.unlock queue_lock;
!async (fun () -> callback Running) ();
let r = call_prover () in
Mutex.lock queue_lock;
decr running_proofs;
print_debug_nb_running ();
Queue.push (Prover_answer (callback,r)) answers_queue ;
Condition.signal queue_condition;
Mutex.unlock queue_lock in
let external_workers =
ManyWorkers.create maximum_running_proofs run_external in
fun () ->
if !scheduled_proofs >= !maximum_running_proofs * coef_buf
then raise Queue.Empty;
let (_debug,timelimit,memlimit,old,command,driver,callback,goal) =
Queue.pop prover_attempts_queue
in
incr scheduled_proofs;
print_debug_nb_running ();
Debug.dprintf debug
"%a is sent to driver;@."
(fun fmt g -> Pretty.print_pr fmt (Task.task_goal g)) goal;
Mutex.unlock queue_lock;
Thread.yield ();
(* build the prover task from goal in [a] *)
try
let call_prover : unit -> unit -> Call_provers.prover_result =
(*
if debug then
Format.eprintf "Task for prover: %a@."
(Driver.print_task driver) goal;
*)
let pre_call =
Driver.prove_task ?old ~command ~timelimit ~memlimit driver goal
in
fun () -> Call_provers.wait_on_call (pre_call ())
in
ManyWorkers.add_work external_workers (call_prover,callback);
with
| e ->
eprintf "%a@." Exn_printer.exn_printer e;
Mutex.lock queue_lock;
decr scheduled_proofs;
Mutex.unlock queue_lock;
!async (fun () -> callback (InternalFailure e)) ()
type priority = (unit -> unit) list
let interactive : priority = [collect_answers;
apply_transform;
edit_proof;
new_external_proof]
let intensive : priority = [collect_answers;
new_external_proof;
apply_transform]
let priority = ref interactive
let set_priority = (:=) priority
let event_handler () =
Mutex.lock queue_lock;
while
Queue.is_empty transf_queue &&
Queue.is_empty answers_queue &&
Queue.is_empty proof_edition_queue &&
(Queue.is_empty prover_attempts_queue ||
!scheduled_proofs >= !maximum_running_proofs * coef_buf)
do
Condition.wait queue_condition queue_lock
done;
let rec try_all = function
| [] ->
eprintf "Scheduler.event_handler: unexpected empty queues@.";
assert false
| f::l -> try f () with Queue.Empty -> try_all l in
try_all !priority
(***** start of the scheduler thread ****)
let (_scheduler_thread : Thread.t) =
Thread.create
(fun () ->
try
(* loop forever *)
while true do
event_handler ()
done;
assert false
with
e ->
eprintf "Scheduler thread stopped unexpectedly : %a@."
Exn_printer.exn_printer e;
raise e)
()
(***** to be called from GUI ****)
let schedule_proof_attempt ~debug ~timelimit ~memlimit ?old
~command ~driver ~callback
goal =
!async (fun () -> callback Scheduled) ();
Mutex.lock queue_lock;
Queue.push (debug,timelimit,memlimit,old,command,driver,callback,goal)
prover_attempts_queue;
Condition.signal queue_condition;
Mutex.unlock queue_lock
let create_proof_attempt ~debug ~timelimit ~memlimit ?old
~command ~driver ~callback
goal =
(debug,timelimit,memlimit,old,command,driver,callback,goal)
let transfer_proof_attempts q =
Queue.iter (fun (_,_,_,_,_,_,callback,_) ->
!async (fun () -> callback Scheduled) ()) q;
Mutex.lock queue_lock;
Queue.transfer q prover_attempts_queue;
Condition.signal queue_condition;
Mutex.unlock queue_lock
let schedule_some_proof_attempts ~debug ~timelimit ~memlimit ?old
~command ~driver ~callback
goal q =
Queue.add
(debug,timelimit,memlimit,old,command,driver,callback,goal) q;
if Queue.length q >= !maximum_running_proofs * coef_buf * 2 then
transfer_proof_attempts q
let edit_proof ~debug ~editor ~file ~driver ~callback goal =
Mutex.lock queue_lock;
Queue.push (debug,editor,file,driver,callback,goal) proof_edition_queue;
Condition.signal queue_condition;
Mutex.unlock queue_lock
let apply_transformation ~callback transf goal =
Mutex.lock queue_lock;
Queue.push (Task (callback,transf,goal)) transf_queue;
Condition.signal queue_condition;
Mutex.unlock queue_lock
let apply_transformation_l ~callback transf goal =
Mutex.lock queue_lock;
Queue.push (TaskL (callback,transf,goal)) transf_queue;
Condition.signal queue_condition;
Mutex.unlock queue_lock
let do_why ~callback funct argument =
let doable = { callback = callback;
argument = argument;
funct = funct } in
let exists f = f.exists doable in
Mutex.lock queue_lock;
Queue.push (Do exists) transf_queue;
Condition.signal queue_condition;
Mutex.unlock queue_lock
(* TODO : understand Thread.Event *)
let do_why_sync funct argument =
let m = Mutex.create () in
let c = Condition.create () in
let r = ref None in
let cb res =
Mutex.lock m; r := Some res; Condition.signal c; Mutex.unlock m in
do_why ~callback:cb funct argument;
Mutex.lock m; while !r = None do Condition.wait c m done;
Util.of_option !r
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Why
val async: ((unit->unit)->unit->unit) ref
(** async f () should call [f ()] asynchronously, in a suitable way
for the current user interface (e.g. GtkThread.async) *)
val maximum_running_proofs: int ref
(** bound on the number of prover processes running in parallel.
default is 2 *)
val debug : Debug.flag
type proof_attempt_status =
| Scheduled (** external proof attempt is scheduled *)
| Running (** external proof attempt is in progress *)
| Done of Call_provers.prover_result (** external proof done *)
| InternalFailure of exn (** external proof aborted by internal error *)
val print_pas : Format.formatter -> proof_attempt_status -> unit
val schedule_proof_attempt :
debug:bool -> timelimit:int -> memlimit:int ->
?old:in_channel ->
command:string -> driver:Driver.driver ->
callback:(proof_attempt_status -> unit) ->
Task.task (* Db.goal *) -> unit
(** schedules an attempt to prove goal with the given prover. This
function just prepares the goal for the proof attempt, and puts
it in the queue of waiting proof attempts, associated with its
callback.
The callback is called each time the status of that proves
changes, typically from Scheduled, then Running, then Success or
Timeout or Failure.
@param timelimit CPU time limit given for that attempt, in
seconds, must be positive. (unlimited attempts are not allowed
with this function)
@param memlimit memory limit given for that attempt, must be
positive. If not given, does not limit memory consumption
@raise AlreadyAttempted if there already exists a non-obsolete
external proof attempt with the same prover and time limit, or
with a lower or equal time limit and a result different from Timeout
*)
type attempt
val create_proof_attempt : debug:bool -> timelimit:int -> memlimit:int ->
?old:in_channel ->
command:string -> driver:Driver.driver ->
callback:(proof_attempt_status -> unit) ->
Task.task -> attempt
val transfer_proof_attempts : attempt Queue.t -> unit
(** same as the iteration of {!schedule_proof_attempt}.
The given queue is cleared. *)
val schedule_some_proof_attempts :
debug:bool -> timelimit:int -> memlimit:int ->
?old:in_channel ->
command:string -> driver:Driver.driver ->
callback:(proof_attempt_status -> unit) ->
Task.task -> attempt Queue.t -> unit
(** a middle between schedule_proof_attempts and
transfer_proof_attempts, use an heuristics to send sometimes the
proof_attemps. dont forget to use transfer_proof_attempts at the
end in order to flush the queue.
*)
val apply_transformation :
callback:(Why.Task.task -> unit) ->
Why.Task.task Trans.trans -> Task.task -> unit
val apply_transformation_l :
callback:(Why.Task.task list -> unit) ->
Why.Task.task list Trans.trans -> Task.task -> unit
val do_why : callback:('b -> unit) -> ('a -> 'b) -> 'a -> unit
(** use do why for all the function which deals with creating why value *)
val do_why_sync : ('a -> 'b) -> 'a -> 'b
val edit_proof :
debug:bool ->