summaryrefslogtreecommitdiff
path: root/stm/vio_checking.ml
blob: a6237daa046c70fa6944004cb00126f61e6a8caa (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Util

let check_vio (ts,f) =
  Dumpglob.noglob ();
  let long_f_dot_v, _, _, _, _, tasks, _ = Library.load_library_todo f in
  Stm.set_compilation_hints long_f_dot_v;
  List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts

module Worker = Spawn.Sync(struct end)

module IntOT = struct
  type t = int
  let compare = compare
end

module Pool = Map.Make(IntOT)

let schedule_vio_checking j fs =
  if j < 1 then CErrors.error "The number of workers must be bigger than 0";
  let jobs = ref [] in
  List.iter (fun f ->
    let f =
      if Filename.check_suffix f ".vio" then Filename.chop_extension f
      else f in
    let long_f_dot_v, _,_,_,_, tasks, _ = Library.load_library_todo f in
    Stm.set_compilation_hints long_f_dot_v;
    let infos = Stm.info_tasks tasks in
    let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
    if infos <> [] then jobs := (f, eta, infos) :: !jobs)
  fs;
  let cmp_job (_,t1,_) (_,t2,_) = compare t2 t1 in
  jobs := List.sort cmp_job !jobs;
  let eta = ref (List.fold_left (fun a j -> a +. pi2 j) 0.0 !jobs) in
  let pool : Worker.process Pool.t ref = ref Pool.empty in
  let rec filter_argv b = function
    | [] -> []
    | "-schedule-vio-checking" :: rest -> filter_argv true rest
    | s :: rest when String.length s > 0 && s.[0] = '-' && b -> filter_argv false (s :: rest)
    | _ :: rest when b -> filter_argv b rest
    | s :: rest -> s :: filter_argv b rest in
  let pack = function
    | [] -> []
    | ((f,_),_,_) :: _ as l ->
        let rec aux last acc = function
          | [] -> [last,acc]
          | ((f',id),_,_) :: tl when last = f' -> aux last (id::acc) tl
          | ((f',id),_,_) :: _ as l -> (last,acc) :: aux f' [] l in
        aux f [] l in
  let prog = Sys.argv.(0) in  
  let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in
  let make_job () =
    let cur = ref 0.0 in
    let what = ref [] in
    let j_left = j - Pool.cardinal !pool in
    let take_next_file () =
      let f, t, tasks = List.hd !jobs in
      jobs := List.tl !jobs;
      cur := !cur +. t;
      what := (List.map (fun (n,t,id) -> (f,id),n,t) tasks) @ !what in
    if List.length !jobs >= j_left then take_next_file ()
    else while !jobs <> [] &&
         !cur < max 0.0 (min 60.0 (!eta /. float_of_int j_left)) do
      let f, t, tasks = List.hd !jobs in
      jobs := List.tl !jobs;
      let n, tt, id = List.hd tasks in
      if List.length tasks > 1 then
        jobs := (f, t -. tt, List.tl tasks) :: !jobs;
      cur := !cur +. tt;
      what := ((f,id),n,tt) :: !what;
    done;
    if !what = [] then take_next_file ();
    eta := !eta -. !cur;
    let cmp_job (f1,_,_) (f2,_,_) = compare f1 f2 in
    List.flatten
      (List.map (fun (f, tl) ->
        "-check-vio-tasks" :: 
        String.concat "," (List.map string_of_int tl) :: [f])
      (pack (List.sort cmp_job !what))) in
  let rc = ref 0 in
  while !jobs <> [] || Pool.cardinal !pool > 0 do
    while Pool.cardinal !pool < j && !jobs <> [] do
      let args = Array.of_list (stdargs @ make_job ()) in
      let proc, _, _ = Worker.spawn prog args in
      pool := Pool.add (Worker.unixpid proc) proc !pool;
    done;
    let pid, ret = Unix.wait () in
    if ret <> Unix.WEXITED 0 then rc := 1;
    pool := Pool.remove pid !pool;
  done;
  exit !rc

let schedule_vio_compilation j fs =
  if j < 1 then CErrors.error "The number of workers must be bigger than 0";
  let jobs = ref [] in
  List.iter (fun f ->
    let f =
      if Filename.check_suffix f ".vio" then Filename.chop_extension f
      else f in
    let long_f_dot_v = Loadpath.locate_file (f^".v") in
    let aux = Aux_file.load_aux_file_for long_f_dot_v in
    let eta =
      try float_of_string (Aux_file.get aux Loc.ghost "vo_compile_time")
      with Not_found -> 0.0 in
    jobs := (f, eta) :: !jobs)
  fs;
  let cmp_job (_,t1) (_,t2) = compare t2 t1 in
  jobs := List.sort cmp_job !jobs;
  let pool : Worker.process Pool.t ref = ref Pool.empty in
  let rec filter_argv b = function
    | [] -> []
    | "-schedule-vio2vo" :: rest -> filter_argv true rest
    | s :: rest when String.length s > 0 && s.[0] = '-' && b -> filter_argv false (s :: rest)
    | _ :: rest when b -> filter_argv b rest
    | s :: rest -> s :: filter_argv b rest in
  let prog = Sys.argv.(0) in  
  let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in
  let make_job () =
    let f, t = List.hd !jobs in
    jobs := List.tl !jobs;
    [ "-vio2vo"; f ] in
  let rc = ref 0 in
  while !jobs <> [] || Pool.cardinal !pool > 0 do
    while Pool.cardinal !pool < j && !jobs <> [] do
      let args = Array.of_list (stdargs @ make_job ()) in
      let proc, _, _ = Worker.spawn prog args in
      pool := Pool.add (Worker.unixpid proc) proc !pool;
    done;
    let pid, ret = Unix.wait () in
    if ret <> Unix.WEXITED 0 then rc := 1;
    pool := Pool.remove pid !pool;
  done;
  exit !rc