lustrec / src / causality.ml @ 22fe1c93
History | View | Annotate | Download (13.3 KB)
1 |
(* ---------------------------------------------------------------------------- |
---|---|
2 |
* SchedMCore - A MultiCore Scheduling Framework |
3 |
* Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
4 |
* |
5 |
* This file is part of Prelude |
6 |
* |
7 |
* Prelude is free software; you can redistribute it and/or |
8 |
* modify it under the terms of the GNU Lesser General Public License |
9 |
* as published by the Free Software Foundation ; either version 2 of |
10 |
* the License, or (at your option) any later version. |
11 |
* |
12 |
* Prelude is distributed in the hope that it will be useful, but |
13 |
* WITHOUT ANY WARRANTY ; without even the implied warranty of |
14 |
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
15 |
* Lesser General Public License for more details. |
16 |
* |
17 |
* You should have received a copy of the GNU Lesser General Public |
18 |
* License along with this program ; if not, write to the Free Software |
19 |
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
20 |
* USA |
21 |
*---------------------------------------------------------------------------- *) |
22 |
|
23 |
|
24 |
(** Simple modular syntactic causality analysis. Can reject correct |
25 |
programs, especially if the program is not flattened first. *) |
26 |
open Utils |
27 |
open LustreSpec |
28 |
open Corelang |
29 |
open Graph |
30 |
open Format |
31 |
|
32 |
exception Cycle of ident list |
33 |
|
34 |
module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule) |
35 |
|
36 |
(*module IdentDepGraphUtil = Oper.P(IdentDepGraph)*) |
37 |
|
38 |
(* Dependency of mem variables on mem variables is cut off |
39 |
by duplication of some mem vars into local node vars. |
40 |
Thus, cylic dependency errors may only arise between no-mem vars. |
41 |
|
42 |
no_mem' = combinational(no_mem, mem); |
43 |
=> (mem -> no_mem' -> no_mem) |
44 |
|
45 |
mem' = pre(no_mem, mem); |
46 |
=> (mem' -> no_mem), (mem -> mem') |
47 |
|
48 |
Global roadmap: |
49 |
- compute two dep graphs g (non-mem/non-mem&mem) and g' (mem/mem) |
50 |
- check cycles in g (a cycle means a dependency error) |
51 |
- break cycles in g' (it's legal !): |
52 |
- check cycles in g' |
53 |
- if any, introduce aux var to break cycle, then start afresh |
54 |
- insert g' into g |
55 |
- return g |
56 |
*) |
57 |
|
58 |
let add_edges src tgt g = |
59 |
(*List.iter (fun s -> List.iter (fun t -> Format.eprintf "add %s -> %s@." s t) tgt) src;*) |
60 |
List.iter |
61 |
(fun s -> |
62 |
List.iter |
63 |
(fun t -> IdentDepGraph.add_edge g s t) |
64 |
tgt) |
65 |
src; |
66 |
g |
67 |
|
68 |
let add_vertices vtc g = |
69 |
(*List.iter (fun t -> Format.eprintf "add %s@." t) vtc;*) |
70 |
List.iter (fun v -> IdentDepGraph.add_vertex g v) vtc; |
71 |
g |
72 |
|
73 |
let new_graph () = |
74 |
IdentDepGraph.create () |
75 |
|
76 |
module ExprDep = struct |
77 |
|
78 |
let eq_var_cpt = ref 0 |
79 |
|
80 |
let instance_var_cpt = ref 0 |
81 |
|
82 |
let mk_eq_var id = |
83 |
incr eq_var_cpt; sprintf "#%s_%d" id !eq_var_cpt |
84 |
|
85 |
let mk_instance_var id = |
86 |
incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt |
87 |
|
88 |
let is_eq_var v = v.[0] = '#' |
89 |
|
90 |
let is_instance_var v = v.[0] = '!' |
91 |
|
92 |
let is_ghost_var v = is_instance_var v || is_eq_var v |
93 |
|
94 |
let eq_memory_variables mems eq = |
95 |
let rec match_mem lhs rhs mems = |
96 |
match rhs.expr_desc with |
97 |
| Expr_fby _ |
98 |
| Expr_pre _ -> List.fold_right ISet.add lhs mems |
99 |
| Expr_tuple tl -> List.fold_right2 match_mem (transpose_list [lhs]) tl mems |
100 |
| _ -> mems in |
101 |
match_mem eq.eq_lhs eq.eq_rhs mems |
102 |
|
103 |
let node_memory_variables nd = |
104 |
List.fold_left eq_memory_variables ISet.empty nd.node_eqs |
105 |
|
106 |
(* computes the equivalence relation relating variables |
107 |
in the same equation lhs, under the form of a table |
108 |
of class representatives *) |
109 |
let node_eq_equiv nd = |
110 |
let eq_equiv = Hashtbl.create 23 in |
111 |
List.iter (fun eq -> |
112 |
let first = List.hd eq.eq_lhs in |
113 |
List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs |
114 |
) |
115 |
nd.node_eqs; |
116 |
eq_equiv |
117 |
|
118 |
(* Create a tuple of right dimension, according to [expr] type, *) |
119 |
(* filled with variable [v] *) |
120 |
let adjust_tuple v expr = |
121 |
match expr.expr_type.Types.tdesc with |
122 |
| Types.Ttuple tl -> duplicate v (List.length tl) |
123 |
| _ -> [v] |
124 |
|
125 |
(* Add dependencies from lhs to rhs in [g, g'], *) |
126 |
(* no-mem/no-mem and mem/no-mem in g *) |
127 |
(* mem/mem in g' *) |
128 |
(* excluding all/[inputs] *) |
129 |
let add_eq_dependencies mems inputs eq (g, g') = |
130 |
let rec add_dep lhs_is_mem lhs rhs g = |
131 |
let add_var x (g, g') = |
132 |
if ISet.mem x inputs then (g, g') else |
133 |
match (lhs_is_mem, ISet.mem x mems) with |
134 |
| (false, true ) -> (add_edges [x] lhs g, g' ) |
135 |
| (false, false) -> (add_edges lhs [x] g, g' ) |
136 |
| (true , false) -> (add_edges lhs [x] g, g' ) |
137 |
| (true , true ) -> (g , add_edges [x] lhs g') in |
138 |
(* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *) |
139 |
(* i.e every input is connected to every output, through a ghost var *) |
140 |
let mashup_appl_dependencies f e g = |
141 |
let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in |
142 |
List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs) |
143 |
(expr_list_of_expr e) (add_var f_var g) in |
144 |
match rhs.expr_desc with |
145 |
| Expr_const _ -> g |
146 |
| Expr_fby (e1, e2) -> add_dep true lhs e2 (add_dep false lhs e1 g) |
147 |
| Expr_pre e -> add_dep true lhs e g |
148 |
| Expr_ident x -> add_var x g |
149 |
| Expr_access (e1, _) |
150 |
| Expr_power (e1, _) -> add_dep lhs_is_mem lhs e1 g |
151 |
| Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g |
152 |
| Expr_tuple t -> List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g |
153 |
| Expr_merge (c, hl) -> add_var c (List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g) |
154 |
| Expr_ite (c, t, e) -> add_dep lhs_is_mem lhs c (add_dep lhs_is_mem lhs t (add_dep lhs_is_mem lhs e g)) |
155 |
| Expr_arrow (e1, e2) -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g) |
156 |
| Expr_when (e, c, _) -> add_dep lhs_is_mem lhs e (add_var c g) |
157 |
| Expr_appl (f, e, None) -> |
158 |
if Basic_library.is_internal_fun f |
159 |
(* tuple component-wise dependency for internal operators *) |
160 |
then |
161 |
List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g |
162 |
(* mashed up dependency for user-defined operators *) |
163 |
else |
164 |
mashup_appl_dependencies f e g |
165 |
| Expr_appl (f, e, Some (r, _)) -> |
166 |
mashup_appl_dependencies f e (add_var r g) |
167 |
| Expr_uclock (e, _) |
168 |
| Expr_dclock (e, _) |
169 |
| Expr_phclock (e, _) -> add_dep lhs_is_mem lhs e g |
170 |
in |
171 |
add_dep false eq.eq_lhs eq.eq_rhs (add_vertices eq.eq_lhs g, g') |
172 |
|
173 |
|
174 |
(* Returns the dependence graph for node [n] *) |
175 |
let dependence_graph mems n = |
176 |
eq_var_cpt := 0; |
177 |
instance_var_cpt := 0; |
178 |
let g = new_graph (), new_graph () in |
179 |
let inputs = List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty n.node_inputs in |
180 |
(* Basic dependencies *) |
181 |
let g = List.fold_right (add_eq_dependencies mems inputs) n.node_eqs g in |
182 |
g |
183 |
|
184 |
end |
185 |
|
186 |
module NodeDep = struct |
187 |
|
188 |
module ExprModule = |
189 |
struct |
190 |
type t = expr |
191 |
let compare = compare |
192 |
let hash n = Hashtbl.hash n |
193 |
let equal n1 n2 = n1 = n2 |
194 |
end |
195 |
|
196 |
module ESet = Set.Make(ExprModule) |
197 |
|
198 |
let rec get_expr_calls prednode expr = |
199 |
match expr.expr_desc with |
200 |
| Expr_const _ |
201 |
| Expr_ident _ -> ESet.empty |
202 |
| Expr_access (e, _) |
203 |
| Expr_power (e, _) -> get_expr_calls prednode e |
204 |
| Expr_array t |
205 |
| Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty |
206 |
| Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty |
207 |
| Expr_fby (e1,e2) |
208 |
| Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2) |
209 |
| Expr_ite (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e)) |
210 |
| Expr_pre e |
211 |
| Expr_when (e,_,_) |
212 |
| Expr_uclock (e,_) |
213 |
| Expr_dclock (e,_) |
214 |
| Expr_phclock (e,_) -> get_expr_calls prednode e |
215 |
| Expr_appl (id,e, _) -> |
216 |
if not (Basic_library.is_internal_fun id) && prednode id |
217 |
then ESet.add expr (get_expr_calls prednode e) |
218 |
else (get_expr_calls prednode e) |
219 |
|
220 |
let get_callee expr = |
221 |
match expr.expr_desc with |
222 |
| Expr_appl (id, args, _) -> id, expr_list_of_expr args |
223 |
| _ -> assert false |
224 |
|
225 |
let get_calls prednode eqs = |
226 |
let deps = |
227 |
List.fold_left |
228 |
(fun accu eq -> ESet.union accu (get_expr_calls prednode eq.eq_rhs)) |
229 |
ESet.empty |
230 |
eqs in |
231 |
ESet.elements deps |
232 |
|
233 |
let dependence_graph prog = |
234 |
let g = new_graph () in |
235 |
let g = List.fold_right |
236 |
(fun td accu -> (* for each node we add its dependencies *) |
237 |
match td.top_decl_desc with |
238 |
| Node nd -> |
239 |
(*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *) |
240 |
let accu = add_vertices [nd.node_id] accu in |
241 |
let deps = List.map (fun e -> fst (get_callee e)) (get_calls (fun _ -> true) nd.node_eqs) in |
242 |
(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *) |
243 |
add_edges [nd.node_id] deps accu |
244 |
| _ -> assert false (* should not happen *) |
245 |
|
246 |
) prog g in |
247 |
g |
248 |
|
249 |
let rec filter_static_inputs inputs args = |
250 |
match inputs, args with |
251 |
| [] , [] -> [] |
252 |
| v::vq, a::aq -> if v.var_dec_const then (dimension_of_expr a) :: filter_static_inputs vq aq else filter_static_inputs vq aq |
253 |
| _ -> assert false |
254 |
|
255 |
let compute_generic_calls prog = |
256 |
List.iter |
257 |
(fun td -> |
258 |
match td.top_decl_desc with |
259 |
| Node nd -> |
260 |
let prednode n = is_generic_node (Hashtbl.find node_table n) in |
261 |
nd.node_gencalls <- get_calls prednode nd.node_eqs |
262 |
| _ -> () |
263 |
|
264 |
) prog |
265 |
|
266 |
end |
267 |
|
268 |
module CycleDetection = struct |
269 |
|
270 |
(* ---- Look for cycles in a dependency graph *) |
271 |
module Cycles = Graph.Components.Make (IdentDepGraph) |
272 |
|
273 |
let mk_copy_var n id = |
274 |
mk_new_name (node_vars n) id |
275 |
|
276 |
let mk_copy_eq n var = |
277 |
let var_decl = node_var var n in |
278 |
let cp_var = mk_copy_var n var in |
279 |
let expr = |
280 |
{ expr_tag = Utils.new_tag (); |
281 |
expr_desc = Expr_ident var; |
282 |
expr_type = var_decl.var_type; |
283 |
expr_clock = var_decl.var_clock; |
284 |
expr_delay = Delay.new_var (); |
285 |
expr_annot = None; |
286 |
expr_loc = var_decl.var_loc } in |
287 |
{ var_decl with var_id = cp_var }, |
288 |
mkeq var_decl.var_loc ([cp_var], expr) |
289 |
|
290 |
let wrong_partition g partition = |
291 |
match partition with |
292 |
| [id] -> IdentDepGraph.mem_edge g id id |
293 |
| _::_::_ -> true |
294 |
| [] -> assert false |
295 |
|
296 |
(* Checks that the dependency graph [g] does not contain a cycle. Raises |
297 |
[Cycle partition] if the succession of dependencies [partition] forms a cycle *) |
298 |
let check_cycles g = |
299 |
let scc_l = Cycles.scc_list g in |
300 |
List.iter (fun partition -> |
301 |
if wrong_partition g partition then |
302 |
raise (Cycle partition) |
303 |
else () |
304 |
) scc_l |
305 |
|
306 |
(* Creates the sub-graph of [g] restricted to vertices and edges in partition *) |
307 |
let copy_partition g partition = |
308 |
let copy_g = IdentDepGraph.create () in |
309 |
IdentDepGraph.iter_edges |
310 |
(fun src tgt -> |
311 |
if List.mem src partition && List.mem tgt partition |
312 |
then IdentDepGraph.add_edge copy_g src tgt) |
313 |
g |
314 |
|
315 |
|
316 |
(* Breaks dependency cycles in a graph [g] by inserting aux variables. |
317 |
[head] is a head of a non-trivial scc of [g]. |
318 |
In Lustre, this is legal only for mem/mem cycles *) |
319 |
let break_cycle head cp_head g = |
320 |
let succs = IdentDepGraph.succ g head in |
321 |
IdentDepGraph.add_edge g head cp_head; |
322 |
List.iter |
323 |
(fun s -> |
324 |
IdentDepGraph.remove_edge g head s; |
325 |
IdentDepGraph.add_edge g s cp_head) |
326 |
succs |
327 |
|
328 |
(* Breaks cycles of the dependency graph [g] of memory variables [mems] |
329 |
belonging in node [node]. Returns: |
330 |
- a list of new auxiliary variable declarations |
331 |
- a list of new equations |
332 |
- a modified acyclic version of [g] |
333 |
*) |
334 |
let break_cycles node mems g = |
335 |
let (mem_eqs, non_mem_eqs) = List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) node.node_eqs in |
336 |
let rec break vdecls mem_eqs g = |
337 |
let scc_l = Cycles.scc_list g in |
338 |
let wrong = List.filter (wrong_partition g) scc_l in |
339 |
match wrong with |
340 |
| [] -> (vdecls, non_mem_eqs@mem_eqs, g) |
341 |
| [head]::_ -> |
342 |
begin |
343 |
IdentDepGraph.remove_edge g head head; |
344 |
break vdecls mem_eqs g |
345 |
end |
346 |
| (head::part)::_ -> |
347 |
begin |
348 |
let vdecl_cp_head, cp_eq = mk_copy_eq node head in |
349 |
let pvar v = List.mem v part in |
350 |
let fvar v = if v = head then vdecl_cp_head.var_id else v in |
351 |
let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in |
352 |
break_cycle head vdecl_cp_head.var_id g; |
353 |
break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g |
354 |
end |
355 |
| _ -> assert false |
356 |
in break [] mem_eqs g |
357 |
|
358 |
end |
359 |
|
360 |
let pp_dep_graph fmt g = |
361 |
begin |
362 |
Format.fprintf fmt "{ /* graph */@."; |
363 |
IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g; |
364 |
Format.fprintf fmt "}@." |
365 |
end |
366 |
|
367 |
let pp_error fmt trace = |
368 |
fprintf fmt "@.Causality error, cyclic data dependencies: %a@." |
369 |
(fprintf_list ~sep:"->" pp_print_string) trace |
370 |
|
371 |
(* Merges elements of graph [g2] into graph [g1] *) |
372 |
let merge_with g1 g2 = |
373 |
IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2; |
374 |
IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2 |
375 |
|
376 |
let global_dependency node = |
377 |
let mems = ExprDep.node_memory_variables node in |
378 |
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems node in |
379 |
(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; |
380 |
Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*) |
381 |
CycleDetection.check_cycles g_non_mems; |
382 |
let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in |
383 |
(*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*) |
384 |
merge_with g_non_mems g_mems'; |
385 |
{ node with node_eqs = eqs'; node_locals = vdecls'@node.node_locals }, |
386 |
g_non_mems |
387 |
|
388 |
|
389 |
(* Local Variables: *) |
390 |
(* compile-command:"make -C .." *) |
391 |
(* End: *) |