Revision 9aaee7f9
Added by Xavier Thirioux almost 9 years ago
src/causality.ml  

33  33  
34  34 
module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule) 
35  35  
36 
(*module IdentDepGraphUtil = Oper.P(IdentDepGraph)*) 

37  
38  36 
(* Dependency of mem variables on mem variables is cut off 
39  37 
by duplication of some mem vars into local node vars. 
40  38 
Thus, cylic dependency errors may only arise between nomem vars. 
41 


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  
42  48 
no_mem' = combinational(no_mem, mem); 
43  49 
=> (mem > no_mem' > no_mem) 
44  50  
...  ...  
85  91  
86  92 
module ExprDep = struct 
87  93  
88 
let eq_var_cpt = ref 0 

89  
90  94 
let instance_var_cpt = ref 0 
91  95  
92 
let mk_eq_var id = 

93 
incr eq_var_cpt; sprintf "#%s_%d" id !eq_var_cpt 

94  
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 
*) 

95  108 
let mk_instance_var id = 
96  109 
incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt 
97  110  
98 
let is_eq_var v = v.[0] = '#'


111 
let is_read_var v = v.[0] = '#'


99  112  
100  113 
let is_instance_var v = v.[0] = '!' 
101  114  
102 
let is_ghost_var v = is_instance_var v  is_eq_var v 

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) 

103  120  
104  121 
let eq_memory_variables mems eq = 
105  122 
let rec match_mem lhs rhs mems = 
...  ...  
108  125 
 Expr_pre _ > List.fold_right ISet.add lhs mems 
109  126 
 Expr_tuple tl > 
110  127 
let lhs' = (transpose_list [lhs]) in 
111 
if List.length tl <> List.length lhs' then 

112 
assert false; 

113  128 
List.fold_right2 match_mem lhs' tl mems 
114  129 
 _ > mems in 
115  130 
match_mem eq.eq_lhs eq.eq_rhs mems 
...  ...  
117  132 
let node_memory_variables nd = 
118  133 
List.fold_left eq_memory_variables ISet.empty nd.node_eqs 
119  134  
120 
let node_non_input_variables nd = 

121 
let outputs = List.fold_left (fun outputs v > ISet.add v.var_id outputs) ISet.empty nd.node_outputs in 

122 
List.fold_left (fun non_inputs v > ISet.add v.var_id non_inputs) outputs nd.node_locals 

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_output_variables nd = 

139 
List.fold_left (fun outputs v > ISet.add v.var_id outputs) ISet.empty nd.node_outputs 

140  
141 
let node_variables nd = 

142 
let inputs = node_input_variables nd in 

143 
let inoutputs = List.fold_left (fun inoutputs v > ISet.add v.var_id inoutputs) inputs nd.node_outputs in 

144 
List.fold_left (fun vars v > ISet.add v.var_id vars) inoutputs nd.node_locals 

123  145  
124  146 
(* computes the equivalence relation relating variables 
125  147 
in the same equation lhs, under the form of a table 
...  ...  
144  166 
(* Add dependencies from lhs to rhs in [g, g'], *) 
145  167 
(* nomem/nomem and mem/nomem in g *) 
146  168 
(* mem/mem in g' *) 
147 
(* excluding all/[inputs] *) 

148 
let add_eq_dependencies mems non_inputs eq (g, g') = 

169 
(* match (lhs_is_mem, ISet.mem x mems) with 

170 
 (false, true ) > (add_edges [x] lhs g, 

171 
g') 

172 
 (false, false) > (add_edges lhs [x] g, 

173 
g') 

174 
 (true , false) > (add_edges lhs [x] g, 

175 
g') 

176 
 (true , true ) > (g, 

177 
add_edges [x] lhs g') 

178 
*) 

179 
let add_eq_dependencies mems inputs node_vars eq (g, g') = 

149  180 
let add_var lhs_is_mem lhs x (g, g') = 
150 
if is_instance_var x  ISet.mem x non_inputs then 

151 
match (lhs_is_mem, ISet.mem x mems) with 

152 
 (false, true ) > (add_edges [x] lhs g, g' ) 

153 
 (false, false) > (add_edges lhs [x] g, g' ) 

154 
 (true , false) > (add_edges lhs [x] g, g' ) 

155 
 (true , true ) > (g , add_edges [x] lhs g') 

181 
if is_instance_var x  ISet.mem x node_vars then 

182 
if ISet.mem x mems 

183 
then 

184 
let g = add_edges lhs [mk_read_var x] g in 

185 
if lhs_is_mem 

186 
then 

187 
(g, add_edges [x] lhs g') 

188 
else 

189 
(add_edges [x] lhs g, g') 

190 
else 

191 
let x = if ISet.mem x inputs then mk_read_var x else x in 

192 
(add_edges lhs [x] g, g') 

156  193 
else (g, g') in 
157  194 
(* Add dependencies from [lhs] to rhs clock [ck]. *) 
158  195 
let rec add_clock lhs_is_mem lhs ck g = 
...  ...  
162  199 
 Clocks.Ccarrying (_, ck') > add_clock lhs_is_mem lhs ck' g 
163  200 
 _ > g 
164  201 
in 
165 


166  
167  202 
let rec add_dep lhs_is_mem lhs rhs g = 
168 


169  203 
(* Add mashup dependencies for a userdefined node instance [lhs] = [f]([e]) *) 
170  204 
(* i.e every input is connected to every output, through a ghost var *) 
171  205 
let mashup_appl_dependencies f e g = 
...  ...  
181  215 
 Expr_access (e1, _) 
182  216 
 Expr_power (e1, _) > add_dep lhs_is_mem lhs e1 g 
183  217 
 Expr_array a > List.fold_right (add_dep lhs_is_mem lhs) a g 
184 
 Expr_tuple t > 

218 
 Expr_tuple t > 

219 
(* 

185  220 
if List.length t <> List.length lhs then ( 
186  221 
match lhs with 
187  222 
 [l] > List.fold_right (fun r > add_dep lhs_is_mem [l] r) t g 
...  ...  
193  228 
(List.length t) 
194  229 
; 
195  230 
assert false 
196 
)


231 
) 

197  232 
else 
233 
*) 

198  234 
List.fold_right2 (fun l r > add_dep lhs_is_mem [l] r) lhs t g 
199  235 
 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) 
200  236 
 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)) 
...  ...  
214  250 
 Expr_dclock (e, _) 
215  251 
 Expr_phclock (e, _) > add_dep lhs_is_mem lhs e g 
216  252 
in 
217 
add_dep false eq.eq_lhs eq.eq_rhs (add_vertices eq.eq_lhs g, g') 

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') 

218  257 

219  258  
220  259 
(* Returns the dependence graph for node [n] *) 
221 
let dependence_graph mems non_inputs n = 

222 
eq_var_cpt := 0; 

260 
let dependence_graph mems inputs node_vars n = 

223  261 
instance_var_cpt := 0; 
224  262 
let g = new_graph (), new_graph () in 
225  263 
(* Basic dependencies *) 
226 
let g = List.fold_right (add_eq_dependencies mems non_inputs) n.node_eqs g in


264 
let g = List.fold_right (add_eq_dependencies mems inputs node_vars) n.node_eqs g in


227  265 
g 
228  266  
229  267 
end 
...  ...  
364  402 
let break_cycle head cp_head g = 
365  403 
let succs = IdentDepGraph.succ g head in 
366  404 
IdentDepGraph.add_edge g head cp_head; 
405 
IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head); 

367  406 
List.iter 
368  407 
(fun s > 
369  408 
IdentDepGraph.remove_edge g head s; 
...  ...  
451  490  
452  491 
let global_dependency node = 
453  492 
let mems = ExprDep.node_memory_variables node in 
454 
let non_inputs = ExprDep.node_non_input_variables node in 

455 
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems non_inputs node in 

493 
let inputs = ExprDep.node_input_variables node in 

494 
let node_vars = ExprDep.node_variables node in 

495 
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in 

456  496 
(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; 
457  497 
Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*) 
458  498 
CycleDetection.check_cycles g_non_mems; 
Also available in: Unified diff
added warnings for useless variables (at verbose level 1)
 exact definition of 'useless' may be further refined
 display could certainly be improved