scheduler

src/manager/db.mli

@@ -152,13 +152,13 @@ val try_prover :
   command:string -> driver:Why.Driver.driver -> goal -> (unit -> unit)
   (** attempts to prove goal with the given prover.  This function
       prepares the goal for that prover, adds it as an new
-      external_proof attempt, setting its current status to Running,
+      external_proof attempt, setting its current status to Scheduled,
       and returns immmediately a function.  When called, this function
-      actually launches the prover, and waits for its
-      termination. Upon termination of the external process, the
-      prover's answer is retrieved and database is updated. The
-      [proved] field of the database is updated, and also these of any
-      goal affected, according to invariant above. 
+      actually sets the status to running, launches the prover, and
+      waits for its termination. Upon termination of the external
+      process, the prover's answer is retrieved and database is
+      updated. The [proved] field of the database is updated, and also
+      these of any goal affected, according to invariant above.
 
       Although goal preparation is not re-entrant, the function
       returned initially is re-entrant, thus is suitable for being executed

src/manager/scheduler.ml

+
+
+let attempts = Queue.create ()
+
+let running_proofs = ref 0
+let maximum_running_proofs = ref 1
+
+(*
+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 try_prover ~debug:bool ~timelimit:int ~memlimit:int ~prover:prover 
+    ~command:string ~driver:Why.Driver.driver ~callback:(unit -> unit) 
+    goal =
+  let call = 
+    try
+      Db.try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver goal 
+    with Db.AlreadyAttempted ->
+      raise Exit
+  in
+  (* store the attemp into the queue *)
+  Queue.push (prepare_goal,callback) attempts;
+  (* try to run attempt if resource available *)
+  while !running_proofs < !maximum_running_proofs do
+    incr running_proofs;
+    call ();
+    callback ();
+    decr running_proofs;
+  done

src/manager/scheduler.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-                                                   *)
+(*    Francois Bobot                                                      *)
+(*    Jean-Christophe Filliatre                                           *)
+(*    Johannes Kanig                                                      *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+
+
+val schedule_proof_attempt : 
+  debug:bool -> timelimit:int -> memlimit:int -> prover:prover -> 
+  command:string -> driver:Why.Driver.driver -> 
+  callback:(unit -> unit) -> goal -> unit
+  (** schedules an attempt to prove goal with the given prover.  This
+      function just prepares the goal for the proof attempt, and put
+      it in the queue of waiting proofs attempts, associated with its
+      callback.
+      
+      @param timelimit CPU time limit given for that attempt, in
+      seconds, must be positive. (unlimited attempts are not allowed
+      with this function)
+
+      @param memlimit memory limit given for that attempt, must be
+      positive. If not given, does not limit memory consumption
+
+      @raise AlreadyAttempted if there already exists a non-obsolete
+      external proof attempt with the same prover and time limit, or
+      with a lower or equal time limit and a result different from Timeout
+
+
+  *)
+
+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.
+
+*)
+
+
+
+(*
+Local Variables: 
+compile-command: "make -C ../.. bin/manager.byte"
+End: 
+*)
+
+
+
+