lustrec / src / causality.ml @ 01c7d5e1
History  View  Annotate  Download (17.9 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 
(* Dependency of mem variables on mem variables is cut off 
37 
by duplication of some mem vars into local node vars. 
38 
Thus, cylic dependency errors may only arise between nomem vars. 
39 
nonmem variables are: 
40 
 inputs: not needed for causality/scheduling, needed only for detecting useless vars 
41 
 read mems (fake vars): same remark as above. 
42 
 outputs: decoupled from mems, if necessary 
43 
 locals 
44 
 instance vars (fake vars): simplify causality analysis 
45  
46 
global constants are not part of the dependency graph. 
47  
48 
no_mem' = combinational(no_mem, mem); 
49 
=> (mem > no_mem' > no_mem) 
50  
51 
mem' = pre(no_mem, mem); 
52 
=> (mem' > no_mem), (mem > mem') 
53  
54 
Global roadmap: 
55 
 compute two dep graphs g (nonmem/nonmem&mem) and g' (mem/mem) 
56 
 check cycles in g (a cycle means a dependency error) 
57 
 break cycles in g' (it's legal !): 
58 
 check cycles in g' 
59 
 if any, introduce aux var to break cycle, then start afresh 
60 
 insert g' into g 
61 
 return g 
62 
*) 
63  
64 
(* Tests whether [v] is a root of graph [g], i.e. a source *) 
65 
let is_graph_root v g = 
66 
IdentDepGraph.in_degree g v = 0 
67  
68 
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *) 
69 
let graph_roots g = 
70 
IdentDepGraph.fold_vertex 
71 
(fun v roots > if is_graph_root v g then v::roots else roots) 
72 
g [] 
73  
74 
let add_edges src tgt g = 
75 
(*List.iter (fun s > List.iter (fun t > Format.eprintf "add %s > %s@." s t) tgt) src;*) 
76 
List.iter 
77 
(fun s > 
78 
List.iter 
79 
(fun t > IdentDepGraph.add_edge g s t) 
80 
tgt) 
81 
src; 
82 
g 
83  
84 
let add_vertices vtc g = 
85 
(*List.iter (fun t > Format.eprintf "add %s@." t) vtc;*) 
86 
List.iter (fun v > IdentDepGraph.add_vertex g v) vtc; 
87 
g 
88  
89 
let new_graph () = 
90 
IdentDepGraph.create () 
91  
92 
module ExprDep = struct 
93  
94 
let instance_var_cpt = ref 0 
95  
96 
(* read vars represent input/mem readonly vars, 
97 
they are not part of the program/schedule, 
98 
as they are not assigned, 
99 
but used to compute useless inputs/mems. 
100 
a mem read var represents a mem at the beginning of a cycle *) 
101 
let mk_read_var id = 
102 
sprintf "#%s" id 
103  
104 
(* instance vars represent node instance calls, 
105 
they are not part of the program/schedule, 
106 
but used to simplify causality analysis 
107 
*) 
108 
let mk_instance_var id = 
109 
incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt 
110  
111 
let is_read_var v = v.[0] = '#' 
112  
113 
let is_instance_var v = v.[0] = '!' 
114  
115 
let is_ghost_var v = is_instance_var v  is_read_var v 
116  
117 
let undo_read_var id = 
118 
assert (is_read_var id); 
119 
String.sub id 1 (String.length id  1) 
120  
121 
let eq_memory_variables mems eq = 
122 
let rec match_mem lhs rhs mems = 
123 
match rhs.expr_desc with 
124 
 Expr_fby _ 
125 
 Expr_pre _ > List.fold_right ISet.add lhs mems 
126 
 Expr_tuple tl > 
127 
let lhs' = (transpose_list [lhs]) in 
128 
List.fold_right2 match_mem lhs' tl mems 
129 
 _ > mems in 
130 
match_mem eq.eq_lhs eq.eq_rhs mems 
131  
132 
let node_memory_variables nd = 
133 
List.fold_left eq_memory_variables ISet.empty nd.node_eqs 
134  
135 
let node_input_variables nd = 
136 
List.fold_left (fun inputs v > ISet.add v.var_id inputs) ISet.empty nd.node_inputs 
137  
138 
let node_local_variables nd = 
139 
List.fold_left (fun locals v > ISet.add v.var_id locals) ISet.empty nd.node_locals 
140  
141 
let node_output_variables nd = 
142 
List.fold_left (fun outputs v > ISet.add v.var_id outputs) ISet.empty nd.node_outputs 
143  
144 
let node_variables nd = 
145 
let inputs = node_input_variables nd in 
146 
let inoutputs = List.fold_left (fun inoutputs v > ISet.add v.var_id inoutputs) inputs nd.node_outputs in 
147 
List.fold_left (fun vars v > ISet.add v.var_id vars) inoutputs nd.node_locals 
148  
149 
(* computes the equivalence relation relating variables 
150 
in the same equation lhs, under the form of a table 
151 
of class representatives *) 
152 
let node_eq_equiv nd = 
153 
let eq_equiv = Hashtbl.create 23 in 
154 
List.iter (fun eq > 
155 
let first = List.hd eq.eq_lhs in 
156 
List.iter (fun v > Hashtbl.add eq_equiv v first) eq.eq_lhs 
157 
) 
158 
nd.node_eqs; 
159 
eq_equiv 
160  
161 
(* Create a tuple of right dimension, according to [expr] type, *) 
162 
(* filled with variable [v] *) 
163 
let adjust_tuple v expr = 
164 
match expr.expr_type.Types.tdesc with 
165 
 Types.Ttuple tl > duplicate v (List.length tl) 
166 
 _ > [v] 
167  
168  
169 
(* Add dependencies from lhs to rhs in [g, g'], *) 
170 
(* nomem/nomem and mem/nomem in g *) 
171 
(* mem/mem in g' *) 
172 
(* match (lhs_is_mem, ISet.mem x mems) with 
173 
 (false, true ) > (add_edges [x] lhs g, 
174 
g') 
175 
 (false, false) > (add_edges lhs [x] g, 
176 
g') 
177 
 (true , false) > (add_edges lhs [x] g, 
178 
g') 
179 
 (true , true ) > (g, 
180 
add_edges [x] lhs g') 
181 
*) 
182 
let add_eq_dependencies mems inputs node_vars eq (g, g') = 
183 
let add_var lhs_is_mem lhs x (g, g') = 
184 
if is_instance_var x  ISet.mem x node_vars then 
185 
if ISet.mem x mems 
186 
then 
187 
let g = add_edges lhs [mk_read_var x] g in 
188 
if lhs_is_mem 
189 
then 
190 
(g, add_edges [x] lhs g') 
191 
else 
192 
(add_edges [x] lhs g, g') 
193 
else 
194 
let x = if ISet.mem x inputs then mk_read_var x else x in 
195 
(add_edges lhs [x] g, g') 
196 
else (g, g') in 
197 
(* Add dependencies from [lhs] to rhs clock [ck]. *) 
198 
let rec add_clock lhs_is_mem lhs ck g = 
199 
(*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*) 
200 
match (Clocks.repr ck).Clocks.cdesc with 
201 
 Clocks.Con (ck', cr, _) > add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g) 
202 
 Clocks.Ccarrying (_, ck') > add_clock lhs_is_mem lhs ck' g 
203 
 _ > g 
204 
in 
205 
let rec add_dep lhs_is_mem lhs rhs g = 
206 
(* Add mashup dependencies for a userdefined node instance [lhs] = [f]([e]) *) 
207 
(* i.e every input is connected to every output, through a ghost var *) 
208 
let mashup_appl_dependencies f e g = 
209 
let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in 
210 
List.fold_right (fun rhs > add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs) 
211 
(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) 
212 
in 
213 
match rhs.expr_desc with 
214 
 Expr_const _ > g 
215 
 Expr_fby (e1, e2) > add_dep true lhs e2 (add_dep false lhs e1 g) 
216 
 Expr_pre e > add_dep true lhs e g 
217 
 Expr_ident x > add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g) 
218 
 Expr_access (e1, _) 
219 
 Expr_power (e1, _) > add_dep lhs_is_mem lhs e1 g 
220 
 Expr_array a > List.fold_right (add_dep lhs_is_mem lhs) a g 
221 
 Expr_tuple t > 
222 
(* 
223 
if List.length t <> List.length lhs then ( 
224 
match lhs with 
225 
 [l] > List.fold_right (fun r > add_dep lhs_is_mem [l] r) t g 
226 
 _ > 
227 
Format.eprintf "Incompatible tuple assign: %a (%i) vs %a (%i)@.@?" 
228 
(Utils.fprintf_list ~sep:"," (Format.pp_print_string)) lhs 
229 
(List.length lhs) 
230 
Printers.pp_expr rhs 
231 
(List.length t) 
232 
; 
233 
assert false 
234 
) 
235 
else 
236 
*) 
237 
List.fold_right2 (fun l r > add_dep lhs_is_mem [l] r) lhs t g 
238 
 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) 
239 
 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)) 
240 
 Expr_arrow (e1, e2) > add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g) 
241 
 Expr_when (e, c, _) > add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g) 
242 
 Expr_appl (f, e, None) > 
243 
if Basic_library.is_internal_fun f 
244 
(* tuple componentwise dependency for internal operators *) 
245 
then 
246 
List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g 
247 
(* mashed up dependency for userdefined operators *) 
248 
else 
249 
mashup_appl_dependencies f e g 
250 
 Expr_appl (f, e, Some (r, _)) > 
251 
mashup_appl_dependencies f e (add_var lhs_is_mem lhs r g) 
252 
in 
253 
let g = 
254 
List.fold_left 
255 
(fun g lhs > if ISet.mem lhs mems then add_vertices [lhs; mk_read_var lhs] g else add_vertices [lhs] g) g eq.eq_lhs in 
256 
add_dep false eq.eq_lhs eq.eq_rhs (g, g') 
257 

258  
259 
(* Returns the dependence graph for node [n] *) 
260 
let dependence_graph mems inputs node_vars n = 
261 
instance_var_cpt := 0; 
262 
let g = new_graph (), new_graph () in 
263 
(* Basic dependencies *) 
264 
let g = List.fold_right (add_eq_dependencies mems inputs node_vars) n.node_eqs g in 
265 
g 
266  
267 
end 
268  
269 
module NodeDep = struct 
270  
271 
module ExprModule = 
272 
struct 
273 
type t = expr 
274 
let compare = compare 
275 
let hash n = Hashtbl.hash n 
276 
let equal n1 n2 = n1 = n2 
277 
end 
278  
279 
module ESet = Set.Make(ExprModule) 
280  
281 
let rec get_expr_calls prednode expr = 
282 
match expr.expr_desc with 
283 
 Expr_const _ 
284 
 Expr_ident _ > ESet.empty 
285 
 Expr_access (e, _) 
286 
 Expr_power (e, _) > get_expr_calls prednode e 
287 
 Expr_array t 
288 
 Expr_tuple t > List.fold_right (fun x set > ESet.union (get_expr_calls prednode x) set) t ESet.empty 
289 
 Expr_merge (_,hl) > List.fold_right (fun (_,h) set > ESet.union (get_expr_calls prednode h) set) hl ESet.empty 
290 
 Expr_fby (e1,e2) 
291 
 Expr_arrow (e1,e2) > ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2) 
292 
 Expr_ite (c, t, e) > ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e)) 
293 
 Expr_pre e 
294 
 Expr_when (e,_,_) > get_expr_calls prednode e 
295 
 Expr_appl (id,e, _) > 
296 
if not (Basic_library.is_internal_fun id) && prednode id 
297 
then ESet.add expr (get_expr_calls prednode e) 
298 
else (get_expr_calls prednode e) 
299  
300 
let get_callee expr = 
301 
match expr.expr_desc with 
302 
 Expr_appl (id, args, _) > Some (id, expr_list_of_expr args) 
303 
 _ > None 
304  
305 
let get_calls prednode eqs = 
306 
let deps = 
307 
List.fold_left 
308 
(fun accu eq > ESet.union accu (get_expr_calls prednode eq.eq_rhs)) 
309 
ESet.empty 
310 
eqs in 
311 
ESet.elements deps 
312  
313 
let dependence_graph prog = 
314 
let g = new_graph () in 
315 
let g = List.fold_right 
316 
(fun td accu > (* for each node we add its dependencies *) 
317 
match td.top_decl_desc with 
318 
 Node nd > 
319 
(*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *) 
320 
let accu = add_vertices [nd.node_id] accu in 
321 
let deps = List.map (fun e > fst (desome (get_callee e))) (get_calls (fun _ > true) nd.node_eqs) in 
322 
(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *) 
323 
add_edges [nd.node_id] deps accu 
324 
 _ > assert false (* should not happen *) 
325 

326 
) prog g in 
327 
g 
328  
329 
let rec filter_static_inputs inputs args = 
330 
match inputs, args with 
331 
 [] , [] > [] 
332 
 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 
333 
 _ > assert false 
334  
335 
let compute_generic_calls prog = 
336 
List.iter 
337 
(fun td > 
338 
match td.top_decl_desc with 
339 
 Node nd > 
340 
let prednode n = is_generic_node (Hashtbl.find node_table n) in 
341 
nd.node_gencalls < get_calls prednode nd.node_eqs 
342 
 _ > () 
343 

344 
) prog 
345  
346 
end 
347  
348 
module CycleDetection = struct 
349  
350 
(*  Look for cycles in a dependency graph *) 
351 
module Cycles = Graph.Components.Make (IdentDepGraph) 
352  
353 
let mk_copy_var n id = 
354 
mk_new_name (get_node_vars n) id 
355  
356 
let mk_copy_eq n var = 
357 
let var_decl = get_node_var var n in 
358 
let cp_var = mk_copy_var n var in 
359 
let expr = 
360 
{ expr_tag = Utils.new_tag (); 
361 
expr_desc = Expr_ident var; 
362 
expr_type = var_decl.var_type; 
363 
expr_clock = var_decl.var_clock; 
364 
expr_delay = Delay.new_var (); 
365 
expr_annot = None; 
366 
expr_loc = var_decl.var_loc } in 
367 
{ var_decl with var_id = cp_var }, 
368 
mkeq var_decl.var_loc ([cp_var], expr) 
369  
370 
let wrong_partition g partition = 
371 
match partition with 
372 
 [id] > IdentDepGraph.mem_edge g id id 
373 
 _::_::_ > true 
374 
 [] > assert false 
375  
376 
(* Checks that the dependency graph [g] does not contain a cycle. Raises 
377 
[Cycle partition] if the succession of dependencies [partition] forms a cycle *) 
378 
let check_cycles g = 
379 
let scc_l = Cycles.scc_list g in 
380 
List.iter (fun partition > 
381 
if wrong_partition g partition then 
382 
raise (Cycle partition) 
383 
else () 
384 
) scc_l 
385  
386 
(* Creates the subgraph of [g] restricted to vertices and edges in partition *) 
387 
let copy_partition g partition = 
388 
let copy_g = IdentDepGraph.create () in 
389 
IdentDepGraph.iter_edges 
390 
(fun src tgt > 
391 
if List.mem src partition && List.mem tgt partition 
392 
then IdentDepGraph.add_edge copy_g src tgt) 
393 
g 
394  
395 

396 
(* Breaks dependency cycles in a graph [g] by inserting aux variables. 
397 
[head] is a head of a nontrivial scc of [g]. 
398 
In Lustre, this is legal only for mem/mem cycles *) 
399 
let break_cycle head cp_head g = 
400 
let succs = IdentDepGraph.succ g head in 
401 
IdentDepGraph.add_edge g head cp_head; 
402 
IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head); 
403 
List.iter 
404 
(fun s > 
405 
IdentDepGraph.remove_edge g head s; 
406 
IdentDepGraph.add_edge g s cp_head) 
407 
succs 
408  
409 
(* Breaks cycles of the dependency graph [g] of memory variables [mems] 
410 
belonging in node [node]. Returns: 
411 
 a list of new auxiliary variable declarations 
412 
 a list of new equations 
413 
 a modified acyclic version of [g] 
414 
*) 
415 
let break_cycles node mems g = 
416 
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 
417 
let rec break vdecls mem_eqs g = 
418 
let scc_l = Cycles.scc_list g in 
419 
let wrong = List.filter (wrong_partition g) scc_l in 
420 
match wrong with 
421 
 [] > (vdecls, non_mem_eqs@mem_eqs, g) 
422 
 [head]::_ > 
423 
begin 
424 
IdentDepGraph.remove_edge g head head; 
425 
break vdecls mem_eqs g 
426 
end 
427 
 (head::part)::_ > 
428 
begin 
429 
let vdecl_cp_head, cp_eq = mk_copy_eq node head in 
430 
let pvar v = List.mem v part in 
431 
let fvar v = if v = head then vdecl_cp_head.var_id else v in 
432 
let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in 
433 
break_cycle head vdecl_cp_head.var_id g; 
434 
break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g 
435 
end 
436 
 _ > assert false 
437 
in break [] mem_eqs g 
438  
439 
end 
440  
441 
(* Module used to compute static disjunction of variables based upon their clocks. *) 
442 
module Disjunction = 
443 
struct 
444 
module ClockedIdentModule = 
445 
struct 
446 
type t = var_decl 
447 
let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock 
448 
let compare v1 v2 = compare (root_branch v2) (root_branch v1) 
449 
end 
450  
451 
module CISet = Set.Make(ClockedIdentModule) 
452  
453 
(* map: var > list of disjoint vars, sorted in increasing branch length order, 
454 
maybe removing shorter branches *) 
455 
type clock_map = (ident, var_decl list) Hashtbl.t 
456  
457 
let clock_disjoint_map vdecls = 
458 
let map = Hashtbl.create 23 in 
459 
begin 
460 
List.iter 
461 
(fun v1 > let disj_v1 = 
462 
List.fold_left 
463 
(fun res v2 > if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res) 
464 
CISet.empty 
465 
vdecls in 
466 
(* disjoint vdecls are stored in increasing branch length order *) 
467 
Hashtbl.add map v1.var_id disj_v1) 
468 
vdecls; 
469 
map 
470 
end 
471  
472 
(* replace variable [v] by [v'] in disjunction [map]. Then: 
473 
 the mapping v > ... disappears 
474 
 the mapping v' becomes v' > (map v) inter (map v') 
475 
 other mappings become x > (map x) \ (if v in x then v else v') 
476 
*) 
477 
let replace_in_disjoint_map map v v' = 
478 
begin 
479 
Hashtbl.remove map v.var_id; 
480 
Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id)); 
481 
Hashtbl.iter (fun x map_x > Hashtbl.replace map x (CISet.remove (if CISet.mem v map_x then v else v') map_x)) map; 
482 
end 
483  
484 
let pp_disjoint_map fmt map = 
485 
begin 
486 
Format.fprintf fmt "{ /* disjoint map */@."; 
487 
Hashtbl.iter (fun k v > Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map; 
488 
Format.fprintf fmt "}@." 
489 
end 
490 
end 
491  
492 
let pp_dep_graph fmt g = 
493 
begin 
494 
Format.fprintf fmt "{ /* graph */@."; 
495 
IdentDepGraph.iter_edges (fun s t > Format.fprintf fmt "%s > %s@." s t) g; 
496 
Format.fprintf fmt "}@." 
497 
end 
498  
499 
let pp_error fmt trace = 
500 
fprintf fmt "@.Causality error, cyclic data dependencies: %a@." 
501 
(fprintf_list ~sep:">" pp_print_string) trace 
502  
503 
(* Merges elements of graph [g2] into graph [g1] *) 
504 
let merge_with g1 g2 = 
505 
IdentDepGraph.iter_vertex (fun v > IdentDepGraph.add_vertex g1 v) g2; 
506 
IdentDepGraph.iter_edges (fun s t > IdentDepGraph.add_edge g1 s t) g2 
507  
508 
let global_dependency node = 
509 
let mems = ExprDep.node_memory_variables node in 
510 
let inputs = ExprDep.node_input_variables node in 
511 
let node_vars = ExprDep.node_variables node in 
512 
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in 
513 
(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; 
514 
Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*) 
515 
CycleDetection.check_cycles g_non_mems; 
516 
let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in 
517 
(*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*) 
518 
merge_with g_non_mems g_mems'; 
519 
{ node with node_eqs = eqs'; node_locals = vdecls'@node.node_locals }, 
520 
g_non_mems 
521  
522  
523 
(* Local Variables: *) 
524 
(* compilecommand:"make C .." *) 
525 
(* End: *) 