better scheduler

Makefile.in

@@ -269,6 +269,64 @@ install::
 	mkdir -p $(BINDIR)
 	cp -f bin/whyml.@OCAMLBEST@ $(BINDIR)/whyml3
 
+###############
+# IDE
+###############
+
+IDE_FILES = scheduler 
+IDE_MAIN_FILE = gmain
+
+IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
+IDEMAIN = $(addprefix src/ide/, $(IDE_MAIN_FILE))
+
+IDEML  = $(addsuffix .ml,  $(IDEMODULES))
+IDEMLI = $(addsuffix .mli, $(IDEMODULES))
+IDECMO = $(addsuffix .cmo, $(IDEMODULES))
+IDECMX = $(addsuffix .cmx, $(IDEMODULES))
+
+IDEMAINML  = $(addsuffix .ml,  $(IDEMAIN))
+
+$(IDECMO) $(IDECMX) $(addsuffix .cmx, $(IDEMAIN)) $(addsuffix .cmo, $(IDEMAIN)): INCLUDES = -thread -I src/ide -I +threads
+# -I +sqlite3 
+
+src/ide/gmain.cmo src/ide/gmain.cmx: INCLUDES += -I +lablgtk2
+
+ifeq (@enable_ide@,yes)
+byte: bin/gwhy.byte
+opt:  bin/gwhy.opt
+endif
+
+bin/gwhy.opt bin/gwhy.byte: INCLUDES = -thread -I +lablgtk2
+# -I +sqlite3 
+
+bin/gwhy.opt: src/why.cmxa $(PGMCMX) $(IDECMX) src/ide/gmain.cmx
+	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \
+	lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx $^
+	$(STRIP) $@
+# sqlite3.cmxa 
+
+bin/gwhy.byte: src/why.cma $(PGMCMO) $(IDECMO) src/ide/gmain.cmo
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \
+	lablgtk.cma lablgtksourceview2.cma gtkThread.cmo $^
+# sqlite3.cma 
+
+# depend and clean targets
+
+include .depend.ide
+
+.depend.ide:
+	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) $(IDEMAINML) > $@
+
+depend: .depend.ide
+
+clean::
+	rm -f src/ide/*.cm[iox] src/ide/*.o
+	rm -f src/ide/*.annot src/ide/*~
+	rm -f bin/gwhy.byte bin/gwhy.opt
+	rm -f .depend.ide
+
 ###############
 # rust prover
 ###############

src/ide/scheduler.ml

+
+
+open Format
+open Why
+
+
+
+let async = ref (fun f () -> f ())
+
+type proof_attempt_status =
+  | Scheduled (** external proof attempt is scheduled *)
+  | Running (** external proof attempt is in progress *)
+  | Success (** external proof attempt succeeded *)
+  | Timeout (** external proof attempt was interrupted *)
+  | Unknown (** external prover answered ``don't know'' or equivalent *)
+  | HighFailure (** external prover call failed *)
+
+
+(**** queues of events to process ****)
+
+type attempt = bool * int * int * string * string * Driver.driver * 
+    (proof_attempt_status -> unit) * Task.task 
+
+(* queue of external proof attempts *)
+let prover_attempts_queue : attempt Queue.t = Queue.create ()
+
+(* queue of transformations *)
+let transf_queue  : int Queue.t = Queue.create ()
+
+(* queue of prover answers *)
+let answers_queue  : (attempt * proof_attempt_status) Queue.t = Queue.create ()
+
+(* number of running external proofs *)
+let running_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 ()
+
+
+
+
+(***** handler of events *****)
+
+let event_handler () =
+  Mutex.lock queue_lock;
+  while 
+    Queue.is_empty transf_queue && 
+      Queue.is_empty answers_queue && 
+      (Queue.is_empty prover_attempts_queue ||
+         !running_proofs >= !maximum_running_proofs)
+  do
+    Condition.wait queue_condition queue_lock
+  done;
+  try
+    let (a,res) = Queue.pop answers_queue in
+    decr running_proofs;
+    Mutex.unlock queue_lock;
+    eprintf "[Why thread] Scheduler.event_handler: got prover answer@.";
+    (* TODO: update database *)
+    (* call GUI callback with argument [res] *)
+    let (_,_,_,_,_,_,callback,_) = a in
+    !async (fun () -> callback res) ()
+  with Queue.Empty ->
+    try
+      let _t = Queue.pop transf_queue in
+      Mutex.unlock queue_lock;
+      eprintf "[Why thread] Scheduler.event_handler: transformations not supported yet@.";
+      (* TODO: update database *)
+      (* TODO: call GUI back given new subgoals *)
+    with Queue.Empty ->
+      (* 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
+      *)
+      try
+        let a = Queue.pop prover_attempts_queue in
+        incr running_proofs;
+        Mutex.unlock queue_lock;
+        (* build the prover task from goal in [a] *)
+        let (debug,timelimit,memlimit,_prover,command,driver,callback,goal) = a 
+        in
+        !async (fun () -> callback Running) ();
+        let call_prover : unit -> Call_provers.prover_result = 
+            if false && debug then 
+              Format.eprintf "Task for prover: %a@." 
+                (Driver.print_task driver) goal;
+            Driver.prove_task ~debug ~command ~timelimit ~memlimit driver goal
+        in              
+        let (_ : Thread.t) = Thread.create 
+          (fun () -> 
+             let r = call_prover () in
+             Mutex.lock queue_lock;
+             let res =
+               match r.Call_provers.pr_answer with
+                 | Call_provers.Valid -> Success         
+                 | Call_provers.Timeout -> Timeout
+                 | Call_provers.Invalid | Call_provers.Unknown _ -> Unknown
+                 | Call_provers.Failure _ | Call_provers.HighFailure 
+                     -> HighFailure
+             in
+             Queue.push (a,res) answers_queue ;
+             Mutex.unlock queue_lock;
+             Condition.signal queue_condition;
+             ()
+          )
+          ()
+        in ()
+      with Queue.Empty -> 
+        eprintf "Scheduler.event_handler: unexpected empty queues@.";
+        assert false
+
+
+(***** start of the scheduler thread ****)
+
+let (_scheduler_thread : Thread.t) =
+  Thread.create 
+    (fun () ->
+       try
+         (* loop forever *)
+         while true do
+           event_handler ()
+         done;
+         assert false
+       with
+           e -> 
+             eprintf "Scheduler thread stopped unexpectedly@.";
+             raise e)
+    ()
+
+
+(***** to be called from GUI ****)
+
+let schedule_proof_attempt ~debug ~timelimit ~memlimit ~prover 
+    ~command ~driver ~callback
+    goal =
+  Mutex.lock queue_lock;
+  Queue.push (debug,timelimit,memlimit,prover,command,driver,callback,goal)
+    prover_attempts_queue;
+  Mutex.unlock queue_lock;
+  Condition.signal queue_condition;
+  ()
+ 
+

src/ide/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.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+open Why
+
+val async: ((unit->unit)->unit->unit) ref
+(** async f () should call [f ()] *)
+
+type proof_attempt_status =
+  | Scheduled (** external proof attempt is scheduled *)
+  | Running (** external proof attempt is in progress *)
+  | Success (** external proof attempt succeeded *)
+  | Timeout (** external proof attempt was interrupted *)
+  | Unknown (** external prover answered ``don't know'' or equivalent *)
+  | HighFailure (** external prover call failed *)
+
+val schedule_proof_attempt : 
+  debug:bool -> timelimit:int -> memlimit:int -> 
+  prover:string (*Db.prover*) -> 
+  command:string -> driver:Driver.driver -> 
+  callback:(proof_attempt_status -> unit) -> 
+  Task.task (* Db.goal *) -> unit
+  (** schedules an attempt to prove goal with the given prover.  This
+      function just prepares the goal for the proof attempt, and puts
+      it in the queue of waiting proof attempts, associated with its
+      callback.
+
+      The callback is called each time the status of that proves
+      changes, typically from Scheduled, then Running, then Success or
+      Timeout or Failure.
+      
+      @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
+
+
+  *)
+
+
+
+
+(*
+Local Variables: 
+compile-command: "make -C ../.. bin/gwhy.byte"
+End: 
+*)
+
+
+
+

src/manager/scheduler.ml

@@ -60,3 +60,10 @@ let schedule_proof_attempt ~async ~debug ~timelimit ~memlimit ~prover
         
 
   
+
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../.. bin/gwhy.byte"
+End: 
+*)