Source file vio_checking.ml
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
143
open Util
let check_vio (ts,f_in) =
let _, _, _, tasks, _ = Library.load_library_todo f_in in
Stm.set_compilation_hints f_in;
List.fold_left (fun acc ids -> Stm.check_task f_in tasks ids && acc) true ts
module Worker = Spawn.Sync ()
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.user_err Pp.(str "The number of workers must be bigger than 0");
let jobs = ref [] in
List.iter (fun long_f_dot_vio ->
let _,_,_, tasks, _ = Library.load_library_todo long_f_dot_vio in
Stm.set_compilation_hints long_f_dot_vio;
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 := (long_f_dot_vio, 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;
Worker.kill (Pool.find pid !pool);
pool := Pool.remove pid !pool;
done;
exit !rc
let schedule_vio_compilation j fs =
if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0");
let jobs = ref [] in
List.iter (fun long_f_dot_vio ->
let aux = Aux_file.load_aux_file_for long_f_dot_vio in
let eta =
try float_of_string (Aux_file.get aux "vo_compile_time")
with Not_found -> 0.0 in
jobs := (long_f_dot_vio, 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 all_jobs = !jobs 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;
Worker.kill (Pool.find pid !pool);
pool := Pool.remove pid !pool;
done;
if !rc = 0 then begin
let t = Unix.gettimeofday () in
List.iter (fun (f,_) -> Unix.utimes (Filename.chop_extension f^".vo") t t) all_jobs;
end;
exit !rc