lustrec / src / checks / liveness.ml @ 684d39e7
History  View  Annotate  Download (12.2 KB)
1 
(********************************************************************) 

2 
(* *) 
3 
(* The LustreC compiler toolset / The LustreC Development Team *) 
4 
(* Copyright 2012   ONERA  CNRS  INPT *) 
5 
(* *) 
6 
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) 
7 
(* under the terms of the GNU Lesser General Public License *) 
8 
(* version 2.1. *) 
9 
(* *) 
10 
(********************************************************************) 
11  
12 
open Utils 
13 
open Lustre_types 
14 
open Corelang 
15 
open Graph 
16 
open Causality 
17  
18 
type context = 
19 
{ 
20 
mutable evaluated : Disjunction.CISet.t; 
21 
dep_graph : IdentDepGraph.t; 
22 
disjoint : (ident, Disjunction.CISet.t) Hashtbl.t; 
23 
policy : (ident, var_decl) Hashtbl.t; 
24 
} 
25  
26 
(* computes the indegree for each local variable of node [n], according to dep graph [g]. 
27 
*) 
28 
let compute_fanin n g = 
29 
let locals = ISet.diff (ExprDep.node_local_variables n) (ExprDep.node_memory_variables n) in 
30 
let inputs = ExprDep.node_input_variables n in 
31 
let fanin = Hashtbl.create 23 in 
32 
begin 
33 
IdentDepGraph.iter_vertex 
34 
(fun v > 
35 
if ISet.mem v locals 
36 
then Hashtbl.add fanin v (IdentDepGraph.in_degree g v) else 
37 
if ExprDep.is_read_var v && not (ISet.mem v inputs) 
38 
then Hashtbl.add fanin (ExprDep.undo_read_var v) (IdentDepGraph.in_degree g v)) g; 
39 
fanin 
40 
end 
41 

42 
let pp_fanin fmt fanin = 
43 
begin 
44 
Format.fprintf fmt "{ /* locals fanin: */@."; 
45 
Hashtbl.iter (fun s t > Format.fprintf fmt "%s > %d@." s t) fanin; 
46 
Format.fprintf fmt "}@." 
47 
end 
48  
49 
(* computes the cone of influence of a given [var] wrt a dependency graph [g]. 
50 
*) 
51 
let cone_of_influence g var = 
52 
(*Format.printf "coi: %s@." var;*) 
53 
let frontier = ref (ISet.add var ISet.empty) in 
54 
let coi = ref ISet.empty in 
55 
while not (ISet.is_empty !frontier) 
56 
do 
57 
let head = ISet.min_elt !frontier in 
58 
(*Format.printf "head: %s@." head;*) 
59 
frontier := ISet.remove head !frontier; 
60 
if ExprDep.is_read_var head then coi := ISet.add (ExprDep.undo_read_var head) !coi; 
61 
List.iter (fun s > frontier := ISet.add s !frontier) (IdentDepGraph.succ g head); 
62 
done; 
63 
!coi 
64  
65 
let compute_unused_variables n g = 
66 
let inputs = ExprDep.node_input_variables n in 
67 
let mems = ExprDep.node_memory_variables n in 
68 
let outputs = ExprDep.node_output_variables n in 
69 
ISet.fold 
70 
(fun var unused > ISet.diff unused (cone_of_influence g var)) 
71 
(ISet.union outputs mems) 
72 
(ISet.union inputs mems) 
73  
74 
(* computes the set of potentially reusable variables. 
75 
We don't reuse input variables, due to possible aliasing *) 
76 
let node_reusable_variables node = 
77 
let mems = ExprDep.node_memory_variables node in 
78 
List.fold_left 
79 
(fun acc l > 
80 
if ISet.mem l.var_id mems then acc else Disjunction.CISet.add l acc) 
81 
Disjunction.CISet.empty 
82 
node.node_locals 
83  
84 
let kill_instance_variables ctx inst = 
85 
IdentDepGraph.remove_vertex ctx.dep_graph inst 
86  
87 
let kill_root ctx head = 
88 
IdentDepGraph.iter_succ (IdentDepGraph.remove_edge ctx.dep_graph head.var_id) ctx.dep_graph head.var_id 
89  
90 
(* Recursively removes useless variables, 
91 
i.e. [ctx.evaluated] variables that are current roots of the dep graph [ctx.dep_graph] 
92 
 [evaluated] is the set of already evaluated variables, 
93 
wrt the scheduling 
94 
 does only remove edges, not variables themselves 
95 
 yet, instance variables are removed 
96 
*) 
97 
let remove_roots ctx = 
98 
let rem = ref true in 
99 
let remaining = ref ctx.evaluated in 
100 
while !rem 
101 
do 
102 
rem := false; 
103 
let all_roots = graph_roots ctx.dep_graph in 
104 
let inst_roots, var_roots = List.partition (fun v > ExprDep.is_instance_var v && v <> Causality.world) all_roots in 
105 
let frontier_roots = Disjunction.CISet.filter (fun v > List.mem v.var_id var_roots) !remaining in 
106 
if not (Disjunction.CISet.is_empty frontier_roots && inst_roots = []) then 
107 
begin 
108 
rem := true; 
109 
List.iter (kill_instance_variables ctx) inst_roots; 
110 
Disjunction.CISet.iter (kill_root ctx) frontier_roots; 
111 
remaining := Disjunction.CISet.diff !remaining frontier_roots 
112 
end 
113 
done 
114 

115 
(* checks whether a variable is aliasable, 
116 
depending on its (address) type *) 
117 
let is_aliasable var = 
118 
(not (!Options.mpfr && Types.is_real_type var.var_type)) && Types.is_address_type var.var_type 
119 

120 
(* checks whether a variable [v] is an input of the [var] equation, with an address type. 
121 
if so, [var] could not safely reuse/alias [v], should [v] be dead in the caller node, 
122 
because [v] may not be dead in the callee node when [var] is assigned *) 
123 
let is_aliasable_input node var = 
124 
let eq_var = get_node_eq var node in 
125 
let inputs_var = 
126 
match NodeDep.get_callee eq_var.eq_rhs with 
127 
 None > [] 
128 
 Some (_, args) > List.fold_right (fun e r > match e.expr_desc with Expr_ident id > id::r  _ > r) args [] in 
129 
fun v > is_aliasable v && List.mem v.var_id inputs_var 
130  
131 
(* replace variable [v] by [v'] in graph [g]. 
132 
[v'] is a dead variable 
133 
*) 
134 
let replace_in_dep_graph v v' g = 
135 
begin 
136 
IdentDepGraph.add_vertex g v'; 
137 
IdentDepGraph.iter_succ (fun s > IdentDepGraph.add_edge g v' s) g v; 
138 
IdentDepGraph.iter_pred (fun p > IdentDepGraph.add_edge g p v') g v; 
139 
IdentDepGraph.remove_vertex g v 
140 
end 
141  
142 
let pp_reuse_policy fmt policy = 
143 
begin 
144 
Format.fprintf fmt "{ /* reuse policy */@."; 
145 
Hashtbl.iter (fun s t > Format.fprintf fmt "%s > %s@." s t.var_id) policy; 
146 
Format.fprintf fmt "}@." 
147 
end 
148  
149 
let pp_context fmt ctx = 
150 
begin 
151 
Format.fprintf fmt "{ /*BEGIN context */@."; 
152 
Format.fprintf fmt "eval=%a;@." Disjunction.pp_ciset ctx.evaluated; 
153 
Format.fprintf fmt "graph=%a;@." pp_dep_graph ctx.dep_graph; 
154 
Format.fprintf fmt "disjoint=%a;@." Disjunction.pp_disjoint_map ctx.disjoint; 
155 
Format.fprintf fmt "policy=%a;@." pp_reuse_policy ctx.policy; 
156 
Format.fprintf fmt "/* END context */ }@."; 
157 
end 
158  
159 
(* computes the reusable dependencies of variable [var] in graph [g], 
160 
once [var] has been evaluated 
161 
 [locals] is the set of potentially reusable variables 
162 
 [evaluated] is the set of evaluated variables 
163 
 [quasi] is the set of quasireusable variables 
164 
 [reusable] is the set of dead/reusable dependencies of [var] in graph [g] 
165 
 [policy] is the reuse map (which domain is [evaluated]) 
166 
*) 
167 
let compute_dependencies heads ctx = 
168 
begin 
169 
(*Log.report ~level:6 (fun fmt > Format.fprintf fmt "compute_reusable_dependencies %a %a %a@." Disjunction.pp_ciset locals Printers.pp_var_name var pp_context ctx);*) 
170 
List.iter (kill_root ctx) heads; 
171 
remove_roots ctx; 
172 
end 
173  
174 
let compute_evaluated heads ctx = 
175 
begin 
176 
List.iter (fun head > ctx.evaluated < Disjunction.CISet.add head ctx.evaluated) heads; 
177 
end 
178  
179 
(* tests whether a variable [v] may be (re)used instead of [var]. The conditions are: 
180 
 [v] has been really used ([v] is its own representative) 
181 
 same type 
182 
 [v] is not an aliasable input of the equation defining [var] 
183 
 [v] is not one of the current heads (which contain [var]) 
184 
 [v] is not currently in use 
185 
*) 
186 
let eligible node ctx heads var v = 
187 
Hashtbl.find ctx.policy v.var_id == v 
188 
&& Typing.eq_ground (Types.unclock_type var.var_type) (Types.unclock_type v.var_type) 
189 
&& not (is_aliasable_input node var.var_id v) 
190 
&& not (List.exists (fun h > h.var_id = v.var_id) heads) 
191 
&& (*let repr_v = Hashtbl.find ctx.policy v.var_id*) 
192 
not (Disjunction.CISet.exists (fun p > IdentDepGraph.mem_edge ctx.dep_graph p.var_id v.var_id) ctx.evaluated) 
193  
194 
let compute_reuse node ctx heads var = 
195 
let disjoint = Hashtbl.find ctx.disjoint var.var_id in 
196 
let locally_reusable v = 
197 
IdentDepGraph.fold_pred (fun p r > r && Disjunction.CISet.exists (fun d > p = d.var_id) disjoint) ctx.dep_graph v.var_id true in 
198 
let eligibles = Disjunction.CISet.filter (eligible node ctx heads var) ctx.evaluated in 
199 
Log.report ~level:7 (fun fmt > Format.fprintf fmt "eligibles:%a@." Disjunction.pp_ciset eligibles); 
200 
let quasi_dead, live = Disjunction.CISet.partition locally_reusable eligibles in 
201 
Log.report ~level:7 (fun fmt > Format.fprintf fmt "live:%a@." Disjunction.pp_ciset live); 
202 
try 
203 
let disjoint_live = Disjunction.CISet.inter disjoint live in 
204 
Log.report ~level:7 (fun fmt > Format.fprintf fmt "disjoint live:%a@." Disjunction.pp_ciset disjoint_live); 
205 
let reuse = Disjunction.CISet.max_elt disjoint_live in 
206 
begin 
207 
IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id; 
208 
Hashtbl.add ctx.policy var.var_id reuse; 
209 
ctx.evaluated < Disjunction.CISet.add var ctx.evaluated; 
210 
(*Format.eprintf "%s reused by live@." var.var_id;*) 
211 
end 
212 
with Not_found > 
213 
try 
214 
let dead = Disjunction.CISet.filter (fun v > is_graph_root v.var_id ctx.dep_graph) quasi_dead in 
215 
Log.report ~level:7 (fun fmt > Format.fprintf fmt "dead:%a@." Disjunction.pp_ciset dead); 
216 
let reuse = Disjunction.CISet.choose dead in 
217 
begin 
218 
IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id; 
219 
Hashtbl.add ctx.policy var.var_id reuse; 
220 
ctx.evaluated < Disjunction.CISet.add var ctx.evaluated; 
221 
(*Format.eprintf "%s reused by dead %s@." var.var_id reuse.var_id;*) 
222 
end 
223 
with Not_found > 
224 
begin 
225 
Hashtbl.add ctx.policy var.var_id var; 
226 
ctx.evaluated < Disjunction.CISet.add var ctx.evaluated; 
227 
end 
228  
229 
let compute_reuse_policy node schedule disjoint g = 
230 
let sort = ref schedule in 
231 
let ctx = { evaluated = Disjunction.CISet.empty; 
232 
dep_graph = g; 
233 
disjoint = disjoint; 
234 
policy = Hashtbl.create 23; } in 
235 
while !sort <> [] 
236 
do 
237 
Log.report ~level:6 (fun fmt > Format.fprintf fmt "new context:%a@." pp_context ctx); 
238 
let heads = List.map (fun v > get_node_var v node) (List.hd !sort) in 
239 
Log.report ~level:6 (fun fmt > Format.fprintf fmt "NEW HEADS:"); 
240 
List.iter (fun head > Log.report ~level:6 (fun fmt > Format.fprintf fmt "%s (%a)" head.var_id Printers.pp_node_eq (get_node_eq head.var_id node))) heads; 
241 
Log.report ~level:6 (fun fmt > Format.fprintf fmt "@."); 
242 
Log.report ~level:6 (fun fmt > Format.fprintf fmt "COMPUTE_DEPENDENCIES@."); 
243 
compute_dependencies heads ctx; 
244 
Log.report ~level:6 (fun fmt > Format.fprintf fmt "new context:%a@." pp_context ctx); 
245 
Log.report ~level:6 (fun fmt > Format.fprintf fmt "COMPUTE_REUSE@."); 
246 
List.iter (compute_reuse node ctx heads) heads; 
247 
(*compute_evaluated heads ctx;*) 
248 
List.iter (fun head > Log.report ~level:6 (fun fmt > Format.fprintf fmt "reuse %s instead of %s@." (Hashtbl.find ctx.policy head.var_id).var_id head.var_id)) heads; 
249 
sort := List.tl !sort; 
250 
done; 
251 
IdentDepGraph.clear ctx.dep_graph; 
252 
ctx.policy 
253  
254 
(* Reuse policy: 
255 
 could reuse variables with the same type exactly only (simple). 
256 
 reusing variables with different types would involve: 
257 
 either dirty castings 
258 
 or complex inclusion expression (for instance: array <> array cell, struct <> struct field) to be able to reuse only some parts of structured data. 
259 
... it seems too complex and potentially unsafe 
260 
 for node instance calls: output variables could NOT reuse aliasable input variables, 
261 
even if inputs become dead, because the correctness would depend on the scheduling 
262 
of the callee (so, the compiling strategy could NOT be modular anymore). 
263 
 once a policy is set, we need to: 
264 
 replace each variable by its reuse alias. 
265 
 simplify resulting equations, as we may now have: 
266 
x = x; > ; for scalar vars 
267 
or: 
268 
x = &{ f1 = x>f1; f2 = t; } > x>f2 = t; for struct vars 
269 
*) 
270  
271  
272 
(* the reuse policy seeks to use less local variables 
273 
by replacing local variables, applying the rules 
274 
in the following order: 
275 
1) use another clock disjoint still live variable, 
276 
with the greatest possible disjoint clock 
277 
2) reuse a dead variable 
278 
For the sake of safety, we replace variables by others: 
279 
 with the same type 
280 
 not aliasable (i.e. address type) 
281 
*) 
282  
283 
(* Local Variables: *) 
284 
(* compilecommand:"make C .." *) 
285 
(* End: *) 