bench.ml 18.1 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
MARCHE Claude's avatar
MARCHE Claude committed
8 9 10 11 12 13 14 15 16 17 18 19 20
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

21
open Thread
22
open Why3
23
open Util
24 25 26 27 28 29 30
open Env
open Theory
open Task
open Trans
open Driver
open Call_provers

31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
type tool_id = {
  tool_name : string;
  prover_name : string;
  tool_db : Db.prover_id option;
  }
(* tool_name, prover_name *)

type prob_id = {
  prob_name : string;
  prob_file : string;
  prob_theory : string;
  prob_db : Db.goal option;
}
(* prob_name, file_name, theory name *)

type tool = {
  tval     : tool_id;
  ttrans   : (task trans * (Db.transf_id option)) list;
49 50 51
  tdriver  : driver;
  tcommand : string;
  tenv     : env;
52
  tuse     : (theory * Db.transf_id option) list;
53 54 55 56
  ttime    : int;
  tmem     : int;
}

57 58 59
type gen_task = env -> (theory * Db.transf_id option) list ->
    (prob_id * task) list

60
type prob = {
61 62
  ptask  : gen_task;
  (** needed for tenv *)
63
  ptrans : env -> (task list trans * (Db.transf_id option)) list;
64 65
}

66 67
type why_result =
  | InternalFailure of exn
68
  | Done of Db.proof_status * float
69

70 71 72 73 74
type result = {tool   : tool_id;
               prob   : prob_id;
               task   : Decl.prsymbol;
               idtask : int;
               result : why_result}
75

76 77 78 79 80 81 82

type proof_attempt_status =
  | Runned of why_result
  | Cached of Db.proof_status * float

open Format

83
type callback = tool_id -> prob_id ->
84 85
    task -> int ->  proof_attempt_status -> unit

86
let debug_call = Debug.register_info_flag "call"
87
  ~desc:"Show when call to provers are done"
88
let debug = Debug.register_info_flag "bench_core"
89
  ~desc:"About the scheduling"
90

91 92 93 94 95

module BenchUtil =
struct

  let print_proof_status fmt = function
96 97
    | Db.Done a -> Call_provers.print_prover_answer fmt a
    | Db.Undone -> fprintf fmt "Undone"
98 99

  open Worker
100

101
(* number of scheduled external proofs *)
102
  let coef_buf = 10
103 104
  let scheduled_proofs = ref 0
  let maximum_running_proofs = ref 2
105 106

(* they are protected by a lock *)
107 108 109
  let answers_queue = Queue.create ()
  let queue_lock = Mutex.create ()
  let queue_condition = Condition.create ()
110

111
(** Before calling this function queue_lock must be locked *)
112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131
  let treat_result () =
    let q_tmp = Queue.create () in
    while not (Queue.is_empty answers_queue) do
      Queue.transfer answers_queue q_tmp;
      Mutex.unlock queue_lock;
      let iter (result,callback) = decr scheduled_proofs; callback (result ())
      in
      Queue.iter iter q_tmp;
      Queue.clear q_tmp;
      Mutex.lock queue_lock
    done

  let yield () =
    Thread.yield ();
    Mutex.lock queue_lock;
    treat_result ();
    Mutex.unlock queue_lock

  (** Wait for the last remaining tasks *)
  let wait_remaining_task () =
132
    Mutex.lock queue_lock;
133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152
    while !scheduled_proofs > 0 do
      while Queue.is_empty answers_queue do
        Condition.wait queue_condition queue_lock
      done;
      treat_result ();
    done;
    Mutex.unlock queue_lock

  let new_external_proof =
    let run_external (call_prover,callback) =
      let r = Call_provers.wait_on_call (call_prover ()) in
      Mutex.lock queue_lock;
      Queue.push (r,callback) answers_queue ;
      Condition.signal queue_condition;
      Mutex.unlock queue_lock in
    let external_workers =
      ManyWorkers.create maximum_running_proofs run_external in
    fun (call_prover,callback) ->
      ManyWorkers.add_work external_workers (call_prover,callback);
      incr scheduled_proofs;
153
    (** Stop the computation if too many external proof are scheduled *)
154
      while !scheduled_proofs >= !maximum_running_proofs * coef_buf do
155 156 157 158 159 160
        Mutex.lock queue_lock;
        while Queue.is_empty answers_queue do
          Condition.wait queue_condition queue_lock
        done;
        treat_result ();
        Mutex.unlock queue_lock;
161
      done
162

163

164
(* from Gmain *)
165 166 167 168 169 170 171 172 173 174 175 176 177 178
  let task_checksum t =
    fprintf str_formatter "%a@." Pretty.print_task t;
    let s = flush_str_formatter () in
    Digest.to_hex (Digest.string s)


  let apply_trans (task,db_goal) (trans,db_trans) =
    let task = Trans.apply trans task in
    match db_goal, db_trans with
      | Some db_goal, Some db_trans ->
        let transf = try Db.Htransf.find (Db.transformations db_goal) db_trans
          with Not_found ->
            Db.add_transformation db_goal db_trans
        in
179 180 181 182 183 184 185 186 187
        let md5 = task_checksum task in
        let db_goal =
          try
            Mstr.find md5 (Db.subgoals transf)
          with Not_found ->
            Db.add_subgoal transf
              (Task.task_goal task).Decl.pr_name.Ident.id_string
              md5
        in
188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
        (task,Some db_goal)
      | _ -> ((task:task),None)

  let apply_transl (task,db_goal) (trans,db_trans) =
    let tasks = Trans.apply trans task in
    match db_goal, db_trans with
      | Some db_goal, Some db_trans ->
        let transf = try Db.Htransf.find (Db.transformations db_goal) db_trans
          with Not_found -> Db.add_transformation db_goal db_trans
        in
        let map task =
          let md5 = task_checksum task in
          let db_goal =
            try
              Mstr.find md5 (Db.subgoals transf)
            with Not_found ->
              Db.add_subgoal transf
                (Task.task_goal task).Decl.pr_name.Ident.id_string
                md5
          in
          (task,Some db_goal) in
        List.map map tasks
      | _ -> List.map (fun task -> (task:task),None) tasks


  let rec apply_transll trl acc (task,db_goal) =
    match trl with
      | [] -> (task,db_goal)::acc
      | tr::trl ->
        let tl = apply_transl (task,db_goal) tr in
        List.fold_left (apply_transll trl) acc tl

220
  let proof_status_to_db_result pr = (Db.Done pr.pr_answer, pr.pr_time)
221

222
end
223 224


225 226 227 228 229 230 231 232 233
let print_why_result fmt = function
  | InternalFailure exn ->
    Format.fprintf fmt "InternalFailure %a" Exn_printer.exn_printer exn
  | Done (pr,_) -> BenchUtil.print_proof_status fmt pr

let print_pas fmt = function
  | Runned sp -> fprintf fmt "Runned %a" print_why_result sp
  | Cached (p,t) -> fprintf fmt "Cached (%a,%f)"
    BenchUtil.print_proof_status p t
234

235
let call callback tool prob =
236
  (** Prove goal *)
237 238 239 240 241 242
  let db_tool = tool.tval.tool_db in
  let new_external_proof pval i cb task =
    try
      let call_prover : Call_provers.pre_prover_call =
        Driver.prove_task ~timelimit:(tool.ttime) ~memlimit:(tool.tmem)
          ~command:(tool.tcommand) (tool.tdriver) task in
243
      BenchUtil.new_external_proof (call_prover,cb)
244 245
    with e ->
      Format.eprintf "%a@." Exn_printer.exn_printer e;
246
      callback pval i task (Runned (InternalFailure e)) in
247 248 249 250 251
  let call pval i (task,db_goal) =
    match db_goal,db_tool with
      | Some db_goal, Some db_tool ->
        let proof_attempt =
          try
252 253
            Db.Hprover.find (Db.external_proofs db_goal) db_tool
          with Not_found ->
254
            Db.add_proof_attempt db_goal db_tool
255
        in
256
        let (proof_status,time,_,_) = Db.status_and_time proof_attempt in
257
        Debug.dprintf debug "Database has (%a,%f) for the goal@."
258
          BenchUtil.print_proof_status proof_status time;
259
        begin
260 261
          if proof_status = Db.Done Call_provers.Valid ||
            (proof_status = Db.Done Call_provers.Timeout &&
262
                time > float tool.ttime)
263
          then
264 265
            callback pval i task (Cached (proof_status,time))
          else
266 267 268 269
            begin
              Debug.dprintf debug "@.time = %f %i@.@."
                time tool.ttime;
              let cb res =
270
                let (status,time) = BenchUtil.proof_status_to_db_result res in
271 272 273 274 275
                callback pval i task (Runned (Done (status,time)));
                Db.set_status proof_attempt status time
              in
              new_external_proof pval i cb task
            end
276 277
        end
      | _ ->
278
        let cb res =
279
          let (status,time) = BenchUtil.proof_status_to_db_result res in
280
          callback pval i task (Runned (Done (status,time))) in
281
        new_external_proof pval i cb task
282
  in
283 284
  (** Apply trans *)
  let iter_task (pval,task) =
285
    let translist = prob.ptrans tool.tenv in
286
    let tasks = BenchUtil.apply_transll translist [] (task,pval.prob_db) in
287
    let tasks = List.map
288 289 290
      (fun task -> List.fold_left BenchUtil.apply_trans task tool.ttrans)
      tasks
    in
291
    let iter i task = call pval i task; succ i in
292
    ignore (List.fold_left iter 0 (List.rev tasks)) in
293
  (** Split *)
294 295 296
  let ths = prob.ptask tool.tenv tool.tuse in
  List.iter iter_task ths

297 298

let general ?(callback=fun _ _ _ _ _ -> ()) iter add =
299
  Debug.dprintf debug "Start one general@.";
300 301
  (** Main worker *)
  (** Start all *)
302
  iter (fun v tool prob ->
303
    let cb pval i task res =
304 305 306 307
      callback tool.tval pval task i res;
      add v {tool = tool.tval; prob = pval;
             task = Task.task_goal task;
             idtask = i;
308 309 310
             result = match res with
               | Runned res -> res
               | Cached (res,time) -> Done (res,time)
311 312
            } in
    call cb tool prob);
313
  BenchUtil.wait_remaining_task ()
314 315 316 317 318 319 320 321

let any ?callback toolprob =
  let l = ref [] in
  general ?callback (fun f -> List.iter (fun (t,p) -> f () t p) toolprob)
    (fun () r -> l:=r::!l);
  !l


322
let all_list_tp ?callback tools probs =
323 324 325 326 327 328
  let l = ref [] in
  general ?callback (fun f ->
    List.iter (fun t -> List.iter (fun p -> f () t p) probs) tools)
    (fun () r -> l:=r::!l);
  !l

329 330 331 332 333 334 335
let all_list_pt ?callback tools probs =
  let l = ref [] in
  general ?callback (fun f ->
    List.iter (fun p -> List.iter (fun t -> f () t p) tools) probs)
    (fun () r -> l:=r::!l);
  !l

336 337 338 339 340 341 342
let all_array ?callback tools probs =
  let m = Array.make_matrix (Array.length tools) (Array.length probs)
    [] in
  general ?callback (fun f ->
    Array.iteri (fun i t -> Array.iteri (fun j p -> f (i,j) t p) probs) tools)
    (fun (i,j) r -> m.(i).(j) <- r::m.(i).(j));
  m
343 344 345 346 347 348 349 350 351 352 353


let all_list_tools ?callback tools probs =
  let tools = List.map (fun t -> (t, ref [])) tools in
  general ?callback (fun f ->
    List.iter (fun (t,l) -> List.iter (fun p -> f l t p) probs) tools)
    (fun l r -> l:=r::!l);
  List.map (fun (t,l) -> (t.tval,!l)) tools

type output =
  (** on stdout *)
François Bobot's avatar
François Bobot committed
354 355
  |Average of string
  |Timeline of string
356
  (** In a file *)
François Bobot's avatar
François Bobot committed
357
  |Csv of string
358

359
type bench =
360
    {
François Bobot's avatar
François Bobot committed
361
      bname  : string;
362 363
      btools : tool list;
      bprobs : prob list;
364 365 366 367
      boutputs : output list;
    }

let run_bench ?callback bench =
368
  all_list_pt ?callback bench.btools bench.bprobs
369 370 371 372 373 374 375 376 377 378 379 380 381 382 383

let run_benchs ?callback benchs =
  let benchs = List.map (fun b -> (b,ref [])) benchs in
  general ?callback (fun f ->
    List.iter (fun (b,l) ->
    List.iter (fun t -> List.iter (fun p -> f l t p) b.bprobs)
      b.btools) benchs)
    (fun l r -> l:=r::!l);
  List.map (fun (b,l) -> (b,!l)) benchs

let run_benchs_tools ?callback benchs =
  let benchs = List.map (fun b ->
    b, List.map (fun t -> t,ref []) b.btools) benchs in
  general ?callback (fun f ->
    List.iter (fun (b,l) ->
384 385
    List.iter (fun p -> List.iter (fun (t,l) -> f l t p) l)
      b.bprobs) benchs)
386 387 388 389
    (fun l r -> l:=r::!l);
  List.map (fun (b,l) -> b,List.map (fun (t,l) -> t.tval,!l) l) benchs


390

391 392 393 394 395 396 397 398 399
(** average *)

(** valid * timeout * unknown * invalid  *)
type nb_avg = int * float

let add_nb_avg (nb,avg) time =
  (succ nb, ((float nb) *. avg +. time) /. (float (succ nb)))
let empty_nb_avg = (0,0.)

400
let print_nb_avg fmt (nb,avg) = fprintf fmt "%i : %.2f" nb avg
401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417

type tool_res =
    { valid : nb_avg;
      timeout : nb_avg;
      unknown : nb_avg;
      invalid : nb_avg;
      failure : nb_avg}

let empty_tool_res =
  { valid   = empty_nb_avg;
    timeout = empty_nb_avg;
    unknown = empty_nb_avg;
    invalid = empty_nb_avg;
    failure = empty_nb_avg;
  }

  let print_tool_res fmt tool_res =
418
    fprintf fmt "(%a, %a, %a, %a, %a)"
419 420 421 422 423 424 425 426 427
      print_nb_avg tool_res.valid
      print_nb_avg tool_res.unknown
      print_nb_avg tool_res.timeout
      print_nb_avg tool_res.invalid
      print_nb_avg tool_res.failure

  let compute_average l =
  let fold tr res =
    let r = res.result in
428
    match r with
429 430
      | Done (answer,time) ->
        begin match answer with
431 432 433 434 435 436
          | Db.Done Call_provers.Valid ->
              {tr with valid = add_nb_avg tr.valid time}
          | Db.Done Call_provers.Timeout ->
              {tr with timeout = add_nb_avg tr.timeout time}
          | Db.Done Call_provers.Invalid ->
              {tr with invalid = add_nb_avg tr.invalid time}
Andrei Paskevich's avatar
Andrei Paskevich committed
437
          | Db.Done Call_provers.OutOfMemory
438 439 440 441 442
          | Db.Undone | Db.Done (Call_provers.Unknown _) ->
              {tr with unknown = add_nb_avg tr.unknown time}
          | Db.Done (Call_provers.Failure _)
          | Db.Done Call_provers.HighFailure ->
              {tr with failure = add_nb_avg tr.failure time}
443 444
        end
      | InternalFailure _ ->
445
          {tr with failure = add_nb_avg tr.failure 0.} in
446 447
    List.fold_left fold empty_tool_res l

448 449
  let extract_time = function Done (_,t) -> t
    | InternalFailure _ -> assert false
450

451
  let filter_timeline l =
452 453
    let l = List.filter (function
      | {result = Done (Db.Done Call_provers.Valid,_)} -> true
454
      | _ -> false) l in
455
    let compare_valid x y =
456 457
      let c = compare (extract_time x.result)
        (extract_time y.result) in
458 459 460 461 462 463 464 465
      if c <> 0 then c else compare x y in
    let l = List.fast_sort compare_valid l in
    l

  let compute_timeline min max step =
    let rec aux acc cur next = function
      | _ when next > max -> List.rev acc
      | [] -> aux (cur::acc) cur (next+.step) []
466
      | {result= InternalFailure _}::l -> aux acc cur next l
467
      | {result= Done (_,t)}::_ as l when t >= next ->
468 469 470 471 472
        aux (cur::acc) cur (next+.step) l
      | _::l -> aux acc (cur+1) next l in
    aux [] 0 min

  let max_time l =
473 474
    List.fold_left (fun acc {result=r} ->
      match r with
475
        | Done (_,t) -> max acc t
476
        | InternalFailure _ -> acc ) 0. l
François Bobot's avatar
François Bobot committed
477 478 479 480 481 482 483 484 485
  open Format
(**
answer output time

*)


  let print_newline fmt () = fprintf fmt "\n"

486 487 488
  let transpose_sorted = function
    | [] -> []
    | (_,lres)::_ as l ->
489
    let lref = List.map (fun r -> (r.prob,r.task,r.idtask),ref []) lres in
490 491 492 493 494 495
    let l = List.rev l in
    let add (_,lr) res = lr := res :: !lr in
    List.iter (fun (_,lres) -> List.iter2 add lref lres) l;
    List.map (fun (b,lr) -> b,!lr) lref

  let print_csv cmp print_tool print_prob fmt l =
François Bobot's avatar
François Bobot committed
496 497 498
    let cmp x y =
      let c = cmp x.prob y.prob in
      if c <> 0 then c else
499
        let id x = x.task.Decl.pr_name.Ident.id_string in
François Bobot's avatar
François Bobot committed
500 501 502
        let c = String.compare (id x) (id y) in
        if c <> 0 then c else compare x.idtask y.idtask in
    let l = List.map (fun (p,l) -> p,List.fast_sort cmp l) l in
503 504 505
    fprintf fmt " ,";
    let print_header fmt (p,_) = fprintf fmt "%a, " print_tool p in
    Pp.print_list Pp.comma print_header fmt l;
François Bobot's avatar
François Bobot committed
506
    print_newline fmt ();
507
    let l = transpose_sorted l in
508 509
    let print_cell fmt {result= r} =
      match r with
510
        | Done (answer,time) ->
511
          fprintf fmt "%a, %.3f" (*"%a, %S, %.3f"*)
512
            BenchUtil.print_proof_status answer (*r.result.pr_output*)
513
            time
514 515
        | InternalFailure _ -> fprintf fmt "InternalFailure, \"\""
in
516 517 518 519
    let print_line fmt ((b,t,id),l) =
      (* No printer for task since we want the same name evenif its
         the same file with different environnement (loaded two times) *)
      fprintf fmt "%a|%s|%i ," print_prob b
520
        t.Decl.pr_name.Ident.id_string
521
        id;
François Bobot's avatar
François Bobot committed
522 523 524 525 526 527 528 529 530 531
      Pp.print_list Pp.comma print_cell fmt l in
    Pp.print_list print_newline print_line fmt l

  let print_timeline print_tool fmt l =
    let l = List.map (fun (t,l) -> t,filter_timeline l) l in
    let max = List.fold_left (fun acc (_,l) -> max acc (max_time l)) 0. l in
    let max = max +. 0.1 in
    let step = max /. 10. in
    let tl = List.map (fun (t,l) -> t,compute_timeline 0. max step l) l in
    let print_timeline (tool_val,timeline) =
532
      fprintf fmt "%a - %a\n"
François Bobot's avatar
François Bobot committed
533 534
        (Pp.print_list Pp.comma (fun fmt -> fprintf fmt "%4i"))
        timeline print_tool tool_val in
535
    fprintf fmt "%a\n"
François Bobot's avatar
François Bobot committed
536 537 538 539 540 541 542 543 544
      (Pp.print_iter1 (fun f -> Util.iterf f 0. max)
         Pp.comma (fun fmt -> fprintf fmt "%3.2f"))
      step;
    List.iter print_timeline tl


  let print_average print_tool fmt l =
    let tool_res = List.map (fun (t,l) -> t,compute_average l) l in
    let print_tool_res (tool_val,tool_res) =
545
      fprintf fmt "%a - %a\n" print_tool_res tool_res print_tool tool_val in
François Bobot's avatar
François Bobot committed
546
    fprintf fmt "(v,u,t,i,f) - valid, unknown, timeout, invalid, failure\n";
François Bobot's avatar
François Bobot committed
547 548 549 550 551 552 553 554 555 556 557 558 559 560
    List.iter print_tool_res tool_res


  let print_output cmp print_tool print_probs (b,l) =
    let open_std f s =
      if s = "-"
      then begin f std_formatter;pp_print_flush std_formatter () end
      else
        let cout = (open_out s) in
        let fmt = (formatter_of_out_channel cout) in
        f fmt;
        pp_print_flush fmt ();
        close_out cout in
    List.iter (function
561 562 563 564 565 566
      | Average s -> open_std (fun fmt ->
        Pp.wnl fmt;
        print_average print_tool fmt l) s
      | Timeline s -> open_std (fun fmt ->
        Pp.wnl fmt;
        print_timeline print_tool fmt l) s
François Bobot's avatar
François Bobot committed
567 568 569 570
      | Csv s ->
        open_std (fun fmt -> Pp.wnl fmt;
          print_csv cmp print_tool print_probs fmt l) s
    ) b.boutputs
571 572