Commit e9922218 authored by MARCHE Claude's avatar MARCHE Claude

compiles with scheduler

parent 24a69914
...@@ -257,7 +257,7 @@ clean:: ...@@ -257,7 +257,7 @@ clean::
# proof manager # proof manager
############### ###############
MNG_FILES = db test MNG_FILES = db scheduler test
MNGMODULES = $(addprefix src/manager/, $(MNG_FILES)) MNGMODULES = $(addprefix src/manager/, $(MNG_FILES))
...@@ -266,23 +266,23 @@ MNGMLI = $(addsuffix .mli, $(MNGMODULES)) ...@@ -266,23 +266,23 @@ MNGMLI = $(addsuffix .mli, $(MNGMODULES))
MNGCMO = $(addsuffix .cmo, $(MNGMODULES)) MNGCMO = $(addsuffix .cmo, $(MNGMODULES))
MNGCMX = $(addsuffix .cmx, $(MNGMODULES)) MNGCMX = $(addsuffix .cmx, $(MNGMODULES))
$(MNGCMO) $(MNGCMX): INCLUDES = -I src/manager -I +sqlite3 $(MNGCMO) $(MNGCMX): INCLUDES = -thread -I src/manager -I +sqlite3
ifeq (@enable_proof_manager@,yes) ifeq (@enable_proof_manager@,yes)
byte: bin/manager.byte byte: bin/manager.byte
opt: bin/manager.opt opt: bin/manager.opt
endif endif
bin/manager.opt bin/manager.byte: INCLUDES = -I +sqlite3 bin/manager.opt bin/manager.byte: INCLUDES = -thread -I +sqlite3
bin/manager.opt: src/why.cmxa $(MNGCMX) bin/manager.opt: src/why.cmxa $(MNGCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \ $(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) sqlite3.cmxa $^ $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa sqlite3.cmxa $^
$(STRIP) $@ $(STRIP) $@
bin/manager.byte: src/why.cma $(MNGCMO) bin/manager.byte: src/why.cma $(MNGCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \ $(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) sqlite3.cma $^ $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma sqlite3.cma $^
# depend and clean targets # depend and clean targets
......
...@@ -17,6 +17,7 @@ ...@@ -17,6 +17,7 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
open Why
(** {1 Proof manager database} *) (** {1 Proof manager database} *)
...@@ -88,7 +89,7 @@ end ...@@ -88,7 +89,7 @@ end
type transf_data = type transf_data =
{ transf_name : string; { transf_name : string;
transf_action : Why.Task.task Why.Register.tlist_reg transf_action : Task.task Register.tlist_reg
} }
type transf type transf
...@@ -103,7 +104,7 @@ val goal_name : goal -> string ...@@ -103,7 +104,7 @@ val goal_name : goal -> string
*) *)
(* (*
val goal_task : goal -> Why.Task.task val goal_task : goal -> Task.task
*) *)
val goal_task_checksum: goal -> string val goal_task_checksum: goal -> string
val external_proofs : goal -> external_proof list val external_proofs : goal -> external_proof list
...@@ -149,7 +150,7 @@ exception AlreadyAttempted ...@@ -149,7 +150,7 @@ exception AlreadyAttempted
val try_prover : val try_prover :
debug:bool -> timelimit:int -> memlimit:int -> prover:prover -> debug:bool -> timelimit:int -> memlimit:int -> prover:prover ->
command:string -> driver:Why.Driver.driver -> goal -> (unit -> unit) command:string -> driver:Driver.driver -> goal -> (unit -> unit)
(** attempts to prove goal with the given prover. This function (** attempts to prove goal with the given prover. This function
prepares the goal for that prover, adds it as an new prepares the goal for that prover, adds it as an new
external_proof attempt, setting its current status to Scheduled, external_proof attempt, setting its current status to Scheduled,
...@@ -206,7 +207,7 @@ val add_transformation: goal -> transf -> unit ...@@ -206,7 +207,7 @@ val add_transformation: goal -> transf -> unit
(* {2 goal updates} *) (* {2 goal updates} *)
val add_or_replace_task: tname:string -> name:string -> Why.Task.task -> goal val add_or_replace_task: tname:string -> name:string -> Task.task -> goal
(** updates the database with the new goal called [name] in the (** updates the database with the new goal called [name] in the
theory called [tname]. If a goal with the same [(tname,name)] theory called [tname]. If a goal with the same [(tname,name)]
already exists, it is checked whether the task to prove is already exists, it is checked whether the task to prove is
......
let attempts = Queue.create () (* queue of pending proof attempts
protected by a lock
*)
let queue_lock = Mutex.create ()
let attempts = Queue.create ()
let running_proofs = ref 0 let running_proofs = ref 0
let maximum_running_proofs = ref 1 let maximum_running_proofs = ref 2
(*
let start_queue_thread n =
if !maximum_running_proofs > 0
then failwith "Scheduler: queue thread already running";
if n <= 0 then invalid_arg "Scheduler.start_queue_thread";
maximum_running_proofs := n;
*)
let schedule_proof_attempt ~debug ~timelimit ~memlimit ~prover
let try_prover ~debug:bool ~timelimit:int ~memlimit:int ~prover:prover ~command ~driver ~callback
~command:string ~driver:Why.Driver.driver ~callback:(unit -> unit)
goal = goal =
let call = let prepare_goal =
try try
Db.try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver goal Db.try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver goal
with Db.AlreadyAttempted -> with Db.AlreadyAttempted ->
raise Exit raise Exit
in in
(* store the attemp into the queue *) let _thread_id =
Queue.push (prepare_goal,callback) attempts; Thread.create
(* try to run attempt if resource available *) begin
while !running_proofs < !maximum_running_proofs do fun () ->
incr running_proofs; try
call (); (* BEGIN LOCKED SECTION *)
callback (); (* lock and store the attempt into the queue *)
decr running_proofs; Mutex.lock queue_lock;
done Queue.push (prepare_goal,callback) attempts;
(* try to run attempt if resource available *)
while !running_proofs < !maximum_running_proofs do
let call,callback = Queue.pop attempts in
incr running_proofs;
Mutex.unlock queue_lock;
(* END LOCKED SECTION *)
call ();
callback ();
(* BEGIN LOCKED SECTION *)
Mutex.lock queue_lock;
decr running_proofs;
done;
Mutex.unlock queue_lock
(* END LOCKED SECTION *)
with
| Queue.Empty ->
(* Queue was Empty *)
Mutex.unlock queue_lock
(* END LOCKED SECTION *)
| e ->
(* any other exception should be propagated
after unlocking the lock *)
Mutex.unlock queue_lock;
(* END LOCKED SECTION *)
raise e
end
()
in ()
...@@ -18,12 +18,12 @@ ...@@ -18,12 +18,12 @@
(**************************************************************************) (**************************************************************************)
open Why
val schedule_proof_attempt : val schedule_proof_attempt :
debug:bool -> timelimit:int -> memlimit:int -> prover:prover -> debug:bool -> timelimit:int -> memlimit:int -> prover:Db.prover ->
command:string -> driver:Why.Driver.driver -> command:string -> driver:Driver.driver ->
callback:(unit -> unit) -> goal -> unit callback:(unit -> unit) -> Db.goal -> unit
(** schedules an attempt to prove goal with the given prover. This (** schedules an attempt to prove goal with the given prover. This
function just prepares the goal for the proof attempt, and put function just prepares the goal for the proof attempt, and put
it in the queue of waiting proofs attempts, associated with its it in the queue of waiting proofs attempts, associated with its
...@@ -43,14 +43,6 @@ val schedule_proof_attempt : ...@@ -43,14 +43,6 @@ val schedule_proof_attempt :
*) *)
val start_queue_thread : int -> unit
(** starts another thread in charge of launching proof attempts
the parameter is the maximal number of proof attempts to run in parallel.
Whenever an external proof attempt terminates, the associated callback
is called.
*)
......
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