Call_prover : Str uses a shared reference...

Scheduler : Schedule the call, precompute the
buffer in advance.

src/bench/bench.ml

@@ -58,7 +58,7 @@ struct
 
   let start s = Mutex.lock s.m; s.nb_task <- s.nb_task + 1; Mutex.unlock s.m
   let stop s = Mutex.lock s.m; s.nb_task <- s.nb_task - 1;
-    Mutex.unlock s.m; if s.nb_task = 0 then Condition.signal s.c
+    if s.nb_task = 0 then Condition.signal s.c; Mutex.unlock s.m
   let wait s = Mutex.lock s.m; Condition.wait s.c s.m
   let lock s = Mutex.lock s.m
   let unlock s = Mutex.unlock s.m

src/bench/whybench.ml

@@ -373,7 +373,12 @@ let count_result =
     Mnm.add res.B.tool tr m in
   List.fold_left fold m
 
-let () = Scheduler.async := (fun f v -> ignore (Thread.create f v))
+let () =
+  (** WHY some outputs are mixed, altought there is a mutex? *)
+  let m = Mutex.create () in
+  Scheduler.async := (fun f v ->
+    let f v = Mutex.lock m; f v; Mutex.unlock m in
+    ignore (Thread.create f v))
 
 let () =
   let callback tool prob task i res =

src/coq-plugin/whytac.ml

@@ -897,7 +897,7 @@ let whytac s gl =
     let command = cp.command in
     if debug then Format.printf "@[%a@]@\n---@." Pretty.print_task !task;
     if debug then Format.printf "@[%a@]@\n---@." (Driver.print_task drv) !task;
-    let res = Driver.prove_task ~command ~timelimit drv !task () in
+    let res = Driver.prove_task ~command ~timelimit drv !task () () in
     match res.pr_answer with
       | Valid -> Tactics.admit_as_an_axiom gl
       | Invalid -> error "Invalid"

src/driver/call_provers.ml

@@ -80,7 +80,7 @@ let call_prover command opt_cout buffer =
   ret, out, time
 
 let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
-                   ~regexps ~exitcodes ~filename buffer () =
+                   ~regexps ~exitcodes ~filename buffer =
   let on_stdin = ref true in
   let on_timelimit = ref false in
   let cmd_regexp = Str.regexp "%\\(.\\)" in
@@ -92,11 +92,13 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
     | _ -> failwith "unknown format specifier, use %%f, %%t or %%m"
   in
   let cmd = Str.global_substitute cmd_regexp (replace "") command in
-  let ret, out, time =
-    if !on_stdin then call_prover cmd None buffer else begin
+  let f = if !on_stdin then
+    fun () -> call_prover cmd None buffer
+  else begin
       let fout,cout = Filename.open_temp_file "why_" ("_" ^ filename) in
       try
         let cmd = Str.global_substitute cmd_regexp (replace fout) command in
+        fun () ->
         let res = call_prover cmd (Some cout) buffer in
         if Debug.nottest_flag debug then Sys.remove fout;
         res
@@ -106,6 +108,9 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
         raise e
     end
   in
+  fun () ->
+    let ret,out,time = f () in
+    fun () ->
   let ans = match ret with
     | Unix.WSTOPPED n ->
         Debug.dprintf debug "Call_provers: stopped by signal %d@." n;

src/driver/call_provers.mli

@@ -65,8 +65,9 @@ val call_on_buffer :
   regexps    : (Str.regexp * prover_answer) list ->
   exitcodes  : (int * prover_answer) list ->
   filename   : string ->
-  Buffer.t -> unit -> prover_result
+  Buffer.t -> unit -> unit -> prover_result
 (** Call a prover on the task printed in the {!type: Buffer.t} given.
+    Only the computation between the two [unit] is parallelisable.
 
     @param timelimit : set the available time limit (default 0 : unlimited)
     @param memlimit : set the available time limit (default 0 :

src/driver/driver.mli

@@ -41,7 +41,7 @@ val call_on_buffer :
   command    : string ->
   ?timelimit : int ->
   ?memlimit  : int ->
-  driver -> Buffer.t -> unit -> Call_provers.prover_result
+  driver -> Buffer.t -> unit -> unit -> Call_provers.prover_result
 
 val print_task :
   ?old       : in_channel ->
@@ -52,5 +52,5 @@ val prove_task :
   ?timelimit : int ->
   ?memlimit  : int ->
   ?old       : in_channel ->
-  driver -> Task.task -> (unit -> Call_provers.prover_result)
+  driver -> Task.task -> (unit -> unit -> Call_provers.prover_result)
 

src/ide/gmain.ml

@@ -86,7 +86,6 @@ open Why
 open Whyconf
 open Gconfig
 
-
 (************************)
 (* parsing command line *)
 (************************)

src/ide/scheduler.ml

@@ -3,7 +3,8 @@
 open Format
 open Why
 
-
+(** max scheduled proofs / max running proofs *)
+let coef_buf = 2
 
 let async = ref (fun f () -> f ())
 
@@ -47,20 +48,25 @@ type job =
 let transf_queue  : job Queue.t = Queue.create ()
 
 type answer =
-  | Prover_answer of callback * proof_attempt_status
+  | Prover_answer of callback * (unit -> Call_provers.prover_result)
   | Editor_exited of (unit -> unit)
 (* queue of prover answers *)
 let answers_queue  : answer Queue.t = Queue.create ()
 
-(* number of running external proofs *)
-let running_proofs = ref 0
+(* number of scheduled external proofs *)
+let scheduled_proofs = ref 0
 let maximum_running_proofs = ref 2
 
 (* they are protected by a lock *)
 let queue_lock = Mutex.create ()
 let queue_condition = Condition.create ()
 
+(* number of running external proofs *)
+let running_proofs = ref 0
 
+(* it is protected by a lock *)
+let running_lock = Mutex.create ()
+let running_condition = Condition.create ()
 
 
 (***** handler of events *****)
@@ -72,27 +78,28 @@ let event_handler () =
       Queue.is_empty answers_queue &&
       Queue.is_empty proof_edition_queue &&
       (Queue.is_empty prover_attempts_queue ||
-         !running_proofs >= !maximum_running_proofs)
+         !scheduled_proofs >= !maximum_running_proofs * coef_buf)
   do
     Condition.wait queue_condition queue_lock
   done;
   try begin
     (* priority 1: collect answers from provers or editors *)
     match Queue.pop answers_queue with
-      | Prover_answer (callback,res) ->
-          decr running_proofs;
-          Mutex.unlock queue_lock;
+      | Prover_answer (callback,r) ->
+        Mutex.unlock queue_lock;
+        let res = r () in
           (*
             eprintf
             "[Why thread] Scheduler.event_handler: got prover answer@.";
           *)
           (* call GUI callback with argument [res] *)
-          !async (fun () -> callback res) ()
+          !async (fun () -> callback (Done res)) ()
       | Editor_exited callback ->
           Mutex.unlock queue_lock;
           !async callback ()
   end
   with Queue.Empty ->
+    Thread.yield ();
     try
       (* priority 2: apply transformations *)
       let k = Queue.pop transf_queue in
@@ -144,18 +151,18 @@ let event_handler () =
       (* since answers_queue and transf_queue are empty,
          we are sure that both
          prover_attempts_queue is non empty and
-         running_proofs < maximum_running_proofs
+         scheduled_proofs < maximum_running_proofs * coef_buf
       *)
       try
         let (_debug,timelimit,memlimit,old,command,driver,callback,goal) =
           Queue.pop prover_attempts_queue
         in
-        incr running_proofs;
+        incr scheduled_proofs;
         Mutex.unlock queue_lock;
         (* build the prover task from goal in [a] *)
-        !async (fun () -> callback Running) ();
+        !async (fun () -> callback Scheduled) ();
         try
-          let call_prover : unit -> Call_provers.prover_result =
+          let call_prover : unit -> unit -> Call_provers.prover_result =
 (*
             if debug then
               Format.eprintf "Task for prover: %a@."
@@ -165,11 +172,25 @@ let event_handler () =
           in
           let (_ : Thread.t) = Thread.create
             (fun () ->
+              Mutex.lock running_lock;
+              while !running_proofs >= !maximum_running_proofs; do
+                Condition.wait running_condition running_lock
+              done;
+              incr running_proofs;
+              Mutex.unlock running_lock;
+              Mutex.lock queue_lock;
+              decr scheduled_proofs;
+              Condition.signal queue_condition;
+              Mutex.unlock queue_lock;
+              !async (fun () -> callback Running) ();
                let r = call_prover () in
+               Mutex.lock running_lock;
+               decr running_proofs;
+               Condition.signal running_condition;
+               Mutex.unlock running_lock;
                Mutex.lock queue_lock;
-               let res = Done r in
                Queue.push
-                 (Prover_answer (callback,res)) answers_queue ;
+                 (Prover_answer (callback,r)) answers_queue ;
                Condition.signal queue_condition;
                Mutex.unlock queue_lock;
                ()
@@ -180,16 +201,13 @@ let event_handler () =
           | e ->
             eprintf "%a@." Exn_printer.exn_printer e;
             Mutex.lock queue_lock;
-            Queue.push
-              (Prover_answer (callback, InternalFailure e)) answers_queue ;
-            (* Condition.signal queue_condition; *)
+            decr scheduled_proofs;
             Mutex.unlock queue_lock;
-            ()
+            !async (fun () -> callback (InternalFailure e)) ()
      with Queue.Empty ->
         eprintf "Scheduler.event_handler: unexpected empty queues@.";
         assert false
 
-
 (***** start of the scheduler thread ****)
 
 let (_scheduler_thread : Thread.t) =
@@ -218,30 +236,26 @@ let schedule_proof_attempt ~debug ~timelimit ~memlimit ?old
   Queue.push (debug,timelimit,memlimit,old,command,driver,callback,goal)
     prover_attempts_queue;
   Condition.signal queue_condition;
-  Mutex.unlock queue_lock;
-  ()
+  Mutex.unlock queue_lock
 
 let edit_proof ~debug ~editor ~file ~driver ~callback goal =
   Mutex.lock queue_lock;
   Queue.push (debug,editor,file,driver,callback,goal) proof_edition_queue;
   Condition.signal queue_condition;
-  Mutex.unlock queue_lock;
-  ()
+  Mutex.unlock queue_lock
 
 let apply_transformation ~callback transf goal =
   Mutex.lock queue_lock;
   Queue.push (Task (callback,transf,goal)) transf_queue;
   Condition.signal queue_condition;
-  Mutex.unlock queue_lock;
-  ()
+  Mutex.unlock queue_lock
 
 
 let apply_transformation_l ~callback transf goal =
   Mutex.lock queue_lock;
   Queue.push (TaskL (callback,transf,goal)) transf_queue;
   Condition.signal queue_condition;
-  Mutex.unlock queue_lock;
-  ()
+  Mutex.unlock queue_lock
 
 
 let do_why ~callback funct argument =
@@ -252,8 +266,7 @@ let do_why ~callback funct argument =
   Mutex.lock queue_lock;
   Queue.push (Do exists) transf_queue;
   Condition.signal queue_condition;
-  Mutex.unlock queue_lock;
-  ()
+  Mutex.unlock queue_lock
 
 (* TODO : understand Thread.Event *)
 let do_why_sync funct argument =

src/main.ml

@@ -341,7 +341,7 @@ let do_task drv fname tname (th : Why.Theory.theory) (task : Task.task) =
   match !opt_output, !opt_command with
     | None, Some command ->
         let res =
-          Driver.prove_task ~command ~timelimit ~memlimit drv task ()
+          Driver.prove_task ~command ~timelimit ~memlimit drv task () ()
         in
         printf "%s %s %s : %a@." fname tname
           (task_goal task).Decl.pr_name.Ident.id_string