## lustrec / src / deadline_calculus.ml @ 587cdc0d

History | View | Annotate | Download (5.96 KB)

1 |
(* ---------------------------------------------------------------------------- |
---|---|

2 |
* SchedMCore - A MultiCore Scheduling Framework |

3 |
* Copyright (C) 2009-2011, 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 02111-1307 |

20 |
* USA |

21 |
*---------------------------------------------------------------------------- *) |

22 | |

23 |
open Format |

24 |
open Corelang |

25 |
open Task_graph |

26 |
open Task_set |

27 |
open Deadlines |

28 |
open Precedence_functions |

29 |
(** Encodes precedences by adjusting task deadlines. The names of the |

30 |
functions below refer to the names in the thesis manuscript *) |

31 | |

32 |
(* ----- Core functions *) |

33 |
let rec t_ops ops t = |

34 |
match ops with |

35 |
| [] -> t |

36 |
| (Gfby _)::rest -> |

37 |
t_ops rest t |

38 |
| (Guclock k)::rest -> |

39 |
k*(t_ops rest t) |

40 |
| (Gdclock k)::rest -> |

41 |
(t_ops rest t)/k |

42 |
| (Gphclock _)::rest -> |

43 |
t_ops rest t |

44 |
| Gtail::rest -> |

45 |
t_ops rest t |

46 |
| (Gconcat _)::rest -> |

47 |
t_ops rest t |

48 | |

49 |
let rec r_ops ops r t = |

50 |
match ops with |

51 |
| [] -> r |

52 |
| (Gfby _)::rest -> |

53 |
r_ops rest r t |

54 |
| (Guclock _)::rest -> |

55 |
r_ops rest r t |

56 |
| (Gdclock _)::rest -> |

57 |
r_ops rest r t |

58 |
| (Gphclock (a,b))::rest -> |

59 |
(r_ops rest r t) - a*(t_ops rest t)/b |

60 |
| Gtail::rest -> |

61 |
(r_ops rest r t) - (t_ops rest t) |

62 |
| (Gconcat _)::rest -> |

63 |
(r_ops rest r t) + (t_ops rest t) |

64 | |

65 |
let delta_ops ops ti tj rj n = |

66 |
(gops ops n)*tj-n*ti+rj-(r_ops ops rj tj) |

67 | |

68 |
(* delta_ops(ti,tj,rj) *) |

69 |
let delta_word ops ti tj rj = |

70 |
let lpref = pref_size ops in |

71 |
let lpat = periodicity ops in |

72 |
Array.init lpref (fun n -> delta_ops ops ti tj rj n), |

73 |
Array.init lpat (fun n -> delta_ops ops ti tj rj (n+lpref)) |

74 | |

75 |
(* P'(ops) *) |

76 |
let rec periodicity' wj ops = |

77 |
match ops with |

78 |
| [] -> pat_length wj |

79 |
| (Guclock k)::rest -> |

80 |
let pops = periodicity' wj rest in |

81 |
pops/(Utils.gcd k pops) |

82 |
| (Gdclock k):: rest -> |

83 |
k*(periodicity' wj rest) |

84 |
| (Gfby _)::rest -> |

85 |
periodicity' wj rest |

86 |
| (Gphclock _)::rest | Gtail::rest | (Gconcat _)::rest -> |

87 |
periodicity' wj rest |

88 | |

89 |
let rec pref_size' wj ops = |

90 |
let rec aux ops = |

91 |
match ops with |

92 |
| [] -> pref_length wj |

93 |
| (Guclock k)::rest -> |

94 |
let props = aux rest in |

95 |
int_of_float (ceil ((float_of_int props) /. (float_of_int k))) |

96 |
| (Gdclock k)::rest -> |

97 |
let props = aux rest in |

98 |
max ((props -1)*k+1) 0 |

99 |
| Gtail::rest -> |

100 |
(aux rest)+1 |

101 |
| (Gfby _)::rest | (Gconcat _)::rest -> |

102 |
let props = aux rest in |

103 |
max (props -1) 0 |

104 |
| (Gphclock _)::rest -> |

105 |
aux rest |

106 |
in |

107 |
max (aux ops) 0 |

108 | |

109 |
let w_ops wj ops = |

110 |
let lpref = pref_size' wj ops in |

111 |
let lpat = periodicity' wj ops in |

112 |
Array.init lpref (fun n -> nth_ud wj (gops ops n)), |

113 |
Array.init lpat (fun n -> nth_ud wj (gops ops n)) |

114 | |

115 |
(* Update deadlines to encode the precedence [from_v]-[annots]->[to_v]. *) |

116 |
let update_dd task_set from_v to_v annots = |

117 |
let task_from = task_of_vertex task_set from_v in |

118 |
let task_to = task_of_vertex task_set to_v in |

119 |
let wi = task_from.task_deadline in |

120 |
let ti = task_from.task_period in |

121 |
let wj = task_to.task_deadline in |

122 |
let tj = task_to.task_period in |

123 |
let rj = task_to.task_release in |

124 |
let cj = task_to.task_wcet in |

125 |
let delta = delta_word annots ti tj rj in |

126 |
let wops = w_ops wj annots in |

127 |
let cstr = add_int (add_dw delta wops) (-cj) in |

128 |
task_from.task_deadline <- min_dw wi cstr |

129 | |

130 |
(* ----- Functions for the topological traversal *) |

131 |
let count_succs g = |

132 |
(* Count successors of tasks, ie count the successors of all the variables |

133 |
of the task. *) |

134 |
let nb_succs = Hashtbl.create 30 in |

135 |
let add_succs v nb = |

136 |
let tid = taskid_of_vertex v in |

137 |
let nb' = |

138 |
try Hashtbl.find nb_succs tid with Not_found -> 0 in |

139 |
Hashtbl.replace nb_succs tid (nb'+nb) |

140 |
in |

141 |
Hashtbl.iter |

142 |
(fun vid v -> |

143 |
let nb = |

144 |
Hashtbl.fold |

145 |
(fun succ annot n -> |

146 |
if is_delayed_prec annot then n else n+1) |

147 |
v.vertex_succs 0 in |

148 |
add_succs vid nb) |

149 |
g.graph; |

150 |
nb_succs |

151 | |

152 |
(* Compute the initial set of vertices that have no successors *) |

153 |
let no_succs task_set nb_succs = |

154 |
Hashtbl.fold |

155 |
(fun tid nb acc -> |

156 |
if nb = 0 then |

157 |
let t = Hashtbl.find task_set tid in |

158 |
(inputs_of_task t)@acc |

159 |
else |

160 |
acc) |

161 |
nb_succs [] |

162 | |

163 |
(* Compute the new set of vertices that have no successors. *) |

164 |
let new_no_succs task_set nb_succs no_succs lost_one_succ = |

165 |
let tid = taskid_of_vertex lost_one_succ in |

166 |
let n = Hashtbl.find nb_succs tid in |

167 |
Hashtbl.replace nb_succs tid (n-1); |

168 |
if n = 1 then |

169 |
no_succs@(inputs_of_task (task_of_vertex task_set lost_one_succ)) |

170 |
else |

171 |
no_succs |

172 | |

173 |
let dd_prog g task_set exp_main = |

174 |
let nb_succs = count_succs g in |

175 |
(* Traversal of the graph as a classic reverse topological sort. *) |

176 |
let rec topo_traversal no_succs = |

177 |
match no_succs with |

178 |
| [] -> () |

179 |
| v::rest -> |

180 |
let pred = (Hashtbl.find g.graph v).vertex_pred in |

181 |
match pred with |

182 |
| None -> topo_traversal rest |

183 |
| Some (p, annot) -> |

184 |
if not (is_delayed_prec annot) then |

185 |
begin |

186 |
update_dd task_set p v annot; |

187 |
let no_succs' = new_no_succs task_set nb_succs rest p in |

188 |
topo_traversal no_succs' |

189 |
end |

190 |
else |

191 |
topo_traversal rest |

192 |
in |

193 |
let no_succs = no_succs task_set nb_succs in |

194 |
topo_traversal no_succs |

195 | |

196 |
(* Local Variables: *) |

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

198 |
(* End: *) |