## lustrec/src/scheduling.ml @ aaa8e454

1 | a2d97a3e | ploc | ```
(********************************************************************)
``` |
---|---|---|---|

2 | ```
(* *)
``` |
||

3 | ```
(* The LustreC compiler toolset / The LustreC Development Team *)
``` |
||

4 | ```
(* Copyright 2012 - -- ONERA - CNRS - INPT *)
``` |
||

5 | ```
(* *)
``` |
||

6 | ```
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
``` |
||

7 | ```
(* under the terms of the GNU Lesser General Public License *)
``` |
||

8 | ```
(* version 2.1. *)
``` |
||

9 | ```
(* *)
``` |
||

10 | ```
(********************************************************************)
``` |
||

11 | 22fe1c93 | ploc | |

12 | open Utils |
||

13 | 8446bf03 | ploc | open Lustre_types |

14 | 22fe1c93 | ploc | open Corelang |

15 | open Causality |
||

16 | 95fb046e | ploc | open Scheduling_type |

17 | 22fe1c93 | ploc | |

18 | ```
(* Topological sort with a priority for variables belonging in the same equation lhs.
``` |
||

19 | ```
For variables still unrelated, standard compare is used to choose the minimal element.
``` |
||

20 | ```
This priority is used since it helps a lot in factorizing generated code.
``` |
||

21 | b1655a21 | xthirioux | ```
Moreover, the dependency graph is browsed in a depth-first manner whenever possible,
``` |

22 | ```
to improve the behavior of optimization algorithms applied in forthcoming compilation steps.
``` |
||

23 | 22fe1c93 | ploc | ```
In the following functions:
``` |

24 | ```
- [eq_equiv] is the equivalence relation between vars of the same equation lhs
``` |
||

25 | ```
- [g] the (imperative) graph to be topologically sorted
``` |
||

26 | ```
- [pending] is the set of unsorted root variables so far, equivalent to the last sorted var
``` |
||

27 | ```
- [frontier] is the set of unsorted root variables so far, not belonging in [pending]
``` |
||

28 | ```
- [sort] is the resulting topological order
``` |
||

29 | ```
*)
``` |
||

30 | a38c681e | xthirioux | |

31 | ```
(* Checks whether the currently scheduled variable [choice]
``` |
||

32 | ```
is an output of a call, possibly among others *)
``` |
||

33 | let is_call_output choice g = |
||

34 | 04d15b97 | xthirioux | List.exists ExprDep.is_instance_var (IdentDepGraph.succ g choice) |

35 | a38c681e | xthirioux | |

36 | 22fe1c93 | ploc | ```
(* Adds successors of [v] in graph [g] in [pending] or [frontier] sets, wrt [eq_equiv],
``` |

37 | ```
then removes [v] from [g]
``` |
||

38 | ```
*)
``` |
||

39 | let add_successors eq_equiv g v pending frontier = |
||

40 | let succs_v = IdentDepGraph.succ g v in |
||

41 | ```
begin
``` |
||

42 | IdentDepGraph.remove_vertex g v; |
||

43 | b84a138e | ploc | List.iter |

44 | (fun v' -> |
||

45 | if is_graph_root v' g then |
||

46 | (if eq_equiv v v' then |
||

47 | pending := ISet.add v' !pending |
||

48 | ```
else
``` |
||

49 | frontier := ISet.add v' !frontier) |
||

50 | ) succs_v; |
||

51 | 22fe1c93 | ploc | ```
end
``` |

52 | |||

53 | ```
(* Chooses the next var to be sorted, taking priority into account.
``` |
||

54 | ```
Modifies [pending] and [frontier] accordingly.
``` |
||

55 | ```
*)
``` |
||

56 | a38c681e | xthirioux | let next_element eq_equiv g sort call pending frontier = |

57 | 8ea13d96 | xthirioux | ```
begin
``` |

58 | if ISet.is_empty !pending |
||

59 | ```
then
``` |
||

60 | ```
begin
``` |
||

61 | let choice = ISet.min_elt !frontier in |
||

62 | 22fe1c93 | ploc | ```
(*Format.eprintf "-1-> %s@." choice;*)
``` |

63 | 8ea13d96 | xthirioux | frontier := ISet.remove choice !frontier; |

64 | let (p, f) = ISet.partition (eq_equiv choice) !frontier in |
||

65 | pending := p; |
||

66 | frontier := f; |
||

67 | a38c681e | xthirioux | call := is_call_output choice g; |

68 | 8ea13d96 | xthirioux | add_successors eq_equiv g choice pending frontier; |

69 | a38c681e | xthirioux | if not (ExprDep.is_ghost_var choice) |

70 | then sort := [choice] :: !sort |
||

71 | 8ea13d96 | xthirioux | ```
end
``` |

72 | ```
else
``` |
||

73 | ```
begin
``` |
||

74 | let choice = ISet.min_elt !pending in |
||

75 | 22fe1c93 | ploc | ```
(*Format.eprintf "-2-> %s@." choice;*)
``` |

76 | 8ea13d96 | xthirioux | pending := ISet.remove choice !pending; |

77 | add_successors eq_equiv g choice pending frontier; |
||

78 | a38c681e | xthirioux | if not (ExprDep.is_ghost_var choice) |

79 | then sort := (if !call |
||

80 | then (choice :: List.hd !sort) :: List.tl !sort |
||

81 | else [choice] :: !sort) |
||

82 | 8ea13d96 | xthirioux | ```
end
``` |

83 | ```
end
``` |
||

84 | |||

85 | 22fe1c93 | ploc | |

86 | ```
(* Topological sort of dependency graph [g], with priority.
``` |
||

87 | ```
*)
``` |
||

88 | let topological_sort eq_equiv g = |
||

89 | let roots = graph_roots g in |
||

90 | assert (roots <> []); |
||

91 | a38c681e | xthirioux | let call = ref false in |

92 | 22fe1c93 | ploc | let frontier = ref (List.fold_right ISet.add roots ISet.empty) in |

93 | let pending = ref ISet.empty in |
||

94 | let sorted = ref [] in |
||

95 | ```
begin
``` |
||

96 | while not (ISet.is_empty !frontier && ISet.is_empty !pending) |
||

97 | ```
do
``` |
||

98 | ```
(*Format.eprintf "frontier = {%a}, pending = {%a}@."
``` |
||

99 | ```
(fun fmt -> ISet.iter (fun e -> Format.pp_print_string fmt e)) !frontier
``` |
||

100 | ```
(fun fmt -> ISet.iter (fun e -> Format.pp_print_string fmt e)) !pending;*)
``` |
||

101 | a38c681e | xthirioux | next_element eq_equiv g sorted call pending frontier; |

102 | 22fe1c93 | ploc | done; |

103 | 8ea13d96 | xthirioux | IdentDepGraph.clear g; |

104 | 22fe1c93 | ploc | !sorted |

105 | ```
end
``` |
||

106 | |||

107 | 54d032f5 | xthirioux | ```
(* Filters out normalization variables and renames instance variables to keep things readable,
``` |

108 | ```
in a case of a dependency error *)
``` |
||

109 | let filter_original n vl = |
||

110 | List.fold_right (fun v res -> |
||

111 | if ExprDep.is_instance_var v then Format.sprintf "node %s" (ExprDep.undo_instance_var v) :: res else |
||

112 | let vdecl = get_node_var v n in |
||

113 | if vdecl.var_orig then v :: res else res) vl [] |
||

114 | |||

115 | f4cba4b8 | ploc | let eq_equiv eq_equiv_hash = |

116 | fun v1 v2 -> |
||

117 | ```
try
``` |
||

118 | Hashtbl.find eq_equiv_hash v1 = Hashtbl.find eq_equiv_hash v2 |
||

119 | with Not_found -> false |
||

120 | |||

121 | 7afcba5a | xthirioux | let schedule_node n = |

122 | 04a63d25 | xthirioux | ```
(* let node_vars = get_node_vars n in *)
``` |

123 | 7ee5f69e | Lélio Brun | Log.report ~level:5 (fun fmt -> Format.fprintf fmt "scheduling node %s@ " n.node_id); |

124 | f4cba4b8 | ploc | let eq_equiv = eq_equiv (ExprDep.node_eq_equiv n) in |

125 | cd670fe1 | ploc | |

126 | aaa8e454 | Lélio Brun | let node, g = global_dependency n in |

127 | e7cc5186 | ploc | |

128 | ```
(* TODO X: extend the graph with inputs (adapt the causality analysis to deal with inputs
``` |
||

129 | 0e1049dc | xthirioux | ```
compute: coi predecessors of outputs
``` |

130 | ```
warning (no modification) when memories are non used (do not impact output) or when inputs are not used (do not impact output)
``` |
||

131 | e7cc5186 | ploc | ```
DONE !
``` |

132 | ```
*)
``` |
||

133 | 0e1049dc | xthirioux | |

134 | aaa8e454 | Lélio Brun | let dep_graph = IdentDepGraph.copy g in |

135 | let schedule = topological_sort eq_equiv g in |
||

136 | let unused_vars = Liveness.compute_unused_variables n dep_graph in |
||

137 | let fanin_table = Liveness.compute_fanin n dep_graph in |
||

138 | { node; schedule; unused_vars; fanin_table; dep_graph } |
||

139 | ec433d69 | xthirioux | |

140 | f4cba4b8 | ploc | ```
(* let schedule_eqs eqs =
``` |

141 | ```
* let eq_equiv = eq_equiv (ExprDep.eqs_eq_equiv eqs) in
``` |
||

142 | ```
* assert false (\* TODO: continue to implement scheduling of eqs for spec *\) *)
``` |
||

143 | b1a97ade | xthirioux | |

144 | 04a63d25 | xthirioux | let compute_node_reuse_table report = |

145 | let disjoint = Disjunction.clock_disjoint_map (get_node_vars report.node) in |
||

146 | let reuse = Liveness.compute_reuse_policy report.node report.schedule disjoint report.dep_graph in |
||

147 | ```
(*
``` |
||

148 | 89a70069 | xthirioux | ```
if !Options.print_reuse
``` |

149 | ```
then
``` |
||

150 | ```
begin
``` |
||

151 | 790765c0 | xthirioux | ```
Log.report ~level:0
``` |

152 | ```
(fun fmt ->
``` |
||

153 | ```
Format.fprintf fmt
``` |
||

154 | ```
"OPT:%B@." (try (Hashtbl.iter (fun s1 v2 -> if s1 = v2.var_id then raise Not_found) reuse; false) with Not_found -> true)
``` |
||

155 | ```
);
``` |
||

156 | 89a70069 | xthirioux | ```
Log.report ~level:0
``` |

157 | ```
(fun fmt ->
``` |
||

158 | ```
Format.fprintf fmt
``` |
||

159 | ```
"OPT:clock disjoint map for node %s: %a"
``` |
||

160 | ```
n'.node_id
``` |
||

161 | ```
Disjunction.pp_disjoint_map disjoint
``` |
||

162 | ```
);
``` |
||

163 | ```
Log.report ~level:0
``` |
||

164 | ```
(fun fmt ->
``` |
||

165 | ```
Format.fprintf fmt
``` |
||

166 | ```
"OPT:reuse policy for node %s: %a"
``` |
||

167 | ```
n'.node_id
``` |
||

168 | ```
Liveness.pp_reuse_policy reuse
``` |
||

169 | ```
);
``` |
||

170 | ```
end;
``` |
||

171 | 04a63d25 | xthirioux | ```
*)
``` |

172 | ```
reuse
``` |
||

173 | |||

174 | 22fe1c93 | ploc | |

175 | 88486aaf | ploc | let schedule_prog prog = |

176 | List.fold_right ( |
||

177 | 3bfed7f9 | xthirioux | fun top_decl (accu_prog, sch_map) -> |

178 | 88486aaf | ploc | match top_decl.top_decl_desc with |

179 | f4050bef | ploc | | Node nd -> |

180 | 7ee5f69e | Lélio Brun | let report = schedule_node nd in |

181 | {top_decl with top_decl_desc = Node report.node}::accu_prog, |
||

182 | IMap.add nd.node_id report sch_map |
||

183 | | _ -> top_decl::accu_prog, sch_map |
||

184 | ```
)
``` |
||

185 | 88486aaf | ploc | ```
prog
``` |

186 | 3bfed7f9 | xthirioux | ([],IMap.empty) |

187 | 7ee5f69e | Lélio Brun | |

188 | 04a63d25 | xthirioux | |

189 | let compute_prog_reuse_table report = |
||

190 | IMap.map compute_node_reuse_table report |
||

191 | |||

192 | ```
(* removes inlined local variables from schedule report,
``` |
||

193 | ```
which are now useless *)
``` |
||

194 | let remove_node_inlined_locals locals report = |
||

195 | let is_inlined v = IMap.exists (fun l _ -> v = l) locals in |
||

196 | let schedule' = |
||

197 | List.fold_right (fun heads q -> let heads' = List.filter (fun v -> not (is_inlined v)) heads |
||

198 | in if heads' = [] then q else heads'::q) |
||

199 | report.schedule [] in |
||

200 | ```
begin
``` |
||

201 | IMap.iter (fun v _ -> Hashtbl.remove report.fanin_table v) locals; |
||

202 | IMap.iter (fun v _ -> let iv = ExprDep.mk_instance_var v |
||

203 | in Liveness.replace_in_dep_graph v iv report.dep_graph) locals; |
||

204 | { report with schedule = schedule' } |
||

205 | ```
end
``` |
||

206 | |||

207 | let remove_prog_inlined_locals removed reuse = |
||

208 | IMap.mapi (fun id -> remove_node_inlined_locals (IMap.find id removed)) reuse |
||

209 | 3bfed7f9 | xthirioux | |

210 | a38c681e | xthirioux | let pp_eq_schedule fmt vl = |

211 | match vl with |
||

212 | | [] -> assert false |
||

213 | | [v] -> Format.fprintf fmt "%s" v |
||

214 | | _ -> Format.fprintf fmt "(%a)" (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) vl |
||

215 | |||

216 | 8a183477 | xthirioux | let pp_schedule fmt node_schs = |

217 | IMap.iter |
||

218 | (fun nd report -> |
||

219 | 7ee5f69e | Lélio Brun | Format.(fprintf fmt "%s schedule: %a@ " |

220 | 8a183477 | xthirioux | ```
nd
``` |

221 | 7ee5f69e | Lélio Brun | (pp_print_list ~pp_sep:pp_print_semicolon pp_eq_schedule) |

222 | report.schedule)) |
||

223 | 8a183477 | xthirioux | ```
node_schs
``` |

224 | |||

225 | let pp_fanin_table fmt node_schs = |
||

226 | IMap.iter |
||

227 | (fun nd report -> |
||

228 | 7ee5f69e | Lélio Brun | Format.fprintf fmt "%s: %a@ " nd Liveness.pp_fanin report.fanin_table) |

229 | 04a63d25 | xthirioux | ```
node_schs
``` |

230 | |||

231 | let pp_dep_graph fmt node_schs = |
||

232 | IMap.iter |
||

233 | (fun nd report -> |
||

234 | 7ee5f69e | Lélio Brun | Format.fprintf fmt "%s dependency graph: %a@ " nd pp_dep_graph report.dep_graph) |

235 | 8a183477 | xthirioux | ```
node_schs
``` |

236 | |||

237 | 3bfed7f9 | xthirioux | let pp_warning_unused fmt node_schs = |

238 | 7ee5f69e | Lélio Brun | IMap.iter |

239 | (fun nd report -> |
||

240 | let unused = report.unused_vars in |
||

241 | if not (ISet.is_empty unused) |
||

242 | ```
then
``` |
||

243 | let nd = match (Corelang.node_from_name nd).top_decl_desc with Node nd -> nd | _ -> assert false in |
||

244 | ISet.iter |
||

245 | (fun u -> |
||

246 | let vu = get_node_var u nd in |
||

247 | if vu.var_orig |
||

248 | then Format.fprintf fmt " Warning: variable '%s' seems unused@, %a@,@," u Location.pp_loc vu.var_loc) |
||

249 | ```
unused
``` |
||

250 | ```
)
``` |
||

251 | ```
node_schs
``` |
||

252 | 22fe1c93 | ploc | |

253 | 04a63d25 | xthirioux | |

254 | 25320f03 | ploc | ```
(* Sort eqs according to schedule *)
``` |

255 | eb9a8c3c | ploc | ```
(* Sort the set of equations of node [nd] according
``` |

256 | ```
to the computed schedule [sch]
``` |
||

257 | ```
*)
``` |
||

258 | 5de4dde4 | ploc | let sort_equations_from_schedule eqs sch = |

259 | 2db953dd | ploc | Log.report ~level:10 (fun fmt -> |

260 | 7ee5f69e | Lélio Brun | Format.fprintf fmt "schedule: %a@ " |

261 | (Format.pp_print_list |
||

262 | ~pp_sep:Format.pp_print_semicolon pp_eq_schedule) sch); |
||

263 | eb9a8c3c | ploc | let split_eqs = Splitting.tuple_split_eq_list eqs in |

264 | 2db953dd | ploc | ```
(* Flatten schedule *)
``` |

265 | e8f55c25 | ploc | let sch = List.fold_right (fun vl res -> (List.map (fun v -> [v]) vl)@res) sch [] in |

266 | eb9a8c3c | ploc | let eqs_rev, remainder = |

267 | List.fold_left |
||

268 | (fun (accu, node_eqs_remainder) vl -> |
||

269 | 2db953dd | ploc | ```
(* For each variable in vl, there should exists the equations in accu *)
``` |

270 | if List.for_all (fun v -> List.exists (fun eq -> List.mem v eq.eq_lhs) accu) vl |
||

271 | eb9a8c3c | ploc | ```
then
``` |

272 | (accu, node_eqs_remainder) |
||

273 | ```
else
``` |
||

274 | let eq_v, remainder = find_eq vl node_eqs_remainder in |
||

275 | eq_v::accu, remainder |
||

276 | ```
)
``` |
||

277 | ([], split_eqs) |
||

278 | ```
sch
``` |
||

279 | ```
in
``` |
||

280 | ```
begin
``` |
||

281 | 25320f03 | ploc | let eqs = List.rev eqs_rev in |

282 | let unused = |
||

283 | if List.length remainder > 0 then ( |
||

284 | Log.report ~level:3 (fun fmt -> Format.fprintf fmt |
||

285 | ```
"[Warning] Equations not used are@ %a@ Full equation set is:@ %a@ "
``` |
||

286 | Printers.pp_node_eqs remainder |
||

287 | Printers.pp_node_eqs eqs |
||

288 | ```
);
``` |
||

289 | let vars = List.fold_left (fun accu eq -> eq.eq_lhs @ accu) [] remainder in |
||

290 | Log.report ~level:1 (fun fmt -> Format.fprintf fmt |
||

291 | ```
"[Warning] Unused variables: %a@ "
``` |
||

292 | (fprintf_list ~sep:", " Format.pp_print_string) |
||

293 | ```
vars
``` |
||

294 | ```
);
``` |
||

295 | ```
vars
``` |
||

296 | ```
)
``` |
||

297 | ```
else
``` |
||

298 | ```
[]
``` |
||

299 | ```
in
``` |
||

300 | eqs, unused |
||

301 | eb9a8c3c | ploc | ```
end
``` |

302 | |||

303 | 22fe1c93 | ploc | ```
(* Local Variables: *)
``` |

304 | ```
(* compile-command:"make -C .." *)
``` |
||

305 | ```
(* End: *)
``` |