Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / deadline_calculus.ml @ 22fe1c93

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