Commit 62df2cae authored by MARCHE Claude's avatar MARCHE Claude

itp: basic scheduler using Unix

parent 53f6b14f
......@@ -25,6 +25,14 @@ let print_status fmt st =
type transformation_status =
| TSscheduled of transID | TSdone of transID | TSfailed
module type Scheduler = sig
val timeout: ms:int -> (unit -> bool) -> unit
val idle: (unit -> bool) -> unit
end
module Make(S : Scheduler) = struct
let schedule_proof_attempt s id pr ~timelimit ~callback =
graft_proof_attempt s id pr ~timelimit;
callback Scheduled
......@@ -58,3 +66,73 @@ let add_file_to_session env s ?format fname =
let reload_session_files (_s : session) =
failwith "Controller_itp.reload_session_files not yet implemented"
end
let usleep t = ignore (Unix.select [] [] [] t)
module Unix_scheduler = struct
let idle_handler = ref None
let timeout_handler = ref None
let verbose = ref true
let idle f =
match !idle_handler with
| None -> idle_handler := Some f;
| Some _ -> failwith "Unix_scheduler.idle: already one handler installed"
let timeout ~ms f =
match !timeout_handler with
| None -> timeout_handler := Some(float ms /. 1000.0 ,f);
| Some _ -> failwith "Unix_scheduler.timeout: already one handler installed"
let notify_timer_state w s r =
if !verbose then
Printf.eprintf "Progress: %d/%d/%d \r%!" w s r
let main_loop () =
let last = ref (Unix.gettimeofday ()) in
try while true do
let time = Unix.gettimeofday () -. !last in
(* attempt to run timeout handler *)
let timeout =
match !timeout_handler with
| None -> false
| Some(ms,f) ->
if time > ms then
let b = f () in
if b then true else
begin
timeout_handler := None;
true
end
else false
in
if timeout then
last := Unix.gettimeofday ()
else
(* attempt to run the idle handler *)
match !idle_handler with
| None ->
begin
let ms =
match !timeout_handler with
| None -> raise Exit
| Some(ms,_) -> ms
in
usleep (ms -. time)
end
| Some f ->
let b = f () in
if b then () else
begin
idle_handler := None;
end
done
with Exit -> ()
end
......@@ -23,6 +23,21 @@ type proof_attempt_status =
val print_status : Format.formatter -> proof_attempt_status -> unit
type transformation_status = TSscheduled of transID | TSdone of transID | TSfailed
module type Scheduler = sig
val timeout: ms:int -> (unit -> bool) -> unit
val idle: (unit -> bool) -> unit
end
module Unix_scheduler : sig
include Scheduler
val main_loop : unit -> unit
end
module Make(S : Scheduler) : sig
val schedule_proof_attempt :
session ->
proofNodeID ->
......@@ -35,8 +50,6 @@ val schedule_proof_attempt :
changes. Typically at Scheduled, then Running, then Done. If there
is already a proof attempt with [p] it is updated. *)
type transformation_status = TSscheduled of transID | TSdone of transID | TSfailed
val schedule_transformations :
session ->
proofNodeID ->
......@@ -71,3 +84,5 @@ val reload_session_files : session -> unit
raises [OutdatedSession] if the session is obsolete and
[allow_obsolete] is false
*)
end
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