Project

General

Profile

Download (17.3 KB) Statistics
| Branch: | Tag: | Revision:
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

    
24
(** Simple modular syntactic causality analysis. Can reject correct
25
    programs, especially if the program is not flattened first. *)
26
open Utils
27
open LustreSpec
28
open Corelang
29
open Graph
30
open Format
31

    
32
exception Cycle of ident list
33

    
34
module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule)
35

    
36
(* Dependency of mem variables on mem variables is cut off 
37
   by duplication of some mem vars into local node vars.
38
   Thus, cylic dependency errors may only arise between no-mem vars.
39
   non-mem variables are:
40
   - inputs: not needed for causality/scheduling, needed only for detecting useless vars
41
   - read mems (fake vars): same remark as above.
42
   - outputs: decoupled from mems, if necessary
43
   - locals
44
   - instance vars (fake vars): simplify causality analysis
45

    
46
   global constants are not part of the dependency graph.
47

    
48
no_mem' = combinational(no_mem, mem);
49
=> (mem -> no_mem' -> no_mem)
50

    
51
mem' = pre(no_mem, mem);
52
=> (mem' -> no_mem), (mem -> mem')
53

    
54
   Global roadmap:
55
   - compute two dep graphs g (non-mem/non-mem&mem) and g' (mem/mem)
56
   - check cycles in g (a cycle means a dependency error)
57
   - break cycles in g' (it's legal !):
58
     - check cycles in g'
59
     - if any, introduce aux var to break cycle, then start afresh
60
   - insert g' into g
61
   - return g
62
*)
63

    
64
(* Tests whether [v] is a root of graph [g], i.e. a source *)
65
let is_graph_root v g =
66
 IdentDepGraph.in_degree g v = 0
67

    
68
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *)
69
let graph_roots g =
70
 IdentDepGraph.fold_vertex
71
   (fun v roots -> if is_graph_root v g then v::roots else roots)
72
   g []
73

    
74
let add_edges src tgt g =
75
(*List.iter (fun s -> List.iter (fun t -> Format.eprintf "add %s -> %s@." s t) tgt) src;*)
76
 List.iter
77
   (fun s ->
78
     List.iter
79
       (fun t -> IdentDepGraph.add_edge g s t)
80
       tgt)
81
   src;
82
  g
83

    
84
let add_vertices vtc g =
85
(*List.iter (fun t -> Format.eprintf "add %s@." t) vtc;*)
86
 List.iter (fun v -> IdentDepGraph.add_vertex g v) vtc;
87
  g
88

    
89
let new_graph () =
90
 IdentDepGraph.create ()
91

    
92
module ExprDep = struct
93

    
94
let instance_var_cpt = ref 0
95

    
96
(* read vars represent input/mem read-only vars,
97
   they are not part of the program/schedule,
98
   as they are not assigned,
99
   but used to compute useless inputs/mems.
100
   a mem read var represents a mem at the beginning of a cycle  *)
101
let mk_read_var id =
102
 sprintf "#%s" id
103

    
104
(* instance vars represent node instance calls,
105
   they are not part of the program/schedule,
106
   but used to simplify causality analysis
107
    *)
108
let mk_instance_var id =
109
 incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt
110

    
111
let is_read_var v = v.[0] = '#'
112

    
113
let is_instance_var v = v.[0] = '!'
114

    
115
let is_ghost_var v = is_instance_var v || is_read_var v
116

    
117
let undo_read_var id =
118
 assert (is_read_var id);
119
 String.sub id 1 (String.length id - 1)
120

    
121
let eq_memory_variables mems eq =
122
  let rec match_mem lhs rhs mems =
123
    match rhs.expr_desc with
124
    | Expr_fby _
125
    | Expr_pre _    -> List.fold_right ISet.add lhs mems
126
    | Expr_tuple tl -> 
127
      let lhs' = (transpose_list [lhs]) in
128
      List.fold_right2 match_mem lhs' tl mems
129
    | _             -> mems in
130
  match_mem eq.eq_lhs eq.eq_rhs mems
131

    
132
let node_memory_variables nd =
133
 List.fold_left eq_memory_variables ISet.empty nd.node_eqs
134

    
135
let node_input_variables nd =
136
 List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty nd.node_inputs
137

    
138
let node_output_variables nd =
139
 List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs
140

    
141
let node_variables nd =
142
  let inputs = node_input_variables nd in
143
  let inoutputs = List.fold_left (fun inoutputs v -> ISet.add v.var_id inoutputs) inputs nd.node_outputs in
144
  List.fold_left (fun vars v -> ISet.add v.var_id vars) inoutputs nd.node_locals
145

    
146
(* computes the equivalence relation relating variables 
147
   in the same equation lhs, under the form of a table 
148
   of class representatives *)
149
let node_eq_equiv nd =
150
  let eq_equiv = Hashtbl.create 23 in
151
  List.iter (fun eq ->
152
    let first = List.hd eq.eq_lhs in
153
    List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs
154
  )
155
    nd.node_eqs;
156
  eq_equiv
157

    
158
(* Create a tuple of right dimension, according to [expr] type, *)
159
(* filled with variable [v] *)
160
let adjust_tuple v expr =
161
 match expr.expr_type.Types.tdesc with
162
 | Types.Ttuple tl -> duplicate v (List.length tl)
163
 | _         -> [v]
164

    
165

    
166
(* Add dependencies from lhs to rhs in [g, g'], *)
167
(* no-mem/no-mem and mem/no-mem in g            *)
168
(* mem/mem in g'                                *)
169
(*     match (lhs_is_mem, ISet.mem x mems) with
170
      | (false, true ) -> (add_edges [x] lhs g,
171
			   g')
172
      | (false, false) -> (add_edges lhs [x] g,
173
			   g')
174
      | (true , false) -> (add_edges lhs [x] g,
175
			   g')
176
      | (true , true ) -> (g,
177
			   add_edges [x] lhs g')
178
*)
179
let add_eq_dependencies mems inputs node_vars eq (g, g') =
180
  let add_var lhs_is_mem lhs x (g, g') =
181
    if is_instance_var x || ISet.mem x node_vars then
182
      if ISet.mem x mems
183
      then
184
	let g = add_edges lhs [mk_read_var x] g in
185
	if lhs_is_mem
186
	then
187
	  (g, add_edges [x] lhs g')
188
	else
189
	  (add_edges [x] lhs g, g')
190
      else
191
	let x = if ISet.mem x inputs then mk_read_var x else x in
192
	(add_edges lhs [x] g, g')
193
    else (g, g') in
194
(* Add dependencies from [lhs] to rhs clock [ck]. *)
195
  let rec add_clock lhs_is_mem lhs ck g =
196
    (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
197
    match (Clocks.repr ck).Clocks.cdesc with
198
    | Clocks.Con (ck', cr, _)   -> add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g)
199
    | Clocks.Ccarrying (_, ck') -> add_clock lhs_is_mem lhs ck' g
200
    | _                         -> g 
201
  in
202
  let rec add_dep lhs_is_mem lhs rhs g =
203
    (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
204
    (* i.e every input is connected to every output, through a ghost var *)
205
    let mashup_appl_dependencies f e g =
206
      let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in
207
      List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)
208
	(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) 
209
    in
210
    match rhs.expr_desc with
211
    | Expr_const _    -> g
212
    | Expr_fby (e1, e2)  -> add_dep true lhs e2 (add_dep false lhs e1 g)
213
    | Expr_pre e      -> add_dep true lhs e g
214
    | Expr_ident x -> add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g)
215
    | Expr_access (e1, _)
216
    | Expr_power (e1, _) -> add_dep lhs_is_mem lhs e1 g
217
    | Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g
218
    | Expr_tuple t ->
219
(*
220
      if List.length t <> List.length lhs then ( 
221
	match lhs with
222
	| [l] -> List.fold_right (fun r -> add_dep lhs_is_mem [l] r) t g
223
	| _ -> 
224
	  Format.eprintf "Incompatible tuple assign: %a (%i) vs %a (%i)@.@?" 
225
	    (Utils.fprintf_list ~sep:"," (Format.pp_print_string)) lhs 
226
	    (List.length lhs)
227
	    Printers.pp_expr rhs
228
	    (List.length t)
229
	  ;
230
	  assert false
231
      )
232
      else
233
*)
234
	List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g
235
    | Expr_merge (c, hl) -> add_var lhs_is_mem lhs c (List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g)
236
    | Expr_ite   (c, t, e) -> add_dep lhs_is_mem lhs c (add_dep lhs_is_mem lhs t (add_dep lhs_is_mem lhs e g))
237
    | Expr_arrow (e1, e2)  -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)
238
    | Expr_when  (e, c, _)  -> add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)
239
    | Expr_appl (f, e, None) ->
240
      if Basic_library.is_internal_fun f
241
      (* tuple component-wise dependency for internal operators *)
242
      then
243
	List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g
244
      (* mashed up dependency for user-defined operators *)
245
      else
246
	mashup_appl_dependencies f e g
247
    | Expr_appl (f, e, Some (r, _)) ->
248
      mashup_appl_dependencies f e (add_var lhs_is_mem lhs r g)
249
    | Expr_uclock  (e, _)
250
    | Expr_dclock  (e, _)
251
    | Expr_phclock (e, _) -> add_dep lhs_is_mem lhs e g 
252
  in
253
  let g =
254
    List.fold_left
255
      (fun g lhs -> if ISet.mem lhs mems then add_vertices [lhs; mk_read_var lhs] g else add_vertices [lhs] g) g eq.eq_lhs in
256
  add_dep false eq.eq_lhs eq.eq_rhs (g, g')
257
  
258

    
259
(* Returns the dependence graph for node [n] *)
260
let dependence_graph mems inputs node_vars n =
261
  instance_var_cpt := 0;
262
  let g = new_graph (), new_graph () in
263
  (* Basic dependencies *)
264
  let g = List.fold_right (add_eq_dependencies mems inputs node_vars) n.node_eqs g in
265
  g
266

    
267
end
268

    
269
module NodeDep = struct
270

    
271
  module ExprModule =
272
  struct
273
    type t = expr
274
    let compare = compare
275
    let hash n = Hashtbl.hash n
276
    let equal n1 n2 = n1 = n2
277
  end
278

    
279
  module ESet = Set.Make(ExprModule)
280

    
281
  let rec get_expr_calls prednode expr = 
282
    match expr.expr_desc with
283
      | Expr_const _ 
284
      | Expr_ident _ -> ESet.empty
285
      | Expr_access (e, _)
286
      | Expr_power (e, _) -> get_expr_calls prednode e
287
      | Expr_array t
288
      | Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty
289
      | Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty
290
      | Expr_fby (e1,e2)
291
      | Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
292
      | Expr_ite   (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
293
      | Expr_pre e 
294
      | Expr_when (e,_,_)
295
      | Expr_uclock (e,_) 
296
      | Expr_dclock (e,_) 
297
      | Expr_phclock (e,_) -> get_expr_calls prednode e
298
      | Expr_appl (id,e, _) ->
299
	if not (Basic_library.is_internal_fun id) && prednode id
300
	then ESet.add expr (get_expr_calls prednode e)
301
	else (get_expr_calls prednode e)
302

    
303
  let get_callee expr =
304
    match expr.expr_desc with
305
    | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)
306
    | _ -> None
307

    
308
  let get_calls prednode eqs =
309
    let deps =
310
      List.fold_left 
311
	(fun accu eq -> ESet.union accu (get_expr_calls prednode eq.eq_rhs))
312
	ESet.empty
313
	eqs in
314
    ESet.elements deps
315

    
316
  let dependence_graph prog =
317
  let g = new_graph () in
318
  let g = List.fold_right 
319
    (fun td accu -> (* for each node we add its dependencies *)
320
      match td.top_decl_desc with 
321
	| Node nd ->
322
	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
323
	  let accu = add_vertices [nd.node_id] accu in
324
	  let deps = List.map (fun e -> fst (desome (get_callee e))) (get_calls (fun _ -> true) nd.node_eqs) in
325
	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
326
	  add_edges [nd.node_id] deps accu
327
	| _ -> assert false (* should not happen *)
328
      
329
    ) prog g in
330
  g   
331

    
332
  let rec filter_static_inputs inputs args =
333
   match inputs, args with
334
   | []   , [] -> []
335
   | v::vq, a::aq -> if v.var_dec_const then (dimension_of_expr a) :: filter_static_inputs vq aq else filter_static_inputs vq aq
336
   | _ -> assert false
337

    
338
  let compute_generic_calls prog =
339
    List.iter
340
      (fun td ->
341
	match td.top_decl_desc with 
342
	| Node nd ->
343
	  let prednode n = is_generic_node (Hashtbl.find node_table n) in
344
	  nd.node_gencalls <- get_calls prednode nd.node_eqs
345
	| _ -> ()
346
      
347
      ) prog
348

    
349
end
350

    
351
module CycleDetection = struct
352

    
353
(* ---- Look for cycles in a dependency graph *)
354
  module Cycles = Graph.Components.Make (IdentDepGraph)
355

    
356
  let mk_copy_var n id =
357
    mk_new_name (node_vars n) id
358

    
359
  let mk_copy_eq n var =
360
    let var_decl = node_var var n in
361
    let cp_var = mk_copy_var n var in
362
    let expr =
363
      { expr_tag = Utils.new_tag ();
364
	expr_desc = Expr_ident var;
365
	expr_type = var_decl.var_type;
366
	expr_clock = var_decl.var_clock;
367
	expr_delay = Delay.new_var ();
368
	expr_annot = None;
369
	expr_loc = var_decl.var_loc } in
370
    { var_decl with var_id = cp_var },
371
    mkeq var_decl.var_loc ([cp_var], expr)
372

    
373
  let wrong_partition g partition =
374
    match partition with
375
    | [id]    -> IdentDepGraph.mem_edge g id id
376
    | _::_::_ -> true
377
    | []      -> assert false
378

    
379
(* Checks that the dependency graph [g] does not contain a cycle. Raises
380
   [Cycle partition] if the succession of dependencies [partition] forms a cycle *)
381
  let check_cycles g =
382
    let scc_l = Cycles.scc_list g in
383
    List.iter (fun partition ->
384
      if wrong_partition g partition then
385
	raise (Cycle partition)
386
      else ()
387
    ) scc_l
388

    
389
(* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
390
  let copy_partition g partition =
391
    let copy_g = IdentDepGraph.create () in
392
    IdentDepGraph.iter_edges
393
      (fun src tgt ->
394
	if List.mem src partition && List.mem tgt partition
395
	then IdentDepGraph.add_edge copy_g src tgt)
396
      g
397

    
398
 
399
(* Breaks dependency cycles in a graph [g] by inserting aux variables.
400
  [head] is a head of a non-trivial scc of [g]. 
401
   In Lustre, this is legal only for mem/mem cycles *)
402
  let break_cycle head cp_head g =
403
    let succs = IdentDepGraph.succ g head in
404
    IdentDepGraph.add_edge g head cp_head;
405
    IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head);
406
    List.iter
407
      (fun s ->
408
	IdentDepGraph.remove_edge g head s;
409
	IdentDepGraph.add_edge    g s cp_head)
410
      succs
411

    
412
(* Breaks cycles of the dependency graph [g] of memory variables [mems]
413
   belonging in node [node]. Returns:
414
   - a list of new auxiliary variable declarations
415
   - a list of new equations
416
   - a modified acyclic version of [g]
417
*)
418
  let break_cycles node mems g =
419
    let (mem_eqs, non_mem_eqs) = List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) node.node_eqs in
420
    let rec break vdecls mem_eqs g =
421
      let scc_l = Cycles.scc_list g in
422
      let wrong = List.filter (wrong_partition g) scc_l in
423
      match wrong with
424
      | []              -> (vdecls, non_mem_eqs@mem_eqs, g)
425
      | [head]::_       ->
426
	begin
427
	  IdentDepGraph.remove_edge g head head;
428
	  break vdecls mem_eqs g
429
	end
430
      | (head::part)::_ -> 
431
	begin
432
	  let vdecl_cp_head, cp_eq = mk_copy_eq node head in
433
	  let pvar v = List.mem v part in
434
	  let fvar v = if v = head then vdecl_cp_head.var_id else v in
435
	  let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in
436
	  break_cycle head vdecl_cp_head.var_id g;
437
	  break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g
438
	end
439
      | _               -> assert false
440
    in break [] mem_eqs g
441

    
442
end
443

    
444
(* Module used to compute static disjunction of variables based upon their clocks. *)
445
module Disjunction =
446
struct
447
  (* map: var |-> list of disjoint vars, sorted in increasing branch length,
448
     maybe removing shorter branches *)
449
  type clock_map = (ident, ident list) Hashtbl.t
450

    
451
  let rec add_vdecl map vdecls =
452
    match vdecls with
453
    | []         -> ()
454
    | vdecl :: q -> begin
455
		      Hashtbl.add map vdecl.var_id (List.fold_left (fun r v -> if Clocks.disjoint v.var_clock vdecl.var_clock then v.var_id::r else r) [] q);
456
                      add_vdecl map q
457
		    end
458

    
459
  let clock_disjoint_map vdecls =
460
    let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock in
461
    let map = Hashtbl.create 23 in
462
    begin
463
      add_vdecl map (List.sort (fun v1 v2 -> compare (root_branch v1) (root_branch v2)) vdecls);
464
      map
465
    end
466

    
467
  let pp_disjoint_map fmt map =
468
    begin
469
      Format.fprintf fmt "{ /* disjoint map */@.";
470
      Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Format.pp_print_string) v) map;
471
      Format.fprintf fmt "}@."
472
    end
473
end
474

    
475
let pp_dep_graph fmt g =
476
  begin
477
    Format.fprintf fmt "{ /* graph */@.";
478
    IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g;
479
    Format.fprintf fmt "}@."
480
  end
481

    
482
let pp_error fmt trace =
483
  fprintf fmt "@.Causality error, cyclic data dependencies: %a@."
484
    (fprintf_list ~sep:"->" pp_print_string) trace
485

    
486
(* Merges elements of graph [g2] into graph [g1] *)
487
let merge_with g1 g2 =
488
    IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
489
    IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
490

    
491
let global_dependency node =
492
  let mems = ExprDep.node_memory_variables node in
493
  let inputs = ExprDep.node_input_variables node in
494
  let node_vars = ExprDep.node_variables node in
495
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in
496
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
497
  Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
498
  CycleDetection.check_cycles g_non_mems;
499
  let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in
500
  (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
501
  merge_with g_non_mems g_mems';
502
  { node with node_eqs = eqs'; node_locals = vdecls'@node.node_locals }, 
503
  g_non_mems
504

    
505

    
506
(* Local Variables: *)
507
(* compile-command:"make -C .." *)
508
(* End: *)
(5-5/49)