Commit 28b9f058 authored by François Bobot's avatar François Bobot

Dont create one thread by external proof

parent b82bb4d2
...@@ -424,7 +424,7 @@ install_local: bin/why3config ...@@ -424,7 +424,7 @@ install_local: bin/why3config
ifeq (@enable_ide@,yes) ifeq (@enable_ide@,yes)
IDE_FILES = gconfig scheduler db gmain IDE_FILES = gconfig worker scheduler db gmain
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES)) IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
...@@ -489,7 +489,7 @@ BENCH_FILES = bench benchrc whybench ...@@ -489,7 +489,7 @@ BENCH_FILES = bench benchrc whybench
BENCHMODULES := $(addprefix src/bench/, $(BENCH_FILES)) BENCHMODULES := $(addprefix src/bench/, $(BENCH_FILES))
BENCHMODULES := src/ide/scheduler $(BENCHMODULES) BENCHMODULES := src/ide/worker src/ide/scheduler $(BENCHMODULES)
BENCHML = $(addsuffix .ml, $(BENCHMODULES)) BENCHML = $(addsuffix .ml, $(BENCHMODULES))
BENCHMLI = $(addsuffix .mli, $(BENCHMODULES)) BENCHMLI = $(addsuffix .mli, $(BENCHMODULES))
......
...@@ -59,76 +59,7 @@ type ('a,'b) callback = 'a -> 'b -> task -> int -> proof_attempt_status -> unit ...@@ -59,76 +59,7 @@ type ('a,'b) callback = 'a -> 'b -> task -> int -> proof_attempt_status -> unit
let debug_call = Debug.register_flag "call" let debug_call = Debug.register_flag "call"
let debug = Debug.register_flag "bench_core" let debug = Debug.register_flag "bench_core"
(** Create and manage one main worker which open Worker
wait for the remaining works *)
module MainWorker :
sig
type 'a t
val create : unit -> 'a t
val treat : 'a t -> ('b -> 'a -> 'b) -> 'b -> 'b
val start_work : 'a t -> unit
val stop_work : 'a t -> unit
val add_work : 'a t -> 'a -> unit
val add_works : 'a t -> 'a Queue.t -> unit
end
=
struct
type 'a t = { queue : 'a Queue.t;
mutex : Mutex.t;
condition : Condition.t;
mutable remaining : int;
}
let create () =
{ queue = Queue.create ();
mutex = Mutex.create ();
condition = Condition.create ();
remaining = 0;
}
let treat t f acc =
let rec main acc =
Mutex.lock t.mutex;
while Queue.is_empty t.queue && t.remaining > 0 do
Condition.wait t.condition t.mutex
done;
if Queue.is_empty t.queue
then begin (* t.remaining < 0 *) Mutex.unlock t.mutex;acc end
else
begin
let v = Queue.pop t.queue in
Mutex.unlock t.mutex;
let acc = f acc v in
Thread.yield ();
main acc
end in
main acc
let start_work t =
Mutex.lock t.mutex;
t.remaining <- t.remaining + 1;
Mutex.unlock t.mutex
let stop_work t =
Mutex.lock t.mutex;
t.remaining <- t.remaining - 1;
if t.remaining = 0 then Condition.signal t.condition;
Mutex.unlock t.mutex
let add_work t x =
Mutex.lock t.mutex;
Queue.push x t.queue;
Condition.signal t.condition;
Mutex.unlock t.mutex
let add_works t q =
Mutex.lock t.mutex;
Queue.transfer q t.queue;
Condition.signal t.condition;
Mutex.unlock t.mutex
end
let call s callback tool prob = let call s callback tool prob =
(** Prove goal *) (** Prove goal *)
......
...@@ -20,6 +20,7 @@ ...@@ -20,6 +20,7 @@
open Format open Format
open Why open Why
open Worker
(** max scheduled proofs / max running proofs *) (** max scheduled proofs / max running proofs *)
let coef_buf = 2 let coef_buf = 2
...@@ -165,7 +166,26 @@ let edit_proof () = ...@@ -165,7 +166,26 @@ let edit_proof () =
prover_attempts_queue is non empty and prover_attempts_queue is non empty and
scheduled_proofs < maximum_running_proofs * coef_buf scheduled_proofs < maximum_running_proofs * coef_buf
*) *)
let new_external_proof () =
let new_external_proof =
let run_external (call_prover,callback) =
Mutex.lock queue_lock;
decr scheduled_proofs;
incr running_proofs;
print_debug_nb_running ();
Condition.signal queue_condition;
Mutex.unlock queue_lock;
!async (fun () -> callback Running) ();
let r = call_prover () in
Mutex.lock queue_lock;
decr running_proofs;
print_debug_nb_running ();
Queue.push (Prover_answer (callback,r)) answers_queue ;
Condition.signal queue_condition;
Mutex.unlock queue_lock in
let external_workers =
ManyWorkers.create maximum_running_proofs run_external in
fun () ->
if !scheduled_proofs >= !maximum_running_proofs * coef_buf if !scheduled_proofs >= !maximum_running_proofs * coef_buf
then raise Queue.Empty; then raise Queue.Empty;
let (_debug,timelimit,memlimit,old,command,driver,callback,goal) = let (_debug,timelimit,memlimit,old,command,driver,callback,goal) =
...@@ -188,35 +208,7 @@ let new_external_proof () = ...@@ -188,35 +208,7 @@ let new_external_proof () =
*) *)
Driver.prove_task ?old ~command ~timelimit ~memlimit driver goal Driver.prove_task ?old ~command ~timelimit ~memlimit driver goal
in in
let (_ : Thread.t) = Thread.create ManyWorkers.add_work external_workers (call_prover,callback);
(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;
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 ;
Condition.signal queue_condition;
Mutex.unlock queue_lock;
()
)
()
in ()
with with
| e -> | e ->
eprintf "%a@." Exn_printer.exn_printer e; eprintf "%a@." Exn_printer.exn_printer e;
......
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