Commit 7089accd authored by Sylvain Dailler's avatar Sylvain Dailler

blocking is a new parameter of module type scheduler.

parent e8e4bf55
......@@ -144,6 +144,8 @@ let backtrace_and_exit f () =
module Scheduler = struct
let blocking = false
let multiplier = 3
let idle ~prio f =
......
......@@ -12,6 +12,8 @@
open Why3.Strings
open Format
let blocking = false
let multiplier = 3
let hexa_digit x =
......
......@@ -9,6 +9,7 @@
(* *)
(********************************************************************)
val blocking: bool
val multiplier: int
......
......@@ -210,6 +210,7 @@ let add_file c ?format fname =
module type Scheduler = sig
val blocking: bool
val multiplier: int
val timeout: ms:int -> (unit -> bool) -> unit
val idle: prio:int -> (unit -> bool) -> unit
......@@ -338,7 +339,7 @@ let timeout_handler () =
(* When no tasks are there, probably no tasks were scheduled and the server
was not launched so getting results could fail. *)
if Hashtbl.length prover_tasks_in_progress != 0 then begin
let results = Call_provers.forward_results ~blocking:false (* TODO *) in
let results = Call_provers.forward_results ~blocking:S.blocking in
while not (Queue.is_empty results) do
let (call, prover_update) = Queue.pop results in
let c = try Some (Hashtbl.find prover_tasks_in_progress call)
......
......@@ -56,6 +56,10 @@ 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 blocking: bool
(** Set to true when the scheduler should wait for results of why3server
(script), false otherwise (ITP which needs reactive scheduling) *)
val multiplier: int
(** Number of allowed task given to why3server is this number times the
number of allowed proc on the machine.
......
......@@ -11,6 +11,9 @@
module Unix_scheduler = struct
(* TODO temporary. This scheduler should be split *)
let blocking = false
let multiplier = 3
(* the private list of functions to call on idle, sorted higher
......
......@@ -11,6 +11,8 @@
module Unix_scheduler : sig
val blocking: bool
val multiplier: int
val timeout: ms:int -> (unit -> bool) -> unit
......
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