Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / causality.ml @ add75bcb

History | View | Annotate | Download (18.1 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

    
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_local_variables nd =
139
 List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals
140

    
141
let node_output_variables nd =
142
 List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs
143

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

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

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

    
168

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

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

    
270
end
271

    
272
module NodeDep = struct
273

    
274
  module ExprModule =
275
  struct
276
    type t = expr
277
    let compare = compare
278
    let hash n = Hashtbl.hash n
279
    let equal n1 n2 = n1 = n2
280
  end
281

    
282
  module ESet = Set.Make(ExprModule)
283

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

    
306
  let get_callee expr =
307
    match expr.expr_desc with
308
    | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)
309
    | _ -> None
310

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

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

    
335
  let rec filter_static_inputs inputs args =
336
   match inputs, args with
337
   | []   , [] -> []
338
   | 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
339
   | _ -> assert false
340

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

    
352
end
353

    
354
module CycleDetection = struct
355

    
356
(* ---- Look for cycles in a dependency graph *)
357
  module Cycles = Graph.Components.Make (IdentDepGraph)
358

    
359
  let mk_copy_var n id =
360
    mk_new_name (node_vars n) id
361

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

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

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

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

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

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

    
445
end
446

    
447
(* Module used to compute static disjunction of variables based upon their clocks. *)
448
module Disjunction =
449
struct
450
  module ClockedIdentModule =
451
  struct
452
    type t = var_decl
453
    let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock
454
    let compare v1 v2 = compare (root_branch v2) (root_branch v1)
455
  end
456

    
457
  module CISet = Set.Make(ClockedIdentModule)
458

    
459
  (* map: var |-> list of disjoint vars, sorted in increasing branch length order,
460
     maybe removing shorter branches *)
461
  type clock_map = (ident, var_decl list) Hashtbl.t
462

    
463
  let clock_disjoint_map vdecls =
464
    let map = Hashtbl.create 23 in
465
    begin
466
      List.iter
467
	(fun v1 -> let disj_v1 =
468
		     List.fold_left
469
		       (fun res v2 -> if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res)
470
		       CISet.empty
471
		       vdecls in
472
		   (* disjoint vdecls are stored in increasing branch length order *)
473
		   Hashtbl.add map v1.var_id disj_v1)
474
	vdecls;
475
      map
476
    end
477

    
478
  (* replace variable [v] by [v'] in disjunction [map]. Then:
479
     - the mapping v |-> ... disappears
480
     - the mapping v' becomes v' |-> (map v) inter (map v')
481
     - other mappings become x |-> (map x) \ (if v in x then v else v')
482
  *)
483
  let replace_in_disjoint_map map v v' =
484
    begin
485
      Hashtbl.remove map v.var_id;
486
      Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id));
487
      Hashtbl.iter (fun x map_x -> Hashtbl.replace map x (CISet.remove (if CISet.mem v map_x then v else v') map_x)) map;
488
    end
489

    
490
  let pp_disjoint_map fmt map =
491
    begin
492
      Format.fprintf fmt "{ /* disjoint map */@.";
493
      Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map;
494
      Format.fprintf fmt "}@."
495
    end
496
end
497

    
498
let pp_dep_graph fmt g =
499
  begin
500
    Format.fprintf fmt "{ /* graph */@.";
501
    IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g;
502
    Format.fprintf fmt "}@."
503
  end
504

    
505
let pp_error fmt trace =
506
  fprintf fmt "@.Causality error, cyclic data dependencies: %a@."
507
    (fprintf_list ~sep:"->" pp_print_string) trace
508

    
509
(* Merges elements of graph [g2] into graph [g1] *)
510
let merge_with g1 g2 =
511
    IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
512
    IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
513

    
514
let global_dependency node =
515
  let mems = ExprDep.node_memory_variables node in
516
  let inputs = ExprDep.node_input_variables node in
517
  let node_vars = ExprDep.node_variables node in
518
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in
519
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
520
  Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
521
  CycleDetection.check_cycles g_non_mems;
522
  let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in
523
  (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
524
  merge_with g_non_mems g_mems';
525
  { node with node_eqs = eqs'; node_locals = vdecls'@node.node_locals }, 
526
  g_non_mems
527

    
528

    
529
(* Local Variables: *)
530
(* compile-command:"make -C .." *)
531
(* End: *)