## lustrec / src / liveness.ml @ 1837ce98

History | View | Annotate | Download (9.65 KB)

1 | d4101ea0 | xthirioux | (* ---------------------------------------------------------------------------- |
---|---|---|---|

2 | * SchedMCore - A MultiCore Scheduling Framework |
||

3 | * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
||

4 | * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE |
||

5 | * |
||

6 | * This file is part of Prelude |
||

7 | * |
||

8 | * Prelude is free software; you can redistribute it and/or |
||

9 | * modify it under the terms of the GNU Lesser General Public License |
||

10 | * as published by the Free Software Foundation ; either version 2 of |
||

11 | * the License, or (at your option) any later version. |
||

12 | * |
||

13 | * Prelude is distributed in the hope that it will be useful, but |
||

14 | * WITHOUT ANY WARRANTY ; without even the implied warranty of |
||

15 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
||

16 | * Lesser General Public License for more details. |
||

17 | * |
||

18 | * You should have received a copy of the GNU Lesser General Public |
||

19 | * License along with this program ; if not, write to the Free Software |
||

20 | * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
||

21 | * USA |
||

22 | *---------------------------------------------------------------------------- *) |
||

23 | |||

24 | open Utils |
||

25 | open LustreSpec |
||

26 | open Corelang |
||

27 | 9aaee7f9 | xthirioux | open Graph |

28 | d4101ea0 | xthirioux | open Causality |

29 | |||

30 | (* Computes the last dependency |
||

31 | *) |
||

32 | |||

33 | (* Computes the death table of [node] wrt dep graph [g] and topological [sort]. |
||

34 | The death table is a mapping: ident -> Set(ident) such that: |
||

35 | death x is the set of local variables which get dead (i.e. unused) |
||

36 | after x is evaluated, but were until live. |
||

37 | let death_table node g sort = |
||

38 | let death = Hashtbl.create 23 in |
||

39 | let sort = ref (List.rev sort) in |
||

40 | let buried = ref ISet.empty in |
||

41 | begin |
||

42 | buried := ExprDep.node_memory_variables node; |
||

43 | buried := List.fold_left (fun dead (v : var_decl) -> ISet.add v.var_id dead) !buried node.node_outputs; |
||

44 | (* We could also try to reuse input variables, due to C parameter copying semantics *) |
||

45 | buried := List.fold_left (fun dead (v : var_decl) -> ISet.add v.var_id dead) !buried node.node_inputs; |
||

46 | while (!sort <> []) |
||

47 | do |
||

48 | let head = List.hd !sort in |
||

49 | let dead = IdentDepGraph.fold_succ |
||

50 | (fun tgt dead -> if not (ExprDep.is_instance_var tgt || ISet.mem tgt !buried) then ISet.add tgt dead else dead) |
||

51 | g head ISet.empty in |
||

52 | buried := ISet.union !buried dead; |
||

53 | Hashtbl.add death head dead; |
||

54 | sort := List.tl !sort |
||

55 | done; |
||

56 | IdentDepGraph.clear g; |
||

57 | death |
||

58 | end |
||

59 | *) |
||

60 | |||

61 | d96d54ac | xthirioux | (* computes the in-degree for each local variable of node [n], according to dep graph [g]. |

62 | *) |
||

63 | let compute_fanin n g = |
||

64 | let locals = ISet.diff (ExprDep.node_local_variables n) (ExprDep.node_memory_variables n) in |
||

65 | let fanin = Hashtbl.create 23 in |
||

66 | begin |
||

67 | IdentDepGraph.iter_vertex (fun v -> if ISet.mem v locals then Hashtbl.add fanin v (IdentDepGraph.in_degree g v)) g; |
||

68 | fanin |
||

69 | end |
||

70 | |||

71 | let pp_fanin fmt fanin = |
||

72 | begin |
||

73 | Format.fprintf fmt "{ /* locals fanin: */@."; |
||

74 | Hashtbl.iter (fun s t -> Format.fprintf fmt "%s -> %d@." s t) fanin; |
||

75 | Format.fprintf fmt "}@." |
||

76 | end |
||

77 | 9aaee7f9 | xthirioux | |

78 | (* computes the cone of influence of a given [var] wrt a dependency graph [g]. |
||

79 | *) |
||

80 | let cone_of_influence g var = |
||

81 | (*Format.printf "coi: %s@." var;*) |
||

82 | let frontier = ref (ISet.add var ISet.empty) in |
||

83 | let coi = ref ISet.empty in |
||

84 | while not (ISet.is_empty !frontier) |
||

85 | do |
||

86 | let head = ISet.min_elt !frontier in |
||

87 | (*Format.printf "head: %s@." head;*) |
||

88 | frontier := ISet.remove head !frontier; |
||

89 | if ExprDep.is_read_var head then coi := ISet.add (ExprDep.undo_read_var head) !coi; |
||

90 | List.iter (fun s -> frontier := ISet.add s !frontier) (IdentDepGraph.succ g head); |
||

91 | done; |
||

92 | !coi |
||

93 | |||

94 | let compute_unused n g = |
||

95 | let inputs = ExprDep.node_input_variables n in |
||

96 | let mems = ExprDep.node_memory_variables n in |
||

97 | let outputs = ExprDep.node_output_variables n in |
||

98 | ISet.fold |
||

99 | (fun var unused -> ISet.diff unused (cone_of_influence g var)) |
||

100 | (ISet.union outputs mems) |
||

101 | (ISet.union inputs mems) |
||

102 | |||

103 | d4101ea0 | xthirioux | (* Computes the set of (input and) output and mem variables of [node]. |

104 | We try to reuse input variables, due to C parameter copying semantics. *) |
||

105 | let node_non_locals node = |
||

106 | List.fold_left (fun non_loc v -> ISet.add v.var_id non_loc) (ExprDep.node_memory_variables node) node.node_outputs |
||

107 | |||

108 | (* Recursively removes useless local variables, |
||

109 | i.e. variables in [non_locals] that are current roots of the dep graph [g] *) |
||

110 | let remove_local_roots non_locals g = |
||

111 | let rem = ref true in |
||

112 | let roots = ref ISet.empty in |
||

113 | while !rem |
||

114 | do |
||

115 | rem := false; |
||

116 | let local_roots = List.filter (fun v -> not (ISet.mem v non_locals)) (graph_roots g) in |
||

117 | if local_roots <> [] then |
||

118 | begin |
||

119 | rem := true; |
||

120 | List.iter (IdentDepGraph.remove_vertex g) local_roots; |
||

121 | roots := List.fold_left (fun roots v -> if ExprDep.is_instance_var v then roots else ISet.add v roots) !roots local_roots |
||

122 | end |
||

123 | done; |
||

124 | !roots |
||

125 | |||

126 | (* Computes the death table of [node] wrt dep graph [g] and topological [sort]. |
||

127 | The death table is a mapping: ident -> Set(ident) such that: |
||

128 | death x is the set of local variables which get dead (i.e. unused) |
||

129 | before x is evaluated, but were until live. |
||

130 | 3c48346d | xthirioux | If death x is not defined, then x is useless. |

131 | d4101ea0 | xthirioux | *) |

132 | let death_table node g sort = |
||

133 | let non_locals = node_non_locals node in |
||

134 | let death = Hashtbl.create 23 in |
||

135 | let sort = ref sort in |
||

136 | begin |
||

137 | while (!sort <> []) |
||

138 | do |
||

139 | let head = List.hd !sort in |
||

140 | 3c48346d | xthirioux | (* If current var is not already dead, i.e. useless *) |

141 | if IdentDepGraph.mem_vertex g head then |
||

142 | d4101ea0 | xthirioux | begin |

143 | IdentDepGraph.iter_succ (IdentDepGraph.remove_edge g head) g head; |
||

144 | 3c48346d | xthirioux | let dead = remove_local_roots non_locals g in |

145 | Hashtbl.add death head dead |
||

146 | end; |
||

147 | d4101ea0 | xthirioux | sort := List.tl !sort |

148 | done; |
||

149 | IdentDepGraph.clear g; |
||

150 | death |
||

151 | end |
||

152 | |||

153 | let pp_death_table fmt death = |
||

154 | begin |
||

155 | Format.fprintf fmt "{ /* death table */@."; |
||

156 | Hashtbl.iter (fun s t -> Format.fprintf fmt "%s -> { %a }@." s (Utils.fprintf_list ~sep:", " Format.pp_print_string) (ISet.elements t)) death; |
||

157 | Format.fprintf fmt "}@." |
||

158 | end |
||

159 | |||

160 | e8c0f452 | xthirioux | |

161 | (* Reuse policy: |
||

162 | - could reuse variables with the same type exactly only (simple). |
||

163 | - reusing variables with different types would involve: |
||

164 | - either dirty castings |
||

165 | - or complex inclusion expression (for instance: array <-> array cell, struct <-> struct field) to be able to reuse only some parts of structured data. |
||

166 | ... it seems too complex and potentially unsafe |
||

167 | - for node instance calls: output variables could NOT reuse input variables, |
||

168 | even if inputs become dead, because the correctness would depend on the scheduling |
||

169 | of the callee (so, the compiling strategy could NOT be modular anymore). |
||

170 | - once a policy is set, we need to: |
||

171 | - replace each variable by its reuse alias. |
||

172 | - simplify resulting equations, as we may now have: |
||

173 | x = x; --> ; for scalar vars |
||

174 | or: |
||

175 | x = &{ f1 = x->f1; f2 = t; } --> x->f2 = t; for struct vars |
||

176 | - such simplifications are, until now, only expressible at the C source level... |
||

177 | *) |
||

178 | |||

179 | d4101ea0 | xthirioux | (* Replaces [v] by [v'] in set [s] *) |

180 | let replace_in_set s v v' = |
||

181 | if ISet.mem v s then ISet.add v' (ISet.remove v s) else s |
||

182 | |||

183 | (* Replaces [v] by [v'] in death table [death] *) |
||

184 | let replace_in_death_table death v v' = |
||

185 | 3c48346d | xthirioux | Hashtbl.iter (fun k dead -> Hashtbl.replace death k (replace_in_set dead v v')) death |

186 | d4101ea0 | xthirioux | |

187 | 1837ce98 | xthirioux | let find_compatible_local node var dead death disjoint policy = |

188 | d96d54ac | xthirioux | (*Format.eprintf "find_compatible_local %s %s %a@." node.node_id var pp_iset dead;*) |

189 | 0038002e | ploc | let typ = (get_node_var var node).var_type in |

190 | let eq_var = get_node_eq var node in |
||

191 | 1837ce98 | xthirioux | let locals = node.node_locals in |

192 | d96d54ac | xthirioux | let aliasable_inputs = |

193 | e8c0f452 | xthirioux | match NodeDep.get_callee eq_var.eq_rhs with |

194 | | None -> [] |
||

195 | | Some (_, args) -> List.fold_right (fun e r -> match e.expr_desc with Expr_ident id -> id::r | _ -> r) args [] in |
||

196 | 1837ce98 | xthirioux | let filter base (v : var_decl) = |

197 | d96d54ac | xthirioux | let res = |

198 | 1837ce98 | xthirioux | base v |

199 | e8c0f452 | xthirioux | && Typing.eq_ground typ v.var_type |

200 | 1837ce98 | xthirioux | && not (Types.is_address_type v.var_type && List.mem v.var_id aliasable_inputs) in |

201 | d96d54ac | xthirioux | begin |

202 | (*Format.eprintf "filter %a = %s@." Printers.pp_var_name v (if res then "true" else "false");*) |
||

203 | res |
||

204 | end in |
||

205 | 1837ce98 | xthirioux | (*Format.eprintf "reuse %s@." var;*) |

206 | d4101ea0 | xthirioux | try |

207 | 1837ce98 | xthirioux | let disj = Hashtbl.find disjoint var in |

208 | let reuse = List.find (filter (fun v -> ISet.mem v.var_id disj && not (ISet.mem v.var_id dead))) locals in |
||

209 | (*Format.eprintf "reuse %s by %s@." var reuse.var_id;*) |
||

210 | Disjunction.replace_in_disjoint_map disjoint var reuse.var_id; |
||

211 | (*Format.eprintf "new disjoint:%a@." Disjunction.pp_disjoint_map disjoint;*) |
||

212 | Hashtbl.add policy var reuse.var_id |
||

213 | with Not_found -> |
||

214 | try |
||

215 | let reuse = List.find (filter (fun v -> ISet.mem v.var_id dead)) locals in |
||

216 | (*Format.eprintf "reuse %s by %s@." var reuse.var_id;*) |
||

217 | replace_in_death_table death var reuse.var_id; |
||

218 | (*Format.eprintf "new death:%a@." pp_death_table death;*) |
||

219 | Hashtbl.add policy var reuse.var_id |
||

220 | with Not_found -> () |
||

221 | d4101ea0 | xthirioux | |

222 | 1837ce98 | xthirioux | (* the reuse policy seeks to use less local variables |

223 | by replacing local variables, applying the rules |
||

224 | in the following order: |
||

225 | 1) use another clock disjoint still live variable, |
||

226 | with the greatest possible disjoint clock |
||

227 | 2) reuse a dead variable |
||

228 | For the sake of safety, we replace variables by others: |
||

229 | - with the same type |
||

230 | - not aliasable (i.e. address type) |
||

231 | *) |
||

232 | let reuse_policy node sort death disjoint = |
||

233 | d4101ea0 | xthirioux | let dead = ref ISet.empty in |

234 | let policy = Hashtbl.create 23 in |
||

235 | let sort = ref sort in |
||

236 | while !sort <> [] |
||

237 | do |
||

238 | let head = List.hd !sort in |
||

239 | 3c48346d | xthirioux | if Hashtbl.mem death head then |

240 | begin |
||

241 | dead := ISet.union (Hashtbl.find death head) !dead; |
||

242 | end; |
||

243 | 1837ce98 | xthirioux | find_compatible_local node head !dead death disjoint policy; |

244 | d4101ea0 | xthirioux | sort := List.tl !sort; |

245 | done; |
||

246 | policy |
||

247 | |||

248 | let pp_reuse_policy fmt policy = |
||

249 | begin |
||

250 | Format.fprintf fmt "{ /* reuse policy */@."; |
||

251 | Hashtbl.iter (fun s t -> Format.fprintf fmt "%s -> %s@." s t) policy; |
||

252 | Format.fprintf fmt "}@." |
||

253 | end |
||

254 | (* Local Variables: *) |
||

255 | (* compile-command:"make -C .." *) |
||

256 | (* End: *) |