Commit 44f9a679 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

scheduler

parent a8bf97d6
...@@ -1073,7 +1073,7 @@ let root_goals () = ...@@ -1073,7 +1073,7 @@ let root_goals () =
exception AlreadyAttempted exception AlreadyAttempted
let try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver let try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver
(g : goal) : unit -> unit = (g : goal) : unit -> proof_attempt_status =
let db = current () in let db = current () in
let attempt = let attempt =
try try
...@@ -1132,16 +1132,20 @@ let try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver ...@@ -1132,16 +1132,20 @@ let try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver
g.proved <- true; g.proved <- true;
Goal.set_proved db g true; Goal.set_proved db g true;
(* TODO: update "proved" status of goal parents if any *) (* TODO: update "proved" status of goal parents if any *)
() Success
| Why.Call_provers.Timeout -> | Why.Call_provers.Timeout ->
External_proof.set_status db attempt Timeout External_proof.set_status db attempt Timeout;
Timeout
| Why.Call_provers.Invalid | Why.Call_provers.Unknown _ -> | Why.Call_provers.Invalid | Why.Call_provers.Unknown _ ->
External_proof.set_status db attempt Unknown External_proof.set_status db attempt Unknown;
Unknown
| Why.Call_provers.Failure _ | Why.Call_provers.HighFailure -> | Why.Call_provers.Failure _ | Why.Call_provers.HighFailure ->
External_proof.set_status db attempt HighFailure External_proof.set_status db attempt HighFailure;
HighFailure
with Exit -> with Exit ->
if debug then Format.eprintf "prover callback aborted because of an exception raised during elaboration@."; if debug then Format.eprintf "prover callback aborted because of an exception raised during elaboration@.";
External_proof.set_status db attempt HighFailure External_proof.set_status db attempt HighFailure;
HighFailure
......
...@@ -150,7 +150,8 @@ exception AlreadyAttempted ...@@ -150,7 +150,8 @@ exception AlreadyAttempted
val try_prover : val try_prover :
debug:bool -> timelimit:int -> memlimit:int -> prover:prover -> debug:bool -> timelimit:int -> memlimit:int -> prover:prover ->
command:string -> driver:Driver.driver -> goal -> (unit -> unit) command:string -> driver:Driver.driver -> goal ->
(unit -> proof_attempt_status)
(** attempts to prove goal with the given prover. This function (** attempts to prove goal with the given prover. This function
prepares the goal for that prover, adds it as an new prepares the goal for that prover, adds it as an new
external_proof attempt, setting its current status to Scheduled, external_proof attempt, setting its current status to Scheduled,
...@@ -158,8 +159,9 @@ val try_prover : ...@@ -158,8 +159,9 @@ val try_prover :
actually sets the status to running, launches the prover, and actually sets the status to running, launches the prover, and
waits for its termination. Upon termination of the external waits for its termination. Upon termination of the external
process, the prover's answer is retrieved and database is process, the prover's answer is retrieved and database is
updated. The [proved] field of the database is updated, and also updated, that is the [proved] field of the database is updated,
these of any goal affected, according to invariant above. and also these of any goal affected, according to invariant
above. The prover result is also returned.
Although goal preparation is not re-entrant, the function Although goal preparation is not re-entrant, the function
returned initially is re-entrant, thus is suitable for being executed returned initially is re-entrant, thus is suitable for being executed
......
...@@ -14,7 +14,7 @@ let schedule_proof_attempt ~debug ~timelimit ~memlimit ~prover ...@@ -14,7 +14,7 @@ let schedule_proof_attempt ~debug ~timelimit ~memlimit ~prover
goal = goal =
let prepare_goal = let prepare_goal =
try try
Db.try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver goal Db.try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver goal;
with Db.AlreadyAttempted -> with Db.AlreadyAttempted ->
raise Exit raise Exit
in in
...@@ -27,14 +27,16 @@ let schedule_proof_attempt ~debug ~timelimit ~memlimit ~prover ...@@ -27,14 +27,16 @@ let schedule_proof_attempt ~debug ~timelimit ~memlimit ~prover
(* lock and store the attempt into the queue *) (* lock and store the attempt into the queue *)
Mutex.lock queue_lock; Mutex.lock queue_lock;
Queue.push (prepare_goal,callback) attempts; Queue.push (prepare_goal,callback) attempts;
callback Db.Scheduled;
(* try to run attempt if resource available *) (* try to run attempt if resource available *)
while !running_proofs < !maximum_running_proofs do while !running_proofs < !maximum_running_proofs do
let call,callback = Queue.pop attempts in let call,callback = Queue.pop attempts in
incr running_proofs; incr running_proofs;
Mutex.unlock queue_lock; Mutex.unlock queue_lock;
(* END LOCKED SECTION *) (* END LOCKED SECTION *)
call (); callback Db.Running;
callback (); let res = call () in
callback res;
(* BEGIN LOCKED SECTION *) (* BEGIN LOCKED SECTION *)
Mutex.lock queue_lock; Mutex.lock queue_lock;
decr running_proofs; decr running_proofs;
......
...@@ -23,7 +23,7 @@ open Why ...@@ -23,7 +23,7 @@ open Why
val schedule_proof_attempt : val schedule_proof_attempt :
debug:bool -> timelimit:int -> memlimit:int -> prover:Db.prover -> debug:bool -> timelimit:int -> memlimit:int -> prover:Db.prover ->
command:string -> driver:Driver.driver -> command:string -> driver:Driver.driver ->
callback:(unit -> unit) -> Db.goal -> unit callback:(Db.proof_attempt_status -> unit) -> Db.goal -> unit
(** schedules an attempt to prove goal with the given prover. This (** schedules an attempt to prove goal with the given prover. This
function just prepares the goal for the proof attempt, and put function just prepares the goal for the proof attempt, and put
it in the queue of waiting proofs attempts, associated with its it in the queue of waiting proofs attempts, associated with its
......
...@@ -178,6 +178,8 @@ let do_theory tname th glist = ...@@ -178,6 +178,8 @@ let do_theory tname th glist =
(* A good-old text-based interface *) (* A good-old text-based interface *)
(***********************************) (***********************************)
let count = ref 0
let goal_menu g = let goal_menu g =
try try
while true do while true do
...@@ -206,11 +208,14 @@ let goal_menu g = ...@@ -206,11 +208,14 @@ let goal_menu g =
raise Exit raise Exit
**) **)
(* this is for calling the scheduler *) (* this is for calling the scheduler *)
let callback () = incr count;
printf "Scheduled goal is finished, you should update@." let c = !count in
printf "Scheduling task #%d@." c;
let callback result =
printf "Scheduled task #%d: status set to %a, you should update the view@." c Db.print_status result
in in
Scheduler.schedule_proof_attempt Scheduler.schedule_proof_attempt
~debug:true ~timelimit ~memlimit:0 ~debug:false ~timelimit ~memlimit:0
~prover:p.prover ~command:p.command ~driver:p.driver ~prover:p.prover ~command:p.command ~driver:p.driver
~callback ~callback
g; g;
......
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