scheduler.ml 1.85 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2


3
(* queue of pending proof attempts
MARCHE Claude's avatar
MARCHE Claude committed
4 5
   protected by a lock
*)
MARCHE Claude's avatar
MARCHE Claude committed
6

MARCHE Claude's avatar
MARCHE Claude committed
7 8
let queue_lock = Mutex.create ()
let attempts = Queue.create ()
MARCHE Claude's avatar
MARCHE Claude committed
9
let running_proofs = ref 0
MARCHE Claude's avatar
MARCHE Claude committed
10
let maximum_running_proofs = ref 2
MARCHE Claude's avatar
MARCHE Claude committed
11

12
let schedule_proof_attempt ~async ~debug ~timelimit ~memlimit ~prover
MARCHE Claude's avatar
MARCHE Claude committed
13
    ~command ~driver ~callback
MARCHE Claude's avatar
MARCHE Claude committed
14
    goal =
15
  let prepare_goal =
MARCHE Claude's avatar
MARCHE Claude committed
16
    try
MARCHE Claude's avatar
MARCHE Claude committed
17
      Db.try_prover ~async ~debug ~timelimit ~memlimit ~prover ~command ~driver goal;
MARCHE Claude's avatar
MARCHE Claude committed
18 19 20
    with Db.AlreadyAttempted ->
      raise Exit
  in
MARCHE Claude's avatar
MARCHE Claude committed
21 22
  let _thread_id =
    Thread.create
23
      begin
MARCHE Claude's avatar
MARCHE Claude committed
24 25 26 27 28 29
        fun () ->
          try
            (* BEGIN LOCKED SECTION *)
            (* lock and store the attempt into the queue *)
            Mutex.lock queue_lock;
            Queue.push (prepare_goal,callback) attempts;
MARCHE Claude's avatar
MARCHE Claude committed
30
            callback Db.Scheduled;
MARCHE Claude's avatar
MARCHE Claude committed
31 32 33 34
            (* try to run attempt if resource available *)
            while !running_proofs < !maximum_running_proofs do
              let call,callback = Queue.pop attempts in
              incr running_proofs;
MARCHE Claude's avatar
MARCHE Claude committed
35
              callback Db.Running;
MARCHE Claude's avatar
MARCHE Claude committed
36
              Mutex.unlock queue_lock;
37
              (* END LOCKED SECTION *)
MARCHE Claude's avatar
MARCHE Claude committed
38
              let res = call () in
MARCHE Claude's avatar
MARCHE Claude committed
39 40
              (* BEGIN LOCKED SECTION *)
              Mutex.lock queue_lock;
MARCHE Claude's avatar
MARCHE Claude committed
41
              callback res;
MARCHE Claude's avatar
MARCHE Claude committed
42 43 44
              decr running_proofs;
            done;
            Mutex.unlock queue_lock
45
              (* END LOCKED SECTION *)
MARCHE Claude's avatar
MARCHE Claude committed
46 47 48 49
          with
            | Queue.Empty ->
                (* Queue was Empty *)
                Mutex.unlock queue_lock
50
                  (* END LOCKED SECTION *)
MARCHE Claude's avatar
MARCHE Claude committed
51
            | e ->
52
                (* any other exception should be propagated
MARCHE Claude's avatar
MARCHE Claude committed
53 54
                   after unlocking the lock *)
                Mutex.unlock queue_lock;
55
                (* END LOCKED SECTION *)
MARCHE Claude's avatar
MARCHE Claude committed
56 57 58 59 60
                raise e
      end
      ()
  in ()

61 62


MARCHE Claude's avatar
MARCHE Claude committed
63 64 65


(*
66
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
67
compile-command: "unset LANG; make -C ../.. bin/gwhy.byte"
68
End:
MARCHE Claude's avatar
MARCHE Claude committed
69
*)