lustrec / src / causality.ml @ bd771bbe
History  View  Annotate  Download (14.4 KB)
1 
(*  

2 
* SchedMCore  A MultiCore Scheduling Framework 
3 
* Copyright (C) 20092011, 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 021111307 
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 nomem 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 (nonmem/nonmem&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 
(* Tests whether [v] is a root of graph [g], i.e. a source *) 
59 
let is_graph_root v g = 
60 
IdentDepGraph.in_degree g v = 0 
61  
62 
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *) 
63 
let graph_roots g = 
64 
IdentDepGraph.fold_vertex 
65 
(fun v roots > if is_graph_root v g then v::roots else roots) 
66 
g [] 
67  
68 
let add_edges src tgt g = 
69 
(*List.iter (fun s > List.iter (fun t > Format.eprintf "add %s > %s@." s t) tgt) src;*) 
70 
List.iter 
71 
(fun s > 
72 
List.iter 
73 
(fun t > IdentDepGraph.add_edge g s t) 
74 
tgt) 
75 
src; 
76 
g 
77  
78 
let add_vertices vtc g = 
79 
(*List.iter (fun t > Format.eprintf "add %s@." t) vtc;*) 
80 
List.iter (fun v > IdentDepGraph.add_vertex g v) vtc; 
81 
g 
82  
83 
let new_graph () = 
84 
IdentDepGraph.create () 
85  
86 
module ExprDep = struct 
87  
88 
let eq_var_cpt = ref 0 
89  
90 
let instance_var_cpt = ref 0 
91  
92 
let mk_eq_var id = 
93 
incr eq_var_cpt; sprintf "#%s_%d" id !eq_var_cpt 
94  
95 
let mk_instance_var id = 
96 
incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt 
97  
98 
let is_eq_var v = v.[0] = '#' 
99  
100 
let is_instance_var v = v.[0] = '!' 
101  
102 
let is_ghost_var v = is_instance_var v  is_eq_var v 
103  
104 
let eq_memory_variables mems eq = 
105 
let rec match_mem lhs rhs mems = 
106 
match rhs.expr_desc with 
107 
 Expr_fby _ 
108 
 Expr_pre _ > List.fold_right ISet.add lhs mems 
109 
 Expr_tuple tl > List.fold_right2 match_mem (transpose_list [lhs]) tl mems 
110 
 _ > mems in 
111 
match_mem eq.eq_lhs eq.eq_rhs mems 
112  
113 
let node_memory_variables nd = 
114 
List.fold_left eq_memory_variables ISet.empty nd.node_eqs 
115  
116 
let node_non_input_variables nd = 
117 
let outputs = List.fold_left (fun outputs v > ISet.add v.var_id outputs) ISet.empty nd.node_outputs in 
118 
List.fold_left (fun non_inputs v > ISet.add v.var_id non_inputs) outputs nd.node_locals 
119  
120 
(* computes the equivalence relation relating variables 
121 
in the same equation lhs, under the form of a table 
122 
of class representatives *) 
123 
let node_eq_equiv nd = 
124 
let eq_equiv = Hashtbl.create 23 in 
125 
List.iter (fun eq > 
126 
let first = List.hd eq.eq_lhs in 
127 
List.iter (fun v > Hashtbl.add eq_equiv v first) eq.eq_lhs 
128 
) 
129 
nd.node_eqs; 
130 
eq_equiv 
131  
132 
(* Create a tuple of right dimension, according to [expr] type, *) 
133 
(* filled with variable [v] *) 
134 
let adjust_tuple v expr = 
135 
match expr.expr_type.Types.tdesc with 
136 
 Types.Ttuple tl > duplicate v (List.length tl) 
137 
 _ > [v] 
138  
139  
140 
(* Add dependencies from lhs to rhs in [g, g'], *) 
141 
(* nomem/nomem and mem/nomem in g *) 
142 
(* mem/mem in g' *) 
143 
(* excluding all/[inputs] *) 
144 
let add_eq_dependencies mems non_inputs eq (g, g') = 
145 
let add_var lhs_is_mem lhs x (g, g') = 
146 
if is_instance_var x  ISet.mem x non_inputs then 
147 
match (lhs_is_mem, ISet.mem x mems) with 
148 
 (false, true ) > (add_edges [x] lhs g, g' ) 
149 
 (false, false) > (add_edges lhs [x] g, g' ) 
150 
 (true , false) > (add_edges lhs [x] g, g' ) 
151 
 (true , true ) > (g , add_edges [x] lhs g') 
152 
else (g, g') in 
153 
(* Add dependencies from [lhs] to rhs clock [ck]. *) 
154 
let rec add_clock lhs_is_mem lhs ck g = 
155 
(*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*) 
156 
match (Clocks.repr ck).Clocks.cdesc with 
157 
 Clocks.Con (ck', cr, _) > add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g) 
158 
 Clocks.Ccarrying (_, ck') > add_clock lhs_is_mem lhs ck' g 
159 
 _ > g in 
160 
let rec add_dep lhs_is_mem lhs rhs g = 
161 
(* Add mashup dependencies for a userdefined node instance [lhs] = [f]([e]) *) 
162 
(* i.e every input is connected to every output, through a ghost var *) 
163 
let mashup_appl_dependencies f e g = 
164 
let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in 
165 
List.fold_right (fun rhs > add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs) 
166 
(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) in 
167 
match rhs.expr_desc with 
168 
 Expr_const _ > g 
169 
 Expr_fby (e1, e2) > add_dep true lhs e2 (add_dep false lhs e1 g) 
170 
 Expr_pre e > add_dep true lhs e g 
171 
 Expr_ident x > add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g) 
172 
 Expr_access (e1, _) 
173 
 Expr_power (e1, _) > add_dep lhs_is_mem lhs e1 g 
174 
 Expr_array a > List.fold_right (add_dep lhs_is_mem lhs) a g 
175 
 Expr_tuple t > List.fold_right2 (fun l r > add_dep lhs_is_mem [l] r) lhs t g 
176 
 Expr_merge (c, hl) > add_var lhs_is_mem lhs c (List.fold_right (fun (_, h) > add_dep lhs_is_mem lhs h) hl g) 
177 
 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)) 
178 
 Expr_arrow (e1, e2) > add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g) 
179 
 Expr_when (e, c, _) > add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g) 
180 
 Expr_appl (f, e, None) > 
181 
if Basic_library.is_internal_fun f 
182 
(* tuple componentwise dependency for internal operators *) 
183 
then 
184 
List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g 
185 
(* mashed up dependency for userdefined operators *) 
186 
else 
187 
mashup_appl_dependencies f e g 
188 
 Expr_appl (f, e, Some (r, _)) > 
189 
mashup_appl_dependencies f e (add_var lhs_is_mem lhs r g) 
190 
 Expr_uclock (e, _) 
191 
 Expr_dclock (e, _) 
192 
 Expr_phclock (e, _) > add_dep lhs_is_mem lhs e g 
193 
in 
194 
add_dep false eq.eq_lhs eq.eq_rhs (add_vertices eq.eq_lhs g, g') 
195 

196  
197 
(* Returns the dependence graph for node [n] *) 
198 
let dependence_graph mems non_inputs n = 
199 
eq_var_cpt := 0; 
200 
instance_var_cpt := 0; 
201 
let g = new_graph (), new_graph () in 
202 
(* Basic dependencies *) 
203 
let g = List.fold_right (add_eq_dependencies mems non_inputs) n.node_eqs g in 
204 
g 
205  
206 
end 
207  
208 
module NodeDep = struct 
209  
210 
module ExprModule = 
211 
struct 
212 
type t = expr 
213 
let compare = compare 
214 
let hash n = Hashtbl.hash n 
215 
let equal n1 n2 = n1 = n2 
216 
end 
217  
218 
module ESet = Set.Make(ExprModule) 
219  
220 
let rec get_expr_calls prednode expr = 
221 
match expr.expr_desc with 
222 
 Expr_const _ 
223 
 Expr_ident _ > ESet.empty 
224 
 Expr_access (e, _) 
225 
 Expr_power (e, _) > get_expr_calls prednode e 
226 
 Expr_array t 
227 
 Expr_tuple t > List.fold_right (fun x set > ESet.union (get_expr_calls prednode x) set) t ESet.empty 
228 
 Expr_merge (_,hl) > List.fold_right (fun (_,h) set > ESet.union (get_expr_calls prednode h) set) hl ESet.empty 
229 
 Expr_fby (e1,e2) 
230 
 Expr_arrow (e1,e2) > ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2) 
231 
 Expr_ite (c, t, e) > ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e)) 
232 
 Expr_pre e 
233 
 Expr_when (e,_,_) 
234 
 Expr_uclock (e,_) 
235 
 Expr_dclock (e,_) 
236 
 Expr_phclock (e,_) > get_expr_calls prednode e 
237 
 Expr_appl (id,e, _) > 
238 
if not (Basic_library.is_internal_fun id) && prednode id 
239 
then ESet.add expr (get_expr_calls prednode e) 
240 
else (get_expr_calls prednode e) 
241  
242 
let get_callee expr = 
243 
match expr.expr_desc with 
244 
 Expr_appl (id, args, _) > Some (id, expr_list_of_expr args) 
245 
 _ > None 
246  
247 
let get_calls prednode eqs = 
248 
let deps = 
249 
List.fold_left 
250 
(fun accu eq > ESet.union accu (get_expr_calls prednode eq.eq_rhs)) 
251 
ESet.empty 
252 
eqs in 
253 
ESet.elements deps 
254  
255 
let dependence_graph prog = 
256 
let g = new_graph () in 
257 
let g = List.fold_right 
258 
(fun td accu > (* for each node we add its dependencies *) 
259 
match td.top_decl_desc with 
260 
 Node nd > 
261 
(*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *) 
262 
let accu = add_vertices [nd.node_id] accu in 
263 
let deps = List.map (fun e > fst (desome (get_callee e))) (get_calls (fun _ > true) nd.node_eqs) in 
264 
(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *) 
265 
add_edges [nd.node_id] deps accu 
266 
 _ > assert false (* should not happen *) 
267 

268 
) prog g in 
269 
g 
270  
271 
let rec filter_static_inputs inputs args = 
272 
match inputs, args with 
273 
 [] , [] > [] 
274 
 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 
275 
 _ > assert false 
276  
277 
let compute_generic_calls prog = 
278 
List.iter 
279 
(fun td > 
280 
match td.top_decl_desc with 
281 
 Node nd > 
282 
let prednode n = is_generic_node (Hashtbl.find node_table n) in 
283 
nd.node_gencalls < get_calls prednode nd.node_eqs 
284 
 _ > () 
285 

286 
) prog 
287  
288 
end 
289  
290 
module CycleDetection = struct 
291  
292 
(*  Look for cycles in a dependency graph *) 
293 
module Cycles = Graph.Components.Make (IdentDepGraph) 
294  
295 
let mk_copy_var n id = 
296 
mk_new_name (node_vars n) id 
297  
298 
let mk_copy_eq n var = 
299 
let var_decl = node_var var n in 
300 
let cp_var = mk_copy_var n var in 
301 
let expr = 
302 
{ expr_tag = Utils.new_tag (); 
303 
expr_desc = Expr_ident var; 
304 
expr_type = var_decl.var_type; 
305 
expr_clock = var_decl.var_clock; 
306 
expr_delay = Delay.new_var (); 
307 
expr_annot = None; 
308 
expr_loc = var_decl.var_loc } in 
309 
{ var_decl with var_id = cp_var }, 
310 
mkeq var_decl.var_loc ([cp_var], expr) 
311  
312 
let wrong_partition g partition = 
313 
match partition with 
314 
 [id] > IdentDepGraph.mem_edge g id id 
315 
 _::_::_ > true 
316 
 [] > assert false 
317  
318 
(* Checks that the dependency graph [g] does not contain a cycle. Raises 
319 
[Cycle partition] if the succession of dependencies [partition] forms a cycle *) 
320 
let check_cycles g = 
321 
let scc_l = Cycles.scc_list g in 
322 
List.iter (fun partition > 
323 
if wrong_partition g partition then 
324 
raise (Cycle partition) 
325 
else () 
326 
) scc_l 
327  
328 
(* Creates the subgraph of [g] restricted to vertices and edges in partition *) 
329 
let copy_partition g partition = 
330 
let copy_g = IdentDepGraph.create () in 
331 
IdentDepGraph.iter_edges 
332 
(fun src tgt > 
333 
if List.mem src partition && List.mem tgt partition 
334 
then IdentDepGraph.add_edge copy_g src tgt) 
335 
g 
336  
337 

338 
(* Breaks dependency cycles in a graph [g] by inserting aux variables. 
339 
[head] is a head of a nontrivial scc of [g]. 
340 
In Lustre, this is legal only for mem/mem cycles *) 
341 
let break_cycle head cp_head g = 
342 
let succs = IdentDepGraph.succ g head in 
343 
IdentDepGraph.add_edge g head cp_head; 
344 
List.iter 
345 
(fun s > 
346 
IdentDepGraph.remove_edge g head s; 
347 
IdentDepGraph.add_edge g s cp_head) 
348 
succs 
349  
350 
(* Breaks cycles of the dependency graph [g] of memory variables [mems] 
351 
belonging in node [node]. Returns: 
352 
 a list of new auxiliary variable declarations 
353 
 a list of new equations 
354 
 a modified acyclic version of [g] 
355 
*) 
356 
let break_cycles node mems g = 
357 
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 
358 
let rec break vdecls mem_eqs g = 
359 
let scc_l = Cycles.scc_list g in 
360 
let wrong = List.filter (wrong_partition g) scc_l in 
361 
match wrong with 
362 
 [] > (vdecls, non_mem_eqs@mem_eqs, g) 
363 
 [head]::_ > 
364 
begin 
365 
IdentDepGraph.remove_edge g head head; 
366 
break vdecls mem_eqs g 
367 
end 
368 
 (head::part)::_ > 
369 
begin 
370 
let vdecl_cp_head, cp_eq = mk_copy_eq node head in 
371 
let pvar v = List.mem v part in 
372 
let fvar v = if v = head then vdecl_cp_head.var_id else v in 
373 
let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in 
374 
break_cycle head vdecl_cp_head.var_id g; 
375 
break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g 
376 
end 
377 
 _ > assert false 
378 
in break [] mem_eqs g 
379  
380 
end 
381  
382 
let pp_dep_graph fmt g = 
383 
begin 
384 
Format.fprintf fmt "{ /* graph */@."; 
385 
IdentDepGraph.iter_edges (fun s t > Format.fprintf fmt "%s > %s@." s t) g; 
386 
Format.fprintf fmt "}@." 
387 
end 
388  
389 
let pp_error fmt trace = 
390 
fprintf fmt "@.Causality error, cyclic data dependencies: %a@." 
391 
(fprintf_list ~sep:">" pp_print_string) trace 
392  
393 
(* Merges elements of graph [g2] into graph [g1] *) 
394 
let merge_with g1 g2 = 
395 
IdentDepGraph.iter_vertex (fun v > IdentDepGraph.add_vertex g1 v) g2; 
396 
IdentDepGraph.iter_edges (fun s t > IdentDepGraph.add_edge g1 s t) g2 
397  
398 
let global_dependency node = 
399 
let mems = ExprDep.node_memory_variables node in 
400 
let non_inputs = ExprDep.node_non_input_variables node in 
401 
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems non_inputs node in 
402 
(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; 
403 
Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*) 
404 
CycleDetection.check_cycles g_non_mems; 
405 
let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in 
406 
(*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*) 
407 
merge_with g_non_mems g_mems'; 
408 
{ node with node_eqs = eqs'; node_locals = vdecls'@node.node_locals }, 
409 
g_non_mems 
410  
411  
412 
(* Local Variables: *) 
413 
(* compilecommand:"make C .." *) 
414 
(* End: *) 