lustrec / src / deadline_calculus.ml @ 0cbf0839
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: *) |