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_flag "call"
87
  ~desc:"Show when call to provers are done"
88
let debug = Debug.register_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