Commit 98c42d6b authored by François Bobot's avatar François Bobot

whybench : remove not anymore needed mutex

debug    : add more debug
parent c4773ded
......@@ -56,7 +56,8 @@ type ('a,'b) result = {tool : 'a;
type ('a,'b) callback = 'a -> 'b -> task -> int -> proof_attempt_status -> unit
let debug = Debug.register_flag "call"
let debug_call = Debug.register_flag "call"
let debug = Debug.register_flag "bench_core"
module MTask :
sig
......@@ -93,7 +94,7 @@ end
let call s callback tool prob =
(** Prove goal *)
let call q cb task =
Queue.add (create_proof_attempt ~debug:(Debug.test_flag debug)
Queue.add (create_proof_attempt ~debug:(Debug.test_flag debug_call)
~timelimit:(tool.ttime) ~memlimit:(tool.tmem)
~command:(tool.tcommand) ~driver:(tool.tdriver)
~callback:cb task) q in
......
......@@ -380,12 +380,10 @@ let () =
Scheduler.async := async
let () =
let m = Mutex.create () in
let nb_scheduled = ref 0 in
let nb_done = ref 0 in
let nb_valid = ref 0 in
let callback (_,tool) (_,file,prob) task i res =
Mutex.lock m;
if not !opt_quiet then
begin match res with
| Scheduler.Scheduled -> incr nb_scheduled
......@@ -401,7 +399,6 @@ let () =
Debug.dprintf Scheduler.debug "%s.%s %a %i with %s : %a@."
file prob Pretty.print_pr (task_goal task) i tool
Scheduler.print_pas res;
Mutex.unlock m
in
let benchs =
List.map (fun b -> List.map snd (Mstr.bindings b.Benchrc.benchs))
......
......@@ -88,6 +88,10 @@ let running_proofs = ref 0
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 *****)
......@@ -119,11 +123,11 @@ let event_handler () =
!async callback ()
end
with Queue.Empty ->
Thread.yield ();
try
(* priority 2: apply transformations *)
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
......@@ -178,12 +182,14 @@ let event_handler () =
Queue.pop prover_attempts_queue
in
incr scheduled_proofs;
Debug.dprintf debug
"scheduled_proofs = %i; maximum_running_proofs = %i;@."
!scheduled_proofs !maximum_running_proofs;
print_debug_nb_running ();
Mutex.unlock queue_lock;
Thread.yield ();
(* build the prover task from goal in [a] *)
try
Debug.dprintf debug
"%a is sent to driver;@."
(fun fmt g -> Pretty.print_pr fmt (Task.task_goal g)) goal;
let call_prover : unit -> unit -> Call_provers.prover_result =
(*
if debug then
......@@ -204,12 +210,14 @@ let event_handler () =
decr scheduled_proofs;
Condition.signal queue_condition;
Mutex.unlock queue_lock;
print_debug_nb_running ();
!async (fun () -> callback Running) ();
let r = call_prover () in
Mutex.lock running_lock;
decr running_proofs;
Condition.signal running_condition;
Mutex.unlock running_lock;
print_debug_nb_running ();
Mutex.lock queue_lock;
Queue.push
(Prover_answer (callback,r)) answers_queue ;
......
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