Commit 1b6db438 authored by Sylvain Dailler's avatar Sylvain Dailler

Adding the multiplier we use for the number of tasks we send to why3server

as a parameter of Scheduler.
Cannot be done via set_max_tasks (because this number is sent to
why3server and it fails when it is arbitrarily high).
parent 73372280
......@@ -144,6 +144,8 @@ let backtrace_and_exit f () =
module Scheduler = struct
let multiplier = 3
let idle ~prio f =
let (_ : GMain.Idle.id) = GMain.Idle.add ~prio (backtrace_and_exit f) in ()
......
......@@ -12,6 +12,8 @@
open Why3.Strings
open Format
let multiplier = 3
let hexa_digit x =
if x >= 10 then Char.chr (Char.code 'A' + x - 10)
else Char.chr (Char.code '0' + x)
......
......@@ -10,6 +10,8 @@
(********************************************************************)
val multiplier: int
val main_loop : string option -> int ->
(Unix.sockaddr * string list -> string ->
......
......@@ -213,6 +213,7 @@ let add_file c ?format fname =
module type Scheduler = sig
val multiplier: int
val timeout: ms:int -> (unit -> bool) -> unit
val idle: prio:int -> (unit -> bool) -> unit
end
......@@ -317,6 +318,12 @@ let build_prover_call ?proof_script ~cntexample c id pr limit callback ores =
let pa = (c.controller_session,id,pr,proof_script,callback,false,call,ores) in
Queue.push pa prover_tasks_in_progress
let update_observer () =
let scheduled = Queue.length scheduled_proof_attempts in
let waiting_or_running = Queue.length prover_tasks_in_progress in
let running = !number_of_running_provers in
!observer scheduled (waiting_or_running - running) running
let timeout_handler () =
(* examine all the prover tasks in progress *)
let q = Queue.create () in
......@@ -362,7 +369,7 @@ let timeout_handler () =
begin
try
for _i = Queue.length prover_tasks_in_progress
to 3 * !max_number_of_running_provers do
to S.multiplier * !max_number_of_running_provers do
let (c,id,pr,limit,proof_script,callback,cntexample,ores) =
Queue.pop scheduled_proof_attempts in
try
......@@ -375,10 +382,7 @@ let timeout_handler () =
done
with Queue.Empty -> ()
end;
let scheduled = Queue.length scheduled_proof_attempts in
let waiting_or_running = Queue.length prover_tasks_in_progress in
let running = !number_of_running_provers in
!observer scheduled (waiting_or_running - running) running;
update_observer ();
true
let interrupt () =
......
......@@ -53,6 +53,11 @@ module type Scheduler = sig
depending on some time constraints: after a given delay, or simply
when there is no more tasks with higher priority. *)
val multiplier: int
(** Number of allowed task given to why3server is this number times the
number of allowed proc on the machine.
*)
val timeout: ms:int -> (unit -> bool) -> unit
(** [timeout ~ms f] registers the function [f] as a function to be
called every [ms] milliseconds. The function is called repeatedly
......
......@@ -11,6 +11,8 @@
module Unix_scheduler = struct
let multiplier = 3
(* the private list of functions to call on idle, sorted higher
priority first. *)
let idle_handler : (int * (unit -> bool)) list ref = ref []
......
......@@ -11,6 +11,8 @@
module Unix_scheduler : sig
val multiplier: int
val timeout: ms:int -> (unit -> bool) -> unit
(** [timeout ~ms f] registers the function [f] as a function to be
called every [ms] milliseconds. The function is called repeatedly
......
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