Project

General

Profile

Revision e7cc5186 src/causality.ml

View differences:

src/causality.ml
18 18
open LustreSpec
19 19
open Corelang
20 20
open Graph
21
open Format
22 21

  
22

  
23
type identified_call = eq * tag
23 24
type error =
24
  | DataCycle of ident list
25
  | DataCycle of ident list list (* multiple failed partitions at once *) 
25 26
  | NodeCycle of ident list
26 27

  
27 28
exception Error of error
......
97 98
   but used to compute useless inputs/mems.
98 99
   a mem read var represents a mem at the beginning of a cycle  *)
99 100
  let mk_read_var id =
100
    sprintf "#%s" id
101
    Format.sprintf "#%s" id
101 102

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

  
109 110
  let is_read_var v = v.[0] = '#'
110 111

  
......
215 216
    (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
216 217
    (* i.e every input is connected to every output, through a ghost var *)
217 218
      let mashup_appl_dependencies f e g =
218
	let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in
219
	let f_var = mk_instance_var (Format.sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in
219 220
	List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)
220 221
	  (expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) 
221 222
      in
......
384 385

  
385 386
end
386 387

  
388

  
387 389
module CycleDetection = struct
388 390

  
389 391
  (* ---- Look for cycles in a dependency graph *)
......
420 422
     [Cycle partition] if the succession of dependencies [partition] forms a cycle *)
421 423
  let check_cycles g =
422 424
    let scc_l = Cycles.scc_list g in
423
    List.iter (fun partition ->
424
      if wrong_partition g partition then
425
	raise (Error (DataCycle partition))
426
      else ()
427
    ) scc_l
425
    let algebraic_loops = List.filter (wrong_partition g) scc_l in
426
    if List.length algebraic_loops > 0 then
427
      raise (Error (DataCycle algebraic_loops))
428
	(* We extract a hint to resolve the cycle: for each variable in the cycle
429
	   which is defined by a call, we return the name of the node call and
430
	   its specific id *)
428 431

  
429 432
  (* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
430 433
  let copy_partition g partition =
......
562 565
    end
563 566
end
564 567

  
568
  
565 569
let pp_dep_graph fmt g =
566 570
  begin
567 571
    Format.fprintf fmt "{ /* graph */@.";
......
571 575

  
572 576
let pp_error fmt err =
573 577
  match err with
574
  | DataCycle trace ->
575
     fprintf fmt "@.Causality error, cyclic data dependencies: %a@."
576
       (fprintf_list ~sep:", " pp_print_string) trace
577 578
  | NodeCycle trace ->
578
     fprintf fmt "@.Causality error, cyclic node calls: %a@."
579
       (fprintf_list ~sep:", " pp_print_string) trace
580

  
579
     Format.fprintf fmt "Causality error, cyclic node calls:@   @[<v 0>%a@]@ "
580
       (fprintf_list ~sep:",@ " Format.pp_print_string) trace
581
  | DataCycle traces -> (
582
     Format.fprintf fmt "Causality error, cyclic data dependencies:@   @[<v 0>%a@]@ "
583
       (fprintf_list ~sep:";@ "
584
       (fun fmt trace ->
585
	 Format.fprintf fmt "@[<v 0>{%a}@]"
586
	   (fprintf_list ~sep:",@ " Format.pp_print_string)
587
	   trace
588
       )) traces
589
  )
590
     
581 591
(* Merges elements of graph [g2] into graph [g1] *)
582 592
let merge_with g1 g2 =
583 593
  begin
......
605 615
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in
606 616
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
607 617
    Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
608
  CycleDetection.check_cycles g_non_mems;
609
  let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in
610
  (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
611
  begin
612
    merge_with g_non_mems g_mems';
613
    add_external_dependency outputs mems g_non_mems;
614
    { node with node_stmts = List.map (fun eq -> Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, 
615
    g_non_mems
616
  end
618
  try
619
    CycleDetection.check_cycles g_non_mems;
620
    let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in
621
    (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
622
    begin
623
      merge_with g_non_mems g_mems';
624
      add_external_dependency outputs mems g_non_mems;
625
      { node with node_stmts = List.map (fun eq -> Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, 
626
      g_non_mems
627
    end
628
  with Error (DataCycle _ as exc) -> (
629
      raise (Error (exc))
630
  )
617 631

  
618 632
(* Local Variables: *)
619 633
(* compile-command:"make -C .." *)

Also available in: Unified diff