lustrec / src / causality.ml @ 0cbf0839
History  View  Annotate  Download (13.3 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 
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 
(* nomem/nomem and mem/nomem 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 userdefined 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 componentwise 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 userdefined 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 subgraph 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 nontrivial 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 
(* compilecommand:"make C .." *) 
391 
(* End: *) 