From 051b2d07e66a89281fde102e850a4fc386dabdae Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 17 Dec 2020 12:36:28 +0000 Subject: Fix whitespace --- src/SoftwarePipelining/SPBasic.ml | 834 ++++++++++++------------ src/SoftwarePipelining/SPIMS.ml | 165 +++-- src/SoftwarePipelining/SPMVE.ml | 291 ++++----- src/SoftwarePipelining/SPSymbolic_evaluation.ml | 170 ++--- src/SoftwarePipelining/SPTyping.ml | 4 +- src/SoftwarePipelining/SoftwarePipelining.ml | 36 +- 6 files changed, 748 insertions(+), 752 deletions(-) (limited to 'src') diff --git a/src/SoftwarePipelining/SPBasic.ml b/src/SoftwarePipelining/SPBasic.ml index 1269faf..dd2b5c1 100644 --- a/src/SoftwarePipelining/SPBasic.ml +++ b/src/SoftwarePipelining/SPBasic.ml @@ -23,8 +23,8 @@ open SPSymbolic_evaluation type node = instruction * int module G = Graph.Persistent.Digraph.AbstractLabeled - (struct type t = node end) - (struct type t = int let compare = compare let default = 0 end) + (struct type t = node end) + (struct type t = int let compare = compare let default = 0 end) module Topo = Graph.Topological.Make (G) module Dom = Graph.Dominator.Make (G) module Index = Map.Make (struct type t = int let compare = compare end) @@ -37,7 +37,7 @@ let string_of_instruction node = | (Istore (chunk, mode, args, src),n) -> Printf.sprintf "%i store %i %s" n (to_int src) (string_of_args args) | (Icall (sign, id, args, dst),n) -> Printf.sprintf "%i call" n | (Itailcall (sign, id, args),n) -> Printf.sprintf "%i tailcall" n -(* | (Ialloc (dst, size),n) -> Printf.sprintf "%i %i := alloc" n (to_int dst) *) + (* | (Ialloc (dst, size),n) -> Printf.sprintf "%i %i := alloc" n (to_int dst) *) | (Icond (cond, args),n) -> Printf.sprintf "%i cond %s %s" n (string_of_cond cond) (string_of_args args) | (Ireturn (res),n) -> Printf.sprintf "%i return" n @@ -66,7 +66,7 @@ let display g name = ignore (Sys.command ("(dot -Tpng " ^ addr ^ " -o " ^ addr ^ ".png ; rm -f " ^ addr ^ ") & ")) (******************************************) - + type cfg = {graph : G.t; start : G.V.t} (* convert traduit un graphe RTL compcert en un graphe RTL ocamlgraph*) @@ -79,58 +79,58 @@ let convert f = in let (graph, index) = Maps.PTree.fold (fun (g,m) key inst -> - let node = make_node inst key in - (G.add_vertex g node, Index.add (to_int key) node m) - ) f.fn_code (G.empty,Index.empty) + let node = make_node inst key in + (G.add_vertex g node, Index.add (to_int key) node m) + ) f.fn_code (G.empty,Index.empty) in let succ = RTL.successors_map f in let rec link n succs g = match succs with - | [] -> g - | pos::[] -> - G.add_edge g (Index.find (to_int n) index) (Index.find (to_int pos) index) - | pos1::pos2::[] -> - let g = G.add_edge_e g (G.E.create (Index.find (to_int n) index) 1 (Index.find (to_int pos1) index)) in - G.add_edge_e g (G.E.create (Index.find (to_int n) index) 2 (Index.find (to_int pos2) index)) - | _ -> failwith "convert : trop de successeurs" - + | [] -> g + | pos::[] -> + G.add_edge g (Index.find (to_int n) index) (Index.find (to_int pos) index) + | pos1::pos2::[] -> + let g = G.add_edge_e g (G.E.create (Index.find (to_int n) index) 1 (Index.find (to_int pos1) index)) in + G.add_edge_e g (G.E.create (Index.find (to_int n) index) 2 (Index.find (to_int pos2) index)) + | _ -> failwith "convert : trop de successeurs" + in let graph = Maps.PTree.fold ( fun g key inst -> - link key (match Maps.PTree.get key succ with + link key (match Maps.PTree.get key succ with Some x -> x | _ -> failwith "Could not index") g - ) f.fn_code graph + ) f.fn_code graph in - + {graph = graph; start = Index.find (to_int (f.fn_entrypoint)) index} - - + + let convert_back g = - - G.fold_vertex (fun node m -> - let v = G.V.label node in - match (fst v) with - | Icond (_,_) -> - begin - let l = - match G.succ_e g node with - | [e1;e2] -> - if G.E.label e1 > G.E.label e2 - then [G.E.dst e2;G.E.dst e1] - else [G.E.dst e1;G.E.dst e2] - | _ -> failwith "convert_back: nombre de successeurs incoherent" - in - let succs = List.map (fun s -> to_binpos (snd (G.V.label s))) l in - Maps.PTree.set (to_binpos (snd v)) (inst_caml_to_coq (fst v) succs) m - end - | _ -> - let succs = List.map (fun s -> to_binpos (snd (G.V.label s))) (G.succ g node) in - Maps.PTree.set (to_binpos (snd v)) (inst_caml_to_coq (fst v) succs) m - ) g Maps.PTree.empty - - - + + G.fold_vertex (fun node m -> + let v = G.V.label node in + match (fst v) with + | Icond (_,_) -> + begin + let l = + match G.succ_e g node with + | [e1;e2] -> + if G.E.label e1 > G.E.label e2 + then [G.E.dst e2;G.E.dst e1] + else [G.E.dst e1;G.E.dst e2] + | _ -> failwith "convert_back: nombre de successeurs incoherent" + in + let succs = List.map (fun s -> to_binpos (snd (G.V.label s))) l in + Maps.PTree.set (to_binpos (snd v)) (inst_caml_to_coq (fst v) succs) m + end + | _ -> + let succs = List.map (fun s -> to_binpos (snd (G.V.label s))) (G.succ g node) in + Maps.PTree.set (to_binpos (snd v)) (inst_caml_to_coq (fst v) succs) m + ) g Maps.PTree.empty + + + (* dominator_tree calcule l'arbre de domination grace au code de FP *) let dominator_tree f = @@ -142,16 +142,16 @@ let dominator_tree f = let detect_loops graph dom_tree = let rec is_dominating v1 v2 l = (* does v1 dominate v2 *) match dom_tree v2 with - | v -> if v1 = v then Some (v :: l) - else is_dominating v1 v (v :: l) - | exception (Not_found) -> None + | v -> if v1 = v then Some (v :: l) + else is_dominating v1 v (v :: l) + | exception (Not_found) -> None in G.fold_edges (fun v1 v2 loops -> - match is_dominating v2 v1 [v1] with - | None -> loops - | Some loop -> (v2,loop) :: loops - ) graph [] + match is_dominating v2 v1 [v1] with + | None -> loops + | Some loop -> (v2,loop) :: loops + ) graph [] let print_index node = Printf.printf "%i " (snd (G.V.label node)) @@ -167,43 +167,43 @@ let print_instruction node = (*| (Ialloc (dst, size),n) -> Printf.printf "%i : Ialloc \n" n *) | (Icond (cond, args),n) -> Printf.printf "%i : Icond \n" n | (Ireturn (res),n) -> Printf.printf "%i : Ireturn \n" n - + let is_rewritten node r = match fst (G.V.label node) with - | Inop -> false - | Iop (op, args, dst) -> if dst = r then true else false - | Iload (chunk, mode, args, dst) -> if dst = r then failwith "J'ai degote une boucle ZARBI !!!" else false - | Istore (chunk, mode, args, src) -> false - | Icall (sign, id, args, dst) -> failwith "call in a loop" - | Itailcall (sign, id, args) -> failwith "tailcall in a loop" -(* | Ialloc (dst, size) -> if dst = r then failwith "J'ai degote une boucle ZARBI !!!" else false *) - | Icond (cond, args) -> false - | Ireturn (res) -> failwith "return in a loop" + | Inop -> false + | Iop (op, args, dst) -> if dst = r then true else false + | Iload (chunk, mode, args, dst) -> if dst = r then failwith "J'ai degote une boucle ZARBI !!!" else false + | Istore (chunk, mode, args, src) -> false + | Icall (sign, id, args, dst) -> failwith "call in a loop" + | Itailcall (sign, id, args) -> failwith "tailcall in a loop" + (* | Ialloc (dst, size) -> if dst = r then failwith "J'ai degote une boucle ZARBI !!!" else false *) + | Icond (cond, args) -> false + | Ireturn (res) -> failwith "return in a loop" let is_variant r loop = List.fold_right (fun node b -> - is_rewritten node r || b - ) loop false + is_rewritten node r || b + ) loop false let is_pipelinable loop = (* true if loop is innermost and without control *) - + let is_acceptable node = match fst (G.V.label node) with - | Icall _ | Itailcall _ | Ireturn _ | Icond _ (*| Ialloc _*) | Iop ((Ocmp _),_,_)-> false - | _ -> true + | Icall _ | Itailcall _ | Ireturn _ | Icond _ (*| Ialloc _*) | Iop ((Ocmp _),_,_)-> false + | _ -> true in - + let is_branching node = match fst (G.V.label node) with - | Icond _ -> true - | _ -> false + | Icond _ -> true + | _ -> false in let is_nop node = match fst (G.V.label node) with - | Inop -> true - | _ -> false + | Inop -> true + | _ -> false in let is_OK_aux l = @@ -212,160 +212,160 @@ let is_pipelinable loop = (* true if loop is innermost and without control *) let is_bounded node loop = match G.V.label node with - | (Icond (cond, args),n) -> - let args = to_caml_list args in - begin - match args with - | [] -> false - | r :: [] -> is_variant r loop (* used to be not *) - | r1 :: r2 :: [] -> - begin - match is_variant r1 loop, is_variant r2 loop with - | true, true -> false - | false, true -> true - | true, false -> true - | false, false -> false - end - | _ -> false - end - | _ -> false + | (Icond (cond, args),n) -> + let args = to_caml_list args in + begin + match args with + | [] -> false + | r :: [] -> not (is_variant r loop) (* used to be not *) + | r1 :: r2 :: [] -> + begin + match is_variant r1 loop, is_variant r2 loop with + | true, true -> false + | false, true -> true + | true, false -> true + | false, false -> false + end + | _ -> false + end + | _ -> false in match List.rev loop with - | v2 :: v1 :: l -> ((*Printf.printf "is_nop: %s | " (is_nop v1 |> string_of_bool);*) - Printf.printf "is_branching: %s | " (is_branching v2 |> string_of_bool); - Printf.printf "is_OK_aux: %s | " (is_OK_aux l |> string_of_bool); - Printf.printf "is_bounded: %s\n" (is_bounded v2 loop |> string_of_bool); - (*is_nop v1 && *)is_branching v2 && is_OK_aux l && is_bounded v2 loop) - | _ -> false - + | v2 :: v1 :: l -> ((*Printf.printf "is_nop: %s | " (is_nop v1 |> string_of_bool);*) + Printf.printf "is_branching: %s | " (is_branching v2 |> string_of_bool); + Printf.printf "is_OK_aux: %s | " (is_OK_aux l |> string_of_bool); + Printf.printf "is_bounded: %s\n" (is_bounded v2 loop |> string_of_bool); + (*is_nop v1 && *)is_branching v2 && is_OK_aux l && is_bounded v2 loop) + | _ -> false + let print_loops loops = List.iter (fun loop -> print_index (fst(loop)); - print_newline (); - List.iter print_index (snd(loop)); - print_newline (); - if is_pipelinable (snd(loop)) then print_string "PIPELINABLE !" else print_string "WASTE"; - print_newline (); - List.iter print_instruction (snd(loop)); - print_newline () - ) loops - + print_newline (); + List.iter print_index (snd(loop)); + print_newline (); + if is_pipelinable (snd(loop)) then print_string "PIPELINABLE !" else print_string "WASTE"; + print_newline (); + List.iter print_instruction (snd(loop)); + print_newline () + ) loops + (* type resource = Reg of reg | Mem *) module Sim = Map.Make (struct type t = resource let compare = compare end) let map_get key map = try Some (Sim.find key map) with - | Not_found -> None + | Not_found -> None let rec to_res l = match l with - | [] -> [] - | e :: l -> Reg e :: to_res l + | [] -> [] + | e :: l -> Reg e :: to_res l let resources_reads_of node = match fst (G.V.label node) with - | Inop -> [] - | Iop (op, args, dst) -> to_res args - | Iload (chunk, mode, args, dst) -> Mem :: (to_res args) - | Istore (chunk, mode, args, src) -> Mem :: Reg src :: (to_res args) - | Icall (sign, id, args, dst) -> failwith "Resource read of call" - | Itailcall (sign, id, args) -> failwith "Resource read of tailcall" - (*| Ialloc (dst, size) -> [Mem] *) - | Icond (cond, args) -> to_res args - | Ireturn (res) -> failwith "Resource read of return" - + | Inop -> [] + | Iop (op, args, dst) -> to_res args + | Iload (chunk, mode, args, dst) -> Mem :: (to_res args) + | Istore (chunk, mode, args, src) -> Mem :: Reg src :: (to_res args) + | Icall (sign, id, args, dst) -> failwith "Resource read of call" + | Itailcall (sign, id, args) -> failwith "Resource read of tailcall" + (*| Ialloc (dst, size) -> [Mem] *) + | Icond (cond, args) -> to_res args + | Ireturn (res) -> failwith "Resource read of return" + let resources_writes_of node = match fst (G.V.label node) with - | Inop -> [] - | Iop (op, args, dst) -> [Reg dst] - | Iload (chunk, mode, args, dst) -> [Reg dst] - | Istore (chunk, mode, args, src) -> [Mem] - | Icall (sign, id, args, dst) -> failwith "Resource read of call" - | Itailcall (sign, id, args) -> failwith "Resource read of tailcall" - (*| Ialloc (dst, size) -> (Reg dst) :: [Mem]*) - | Icond (cond, args) -> [] - | Ireturn (res) -> failwith "Resource read of return" - + | Inop -> [] + | Iop (op, args, dst) -> [Reg dst] + | Iload (chunk, mode, args, dst) -> [Reg dst] + | Istore (chunk, mode, args, src) -> [Mem] + | Icall (sign, id, args, dst) -> failwith "Resource read of call" + | Itailcall (sign, id, args) -> failwith "Resource read of tailcall" + (*| Ialloc (dst, size) -> (Reg dst) :: [Mem]*) + | Icond (cond, args) -> [] + | Ireturn (res) -> failwith "Resource read of return" + let build_intra_dependency_graph loop = - + let rec build_aux graph read write l = match l with - | [] -> (graph,(read,write)) - | v :: l-> - let g = G.add_vertex graph v in - let reads = resources_reads_of v in - let writes = resources_writes_of v in - (* dependances RAW *) - let g = List.fold_right (fun r g -> - match map_get r write with - | Some n -> G.add_edge_e g (G.E.create n 1 v) - | None -> g - ) reads g in - (* dependances WAR *) - let g = List.fold_right (fun r g -> - match map_get r read with - | Some l -> List.fold_right (fun n g -> G.add_edge_e g (G.E.create n 2 v)) l g - | None -> g - ) writes g in - (* dependances WAW *) - let g = List.fold_right (fun r g -> - match map_get r write with - | Some n -> G.add_edge_e g (G.E.create n 3 v) - | None -> g - ) writes g in - let write = List.fold_right (fun r m -> Sim.add r v m) writes write in - let read_tmp = List.fold_right (fun r m -> - match map_get r read with - | Some al -> Sim.add r (v :: al) m - | None -> Sim.add r (v :: []) m - ) reads read - in - let read = List.fold_right (fun r m -> Sim.add r [] m) writes read_tmp in - - build_aux g read write l + | [] -> (graph,(read,write)) + | v :: l-> + let g = G.add_vertex graph v in + let reads = resources_reads_of v in + let writes = resources_writes_of v in + (* dependances RAW *) + let g = List.fold_right (fun r g -> + match map_get r write with + | Some n -> G.add_edge_e g (G.E.create n 1 v) + | None -> g + ) reads g in + (* dependances WAR *) + let g = List.fold_right (fun r g -> + match map_get r read with + | Some l -> List.fold_right (fun n g -> G.add_edge_e g (G.E.create n 2 v)) l g + | None -> g + ) writes g in + (* dependances WAW *) + let g = List.fold_right (fun r g -> + match map_get r write with + | Some n -> G.add_edge_e g (G.E.create n 3 v) + | None -> g + ) writes g in + let write = List.fold_right (fun r m -> Sim.add r v m) writes write in + let read_tmp = List.fold_right (fun r m -> + match map_get r read with + | Some al -> Sim.add r (v :: al) m + | None -> Sim.add r (v :: []) m + ) reads read + in + let read = List.fold_right (fun r m -> Sim.add r [] m) writes read_tmp in + + build_aux g read write l in build_aux G.empty Sim.empty Sim.empty (List.tl loop) - + let build_inter_dependency_graph loop = let rec build_aux2 graph read write l = match l with - | [] -> graph - | v :: l-> - let g = graph in - let reads = resources_reads_of v in - let writes = resources_writes_of v in - (* dependances RAW *) - let g = List.fold_right (fun r g -> - match map_get r write with - | Some n -> (* if n = v then g else *) G.add_edge_e g (G.E.create n 4 v) - | None -> g - ) reads g in - (* dependances WAR *) - let g = List.fold_right (fun r g -> - match map_get r read with - | Some l -> List.fold_right - (fun n g -> (* if n = v then g else *) G.add_edge_e g (G.E.create n 5 v)) l g - | None -> g - ) writes g in - (* dependances WAW *) - let g = List.fold_right (fun r g -> - match map_get r write with - | Some n -> (* if n = v then g else *) G.add_edge_e g (G.E.create n 6 v) - | None -> g - ) writes g in - let write = List.fold_right (fun r m -> Sim.remove r m) writes write in - let read = List.fold_right (fun r m -> Sim.remove r m) writes read in - - - build_aux2 g read write l + | [] -> graph + | v :: l-> + let g = graph in + let reads = resources_reads_of v in + let writes = resources_writes_of v in + (* dependances RAW *) + let g = List.fold_right (fun r g -> + match map_get r write with + | Some n -> (* if n = v then g else *) G.add_edge_e g (G.E.create n 4 v) + | None -> g + ) reads g in + (* dependances WAR *) + let g = List.fold_right (fun r g -> + match map_get r read with + | Some l -> List.fold_right + (fun n g -> (* if n = v then g else *) G.add_edge_e g (G.E.create n 5 v)) l g + | None -> g + ) writes g in + (* dependances WAW *) + let g = List.fold_right (fun r g -> + match map_get r write with + | Some n -> (* if n = v then g else *) G.add_edge_e g (G.E.create n 6 v) + | None -> g + ) writes g in + let write = List.fold_right (fun r m -> Sim.remove r m) writes write in + let read = List.fold_right (fun r m -> Sim.remove r m) writes read in + + + build_aux2 g read write l in let (g,(r,w)) = build_intra_dependency_graph loop in build_aux2 g r w (List.tl loop) - + (* patch_graph prepare le graphe pour la boucle commencant au noeud entry qui a une borne de boucle bound et pour un software pipelining de au minimum min tours et de deroulement ur *) @@ -390,7 +390,7 @@ let patch_graph graph entry lastone loop bound min ur r1 r2 r3 r4 next_pc prolog let wannabes = List.filter (fun e -> not (e = lastone)) wannabes in let graph = List.fold_right (fun e g -> G.remove_edge_e g e) preds_e graph in let graph = G.add_edge graph lastone entry in - + (* 2. Add the test for minimal iterations and link it*) let cond = G.V.create (Icond ((Ccompimm (Integers.Cle,min)),to_coq_list [bound]), next_pc) in @@ -400,11 +400,11 @@ let patch_graph graph entry lastone loop bound min ur r1 r2 r3 r4 next_pc prolog (* 3. Link its predecessors and successors *) (* It is false in case there is a condition that points to the entry: inthis case, the edge should not be labeled with 0 !*) - + let graph = List.fold_right (fun n g -> G.add_edge g n cond) wannabes graph in let graph = G.add_edge_e graph (G.E.create cond 1 entry) in - + (* 4. Add the div and modulo code, link it *) let n1 = G.V.create (Iop ((Ointconst ur),to_coq_list [],r1),next_pc) in let next_pc = next_pc + 1 in @@ -426,56 +426,56 @@ let patch_graph graph entry lastone loop bound min ur r1 r2 r3 r4 next_pc prolog let graph = G.add_edge graph n2 n3 in let graph = G.add_edge graph n3 n4 in let graph = G.add_edge graph n4 n5 in - + (* 5. Fabriquer la pipelined loop et la linker, sans la condition d entree *) - + let (graph,next_pc,l) = List.fold_right (fun e (g,npc,l) -> - let n = G.V.create (e,npc) in - (G.add_vertex g n, npc+1, n :: l) - ) loop (graph,next_pc,[]) in + let n = G.V.create (e,npc) in + (G.add_vertex g n, npc+1, n :: l) + ) loop (graph,next_pc,[]) in let pipe_cond = List.hd l in let pipeline = List.tl l in - + let rec link l graph node = match l with - | n1 :: n2 :: l -> link (n2 :: l) (G.add_edge graph n1 n2) node - | n1 :: [] -> G.add_edge graph n1 node - | _ -> graph + | n1 :: n2 :: l -> link (n2 :: l) (G.add_edge graph n1 n2) node + | n1 :: [] -> G.add_edge graph n1 node + | _ -> graph in - + let graph = link pipeline graph pipe_cond in - + (* link de l entree de la boucle *) - + let (graph,next_pc,prolog) = List.fold_right (fun e (g,npc,l) -> - let n = G.V.create (e,npc) in - (G.add_vertex g n, npc+1, n :: l) - ) prolog (graph,next_pc,[]) in + let n = G.V.create (e,npc) in + (G.add_vertex g n, npc+1, n :: l) + ) prolog (graph,next_pc,[]) in let (graph,next_pc,epilog) = List.fold_right (fun e (g,npc,l) -> - let n = G.V.create (e,npc) in - (G.add_vertex g n, npc+1, n :: l) - ) epilog (graph,next_pc,[]) in + let n = G.V.create (e,npc) in + (G.add_vertex g n, npc+1, n :: l) + ) epilog (graph,next_pc,[]) in (* 6. Creation du reste et branchement et la condition *) let n6 = G.V.create (Iop (Omove,to_coq_list [r4],bound),next_pc) in (* Iop (Omove,to_coq_list [r4],bound) *) let next_pc = next_pc + 1 in - + (* 7. Creation du ramp up *) let ramp_up = List.map (fun (a,b) -> Iop (Omove, [b], a)) ramp_up in let (graph,next_pc,ramp_up) = List.fold_right (fun e (g,npc,l) -> - let n = G.V.create (e,npc) in - (G.add_vertex g n, npc+1, n :: l) - ) ramp_up (graph,next_pc,[]) in + let n = G.V.create (e,npc) in + (G.add_vertex g n, npc+1, n :: l) + ) ramp_up (graph,next_pc,[]) in let next_pc = next_pc + 1 in let ramp_down = List.map (fun (a,b) -> Iop (Omove,[b],a)) ramp_down in let (graph,next_pc,ramp_down) = List.fold_right (fun e (g,npc,l) -> - let n = G.V.create (e,npc) in - (G.add_vertex g n, npc+1, n :: l) - ) ramp_down (graph,next_pc,[]) in + let n = G.V.create (e,npc) in + (G.add_vertex g n, npc+1, n :: l) + ) ramp_down (graph,next_pc,[]) in (* let next_pc = next_pc + 1 in *) @@ -494,7 +494,7 @@ let patch_graph graph entry lastone loop bound min ur r1 r2 r3 r4 next_pc prolog let graph = G.add_edge graph n6 entry in graph - + let regs_of_node node = match G.V.label node with | (Inop,n) -> [] @@ -510,45 +510,45 @@ let regs_of_node node = let max_reg_of_graph graph params = Printf.fprintf SPDebug.dc "Calcul du registre de depart.\n"; let regs = G.fold_vertex (fun node regs -> - (regs_of_node node) @ regs - ) graph [] in + (regs_of_node node) @ regs + ) graph [] in let regs = regs @ params in let max_reg = List.fold_right (fun reg max -> - Printf.fprintf SPDebug.dc "%i " (P.to_int reg); - if Int32.compare (P.to_int32 reg) max > 0 - then (P.to_int32 reg) - else max - ) regs Int32.zero in - + Printf.fprintf SPDebug.dc "%i " (P.to_int reg); + if Int32.compare (P.to_int32 reg) max > 0 + then (P.to_int32 reg) + else max + ) regs Int32.zero in + Printf.fprintf SPDebug.dc "MAX REG = %i\n" (Int32.to_int max_reg); BinPos.Pos.succ (P.of_int32 max_reg) - + let get_bound node loop = match G.V.label node with - | (Icond (cond, args),n) -> - let args = to_caml_list args in - begin - match args with - | [] -> failwith "get_bound: condition sans variables" - | r :: [] -> if is_variant r loop then failwith "Pas de borne dans la boucle" else r - | r1 :: r2 :: [] -> - begin - match is_variant r1 loop, is_variant r2 loop with - | true, true -> failwith "Pas de borne dans la boucle " - | false, true -> r1 - | true, false -> r2 - | false, false -> failwith "deux bornes possibles dans la boucle" - end - | _ -> failwith "get_bound: condition avec nombre de variables superieur a 2" - end - | _ -> failwith "get_bound: the node I was given is not a condition\n" + | (Icond (cond, args),n) -> + let args = to_caml_list args in + begin + match args with + | [] -> failwith "get_bound: condition sans variables" + | r :: [] -> if is_variant r loop then failwith "Pas de borne dans la boucle" else r + | r1 :: r2 :: [] -> + begin + match is_variant r1 loop, is_variant r2 loop with + | true, true -> failwith "Pas de borne dans la boucle " + | false, true -> r1 + | true, false -> r2 + | false, false -> failwith "deux bornes possibles dans la boucle" + end + | _ -> failwith "get_bound: condition avec nombre de variables superieur a 2" + end + | _ -> failwith "get_bound: the node I was given is not a condition\n" let get_nextpc graph = (G.fold_vertex (fun node max -> - if (snd (G.V.label node)) > max - then (snd (G.V.label node)) - else max - ) graph 0) + 1 + if (snd (G.V.label node)) > max + then (snd (G.V.label node)) + else max + ) graph 0) + 1 let substitute_pipeline graph loop steady_state prolog epilog min unrolling ru rd params = let n1 = max_reg_of_graph graph params in @@ -562,7 +562,7 @@ let substitute_pipeline graph loop steady_state prolog epilog min unrolling ru r let unrolling = Z.of_sint unrolling in let next_pc = get_nextpc graph in patch_graph graph way_in way_out steady_state bound min unrolling n1 n2 n3 n4 next_pc prolog epilog ru rd - + let get_loops cfg = let domi = dominator_tree cfg in let loops = detect_loops cfg.graph domi in @@ -571,7 +571,7 @@ let get_loops cfg = loops type pipeline = {steady_state : G.V.t list; prolog : G.V.t list; epilog : G.V.t list; - min : int; unrolling : int; ramp_up : (reg * reg) list; ramp_down : (reg * reg) list} + min : int; unrolling : int; ramp_up : (reg * reg) list; ramp_down : (reg * reg) list} let delete_indexes l = List.map (fun e -> fst (G.V.label e) ) l @@ -581,107 +581,107 @@ let fresh = ref BinNums.Coq_xH let distance e = match G.E.label e with - | 1 | 2 | 3 -> 0 - | _ -> 1 + | 1 | 2 | 3 -> 0 + | _ -> 1 type et = IntraRAW | IntraWAW | IntraWAR | InterRAW | InterWAW | InterWAR let edge_type e = match G.E.label e with - | 1 -> IntraRAW - | 2 -> IntraWAR - | 3 -> IntraWAW - | 4 -> InterRAW - | 5 -> InterWAR - | 6 -> InterWAW - | _ -> failwith "Unknown edge type" + | 1 -> IntraRAW + | 2 -> IntraWAR + | 3 -> IntraWAW + | 4 -> InterRAW + | 5 -> InterWAR + | 6 -> InterWAW + | _ -> failwith "Unknown edge type" let latency n = (* A raffiner *) match fst (G.V.label n) with - | Iop (op,args, dst) -> - begin - match op with - | Omove -> 1 - (*| Oaddimm _ -> 1*) - (*| Oadd -> 2*) - | Omul -> 3 - | Odiv -> 30 - | Omulimm _ -> 5 - | _ -> 2 - end - | Iload _ -> 10 -(* | Ialloc _ -> 20*) - | _ -> 1 - + | Iop (op,args, dst) -> + begin + match op with + | Omove -> 1 + (*| Oaddimm _ -> 1*) + (*| Oadd -> 2*) + | Omul -> 3 + | Odiv -> 30 + | Omulimm _ -> 5 + | _ -> 2 + end + | Iload _ -> 10 + (* | Ialloc _ -> 20*) + | _ -> 1 + let reforge_writes inst r = G.V.create ((match fst (G.V.label inst) with - | Inop -> Inop - | Iop (op, args, dst) -> Iop (op, args, r) - | Iload (chunk, mode, args, dst) -> Iload (chunk, mode, args, r) - | Istore (chunk, mode, args, src) -> Istore (chunk, mode, args, src) - | Icall (sign, id, args, dst) -> failwith "reforge_writes: call" - | Itailcall (sign, id, args) -> failwith "reforge_writes: tailcall" -(* | Ialloc (dst, size) -> Ialloc (r, size)*) - | Icond (cond, args) -> Icond (cond, args) - | Ireturn (res) -> failwith "reforge_writes: return") - , snd (G.V.label inst)) + | Inop -> Inop + | Iop (op, args, dst) -> Iop (op, args, r) + | Iload (chunk, mode, args, dst) -> Iload (chunk, mode, args, r) + | Istore (chunk, mode, args, src) -> Istore (chunk, mode, args, src) + | Icall (sign, id, args, dst) -> failwith "reforge_writes: call" + | Itailcall (sign, id, args) -> failwith "reforge_writes: tailcall" + (* | Ialloc (dst, size) -> Ialloc (r, size)*) + | Icond (cond, args) -> Icond (cond, args) + | Ireturn (res) -> failwith "reforge_writes: return") + , snd (G.V.label inst)) let rec reforge_args args oldr newr = match args with - | [] -> [] - | e :: l -> (if e = oldr then newr else e) :: (reforge_args l oldr newr) + | [] -> [] + | e :: l -> (if e = oldr then newr else e) :: (reforge_args l oldr newr) let rec mem_args args r = match args with - | [] -> false - | e :: l -> if e = r then true else mem_args l r + | [] -> false + | e :: l -> if e = r then true else mem_args l r let check_read_exists inst r = match fst (G.V.label inst) with - | Inop -> false - | Iop (op, args, dst) -> mem_args args r - | Iload (chunk, mode, args, dst) -> mem_args args r - | Istore (chunk, mode, args, src) -> src = r || mem_args args r - | Icall (sign, id, args, dst) -> mem_args args r - | Itailcall (sign, id, args) -> false - (*| Ialloc (dst, size) -> false*) - | Icond (cond, args) -> mem_args args r - | Ireturn (res) -> false + | Inop -> false + | Iop (op, args, dst) -> mem_args args r + | Iload (chunk, mode, args, dst) -> mem_args args r + | Istore (chunk, mode, args, src) -> src = r || mem_args args r + | Icall (sign, id, args, dst) -> mem_args args r + | Itailcall (sign, id, args) -> false + (*| Ialloc (dst, size) -> false*) + | Icond (cond, args) -> mem_args args r + | Ireturn (res) -> false let reforge_reads inst oldr newr = assert (check_read_exists inst oldr); G.V.create ((match fst (G.V.label inst) with - | Inop -> Inop - | Iop (op, args, dst) -> Iop (op, reforge_args args oldr newr, dst) - | Iload (chunk, mode, args, dst) -> Iload (chunk, mode, reforge_args args oldr newr, dst) - | Istore (chunk, mode, args, src) -> Istore (chunk, mode, reforge_args args oldr newr , if src = oldr then newr else src) - | Icall (sign, id, args, dst) -> failwith "reforge_reads: call" - | Itailcall (sign, id, args) -> failwith "reforge_reads: tailcall" - (*| Ialloc (dst, size) -> Ialloc (dst, size)*) - | Icond (cond, args) -> Icond (cond, reforge_args args oldr newr) - | Ireturn (res) -> failwith "reforge_reads: return") - , snd (G.V.label inst)) + | Inop -> Inop + | Iop (op, args, dst) -> Iop (op, reforge_args args oldr newr, dst) + | Iload (chunk, mode, args, dst) -> Iload (chunk, mode, reforge_args args oldr newr, dst) + | Istore (chunk, mode, args, src) -> Istore (chunk, mode, reforge_args args oldr newr , if src = oldr then newr else src) + | Icall (sign, id, args, dst) -> failwith "reforge_reads: call" + | Itailcall (sign, id, args) -> failwith "reforge_reads: tailcall" + (*| Ialloc (dst, size) -> Ialloc (dst, size)*) + | Icond (cond, args) -> Icond (cond, reforge_args args oldr newr) + | Ireturn (res) -> failwith "reforge_reads: return") + , snd (G.V.label inst)) let get_succs_raw ddg node = let succs = G.succ_e ddg node in let succs = List.filter (fun succ -> - match G.E.label succ with - | 1 | 4 -> true - | _ -> false - ) succs in + match G.E.label succ with + | 1 | 4 -> true + | _ -> false + ) succs in List.map (fun e -> G.E.dst e) succs let written inst = match fst (G.V.label inst) with - | Inop -> None - | Iop (op, args, dst) -> Some dst - | Iload (chunk, mode, args, dst) -> Some dst - | Istore (chunk, mode, args, src) -> None - | Icall (sign, id, args, dst) -> failwith "written: call" - | Itailcall (sign, id, args) -> failwith "written: tailcall" - (*| Ialloc (dst, size) -> Some dst*) - | Icond (cond, args) -> None - | Ireturn (res) -> failwith "written: return" + | Inop -> None + | Iop (op, args, dst) -> Some dst + | Iload (chunk, mode, args, dst) -> Some dst + | Istore (chunk, mode, args, src) -> None + | Icall (sign, id, args, dst) -> failwith "written: call" + | Itailcall (sign, id, args) -> failwith "written: tailcall" + (*| Ialloc (dst, size) -> Some dst*) + | Icond (cond, args) -> None + | Ireturn (res) -> failwith "written: return" let fresh_regs n = let t = Array.make n (BinNums.Coq_xH) in @@ -690,27 +690,27 @@ let fresh_regs n = fresh := BinPos.Pos.succ !fresh done; t - + let print_reg r = Printf.fprintf SPDebug.dc "%i " (P.to_int r) let is_cond node = match fst (G.V.label node) with - | Icond _ -> true - | _ -> false - - + | Icond _ -> true + | _ -> false + + (*******************************************) - + let watch_regs l = List.fold_right (fun (a,b) l -> - if List.mem a l then l else a :: l - ) l [] + if List.mem a l then l else a :: l + ) l [] let make_moves = List.map (fun (a,b) -> Iop (Omove,[b],a)) let rec repeat l n = match n with - | 0 -> [] - | n -> l @ repeat l (n-1) + | 0 -> [] + | n -> l @ repeat l (n-1) let fv = ref 0 @@ -722,98 +722,98 @@ let apply_pipeliner f p ?(debug=false) = let loops = get_loops cfg in Printf.fprintf SPDebug.dc "Loops: %d\n" (List.length loops); let ddgs = List.map (fun (qqch,loop) -> (loop,build_inter_dependency_graph loop)) loops in - + let lv = ref 0 in let graph = List.fold_right (fun (loop,ddg) graph -> - Printf.fprintf SPDebug.dc "__________________ NEW LOOP ____________________\n"; - Printf.printf "Pipelinable loop: "; - incr lv; - fresh := (BinPos.Pos.succ - (BinPos.Pos.succ - (BinPos.Pos.succ - (BinPos.Pos.succ - (BinPos.Pos.succ - (max_reg_of_graph graph (to_caml_list f.fn_params) - )))))); - Printf.fprintf SPDebug.dc "FRESH = %i \n" - (P.to_int !fresh); - match p ddg with - | Some pipe -> - Printf.printf "Rock On ! Min = %i - Unroll = %i\n" pipe.min pipe.unrolling; - let p = (make_moves pipe.ramp_up) @ (delete_indexes pipe.prolog) in - let e = (delete_indexes pipe.epilog) @ (make_moves pipe.ramp_down) in - let b = delete_indexes (List.tl (List.rev loop)) in - let bt = (List.tl (delete_indexes pipe.steady_state)) in - let cond1 = fst (G.V.label (List.hd (List.rev loop))) in - let cond2 = (List.hd (delete_indexes pipe.steady_state)) in - - let bu = symbolic_evaluation (repeat b (pipe.min + 1)) in - let pe = symbolic_evaluation (p @ e) in - let bte = symbolic_evaluation (bt @ e) in - let ebu = symbolic_evaluation (e @ repeat b pipe.unrolling) in - let regs = watch_regs pipe.ramp_down in - let c1 = symbolic_condition cond1 (repeat b pipe.unrolling) in - let d1 = symbolic_condition cond1 (repeat b (pipe.min + 1)) in - (*let c2 = symbolic_condition cond2 p in - let d2 = symbolic_condition cond2 ((make_moves pipe.ramp_up) @ bt) in*) - - - - let sbt = symbolic_evaluation (bt) in - let sep = symbolic_evaluation (e @ repeat b (pipe.unrolling - (pipe.min + 1)) @ p) in (* er @ pr *) - - Printf.printf "Initialisation : %s \n" - (if symbolic_equivalence bu pe regs then "OK" else "FAIL"); - Printf.printf "Etat stable : %s \n" - (if symbolic_equivalence bte ebu regs then "OK" else "FAIL"); - Printf.printf "Egalite fondamentale : %s \n" - (if symbolic_equivalence sbt sep (watch_regs pipe.ramp_up) then "OK" else "FAIL"); - (* Printf.printf "Condition initiale : %s \n" - (if c1 = c2 then "OK" else "FAIL"); - Printf.printf "Condition stable : %s \n" - (if d1 = d2 then "OK" else "FAIL"); - - - Printf.fprintf SPDebug.dc "pbte\n";*) - List.iter (fun e -> - Printf.fprintf SPDebug.dc "%s\n" - (string_of_node (G.V.create (e,0))) - ) (p @ bt @ e); - Printf.fprintf SPDebug.dc "bu\n"; - List.iter (fun e -> Printf.fprintf SPDebug.dc "%s\n" - (string_of_node (G.V.create (e,0))) - ) (repeat b (pipe.unrolling + pipe.min)); - - - - if debug then - display_st ("pbte"^ (string_of_int !fv) ^ (string_of_int !lv)) (p @ bt @ e) (watch_regs pipe.ramp_down); - if debug then - display_st ("bu"^ (string_of_int !fv) ^ (string_of_int !lv)) (repeat b (pipe.min + pipe.unrolling)) (watch_regs pipe.ramp_down); - - if debug then display_st ("bt"^ (string_of_int !fv) ^ (string_of_int !lv)) (bt) (watch_regs pipe.ramp_up); - if debug then display_st ("ep"^ (string_of_int !fv) ^ (string_of_int !lv)) (e @ repeat b (pipe.unrolling - (pipe.min + 1)) @ p) (watch_regs pipe.ramp_up); - - substitute_pipeline graph loop - (delete_indexes pipe.steady_state) (delete_indexes pipe.prolog) - (delete_indexes pipe.epilog) (pipe.min + pipe.unrolling) - pipe.unrolling pipe.ramp_up - pipe.ramp_down - (to_caml_list f.fn_params) - | None -> Printf.printf "Damn It ! \n"; graph - ) ddgs cfg.graph in + Printf.fprintf SPDebug.dc "__________________ NEW LOOP ____________________\n"; + Printf.printf "Pipelinable loop: "; + incr lv; + fresh := (BinPos.Pos.succ + (BinPos.Pos.succ + (BinPos.Pos.succ + (BinPos.Pos.succ + (BinPos.Pos.succ + (max_reg_of_graph graph (to_caml_list f.fn_params) + )))))); + Printf.fprintf SPDebug.dc "FRESH = %i \n" + (P.to_int !fresh); + match p ddg with + | Some pipe -> + Printf.printf "Rock On ! Min = %i - Unroll = %i\n" pipe.min pipe.unrolling; + let p = (make_moves pipe.ramp_up) @ (delete_indexes pipe.prolog) in + let e = (delete_indexes pipe.epilog) @ (make_moves pipe.ramp_down) in + let b = delete_indexes (List.tl (List.rev loop)) in + let bt = (List.tl (delete_indexes pipe.steady_state)) in + let cond1 = fst (G.V.label (List.hd (List.rev loop))) in + let cond2 = (List.hd (delete_indexes pipe.steady_state)) in + + let bu = symbolic_evaluation (repeat b (pipe.min + 1)) in + let pe = symbolic_evaluation (p @ e) in + let bte = symbolic_evaluation (bt @ e) in + let ebu = symbolic_evaluation (e @ repeat b pipe.unrolling) in + let regs = watch_regs pipe.ramp_down in + let c1 = symbolic_condition cond1 (repeat b pipe.unrolling) in + let d1 = symbolic_condition cond1 (repeat b (pipe.min + 1)) in + (*let c2 = symbolic_condition cond2 p in + let d2 = symbolic_condition cond2 ((make_moves pipe.ramp_up) @ bt) in*) + + + + let sbt = symbolic_evaluation (bt) in + let sep = symbolic_evaluation (e @ repeat b (pipe.unrolling - (pipe.min + 1)) @ p) in (* er @ pr *) + + Printf.printf "Initialisation : %s \n" + (if symbolic_equivalence bu pe regs then "OK" else "FAIL"); + Printf.printf "Etat stable : %s \n" + (if symbolic_equivalence bte ebu regs then "OK" else "FAIL"); + Printf.printf "Egalite fondamentale : %s \n" + (if symbolic_equivalence sbt sep (watch_regs pipe.ramp_up) then "OK" else "FAIL"); + (* Printf.printf "Condition initiale : %s \n" + (if c1 = c2 then "OK" else "FAIL"); + Printf.printf "Condition stable : %s \n" + (if d1 = d2 then "OK" else "FAIL"); + + + Printf.fprintf SPDebug.dc "pbte\n";*) + List.iter (fun e -> + Printf.fprintf SPDebug.dc "%s\n" + (string_of_node (G.V.create (e,0))) + ) (p @ bt @ e); + Printf.fprintf SPDebug.dc "bu\n"; + List.iter (fun e -> Printf.fprintf SPDebug.dc "%s\n" + (string_of_node (G.V.create (e,0))) + ) (repeat b (pipe.unrolling + pipe.min)); + + + + if debug then + display_st ("pbte"^ (string_of_int !fv) ^ (string_of_int !lv)) (p @ bt @ e) (watch_regs pipe.ramp_down); + if debug then + display_st ("bu"^ (string_of_int !fv) ^ (string_of_int !lv)) (repeat b (pipe.min + pipe.unrolling)) (watch_regs pipe.ramp_down); + + if debug then display_st ("bt"^ (string_of_int !fv) ^ (string_of_int !lv)) (bt) (watch_regs pipe.ramp_up); + if debug then display_st ("ep"^ (string_of_int !fv) ^ (string_of_int !lv)) (e @ repeat b (pipe.unrolling - (pipe.min + 1)) @ p) (watch_regs pipe.ramp_up); + + substitute_pipeline graph loop + (delete_indexes pipe.steady_state) (delete_indexes pipe.prolog) + (delete_indexes pipe.epilog) (pipe.min + pipe.unrolling) + pipe.unrolling pipe.ramp_up + pipe.ramp_down + (to_caml_list f.fn_params) + | None -> Printf.printf "Damn It ! \n"; graph + ) ddgs cfg.graph in if debug then display graph ("output"^ (string_of_int !fv)); let tg = convert_back graph in let tg_to_type = {fn_sig = f.fn_sig; - fn_params = f.fn_params; - fn_stacksize = f.fn_stacksize; - fn_code = tg; - fn_entrypoint = f.fn_entrypoint; - (*fn_nextpc = P.of_int ((get_nextpc (graph)))*) - } in + fn_params = f.fn_params; + fn_stacksize = f.fn_stacksize; + fn_code = tg; + fn_entrypoint = f.fn_entrypoint; + (*fn_nextpc = P.of_int ((get_nextpc (graph)))*) + } in (*SPTyping.type_function tg_to_type;*) tg_to_type diff --git a/src/SoftwarePipelining/SPIMS.ml b/src/SoftwarePipelining/SPIMS.ml index 48e7339..1933268 100644 --- a/src/SoftwarePipelining/SPIMS.ml +++ b/src/SoftwarePipelining/SPIMS.ml @@ -18,80 +18,80 @@ module NI = Map.Make (struct type t = G.V.t let compare = compare end) let find key map def = try NI.find key map with - | Not_found -> def + | Not_found -> def let unpack v = match v with - | Some v -> v - | None -> failwith "unpack abusif" - + | Some v -> v + | None -> failwith "unpack abusif" + let dep_latency edge = match edge_type edge with - | IntraRAW | InterRAW -> latency (G.E.src edge) - | _ -> 1 + | IntraRAW | InterRAW -> latency (G.E.src edge) + | _ -> 1 let estart ddg schedule node ii = let preds = G.pred_e ddg node in let starts = List.map (fun edge -> - match find (G.E.src edge) schedule None with - | Some t -> - let start = t + dep_latency edge - ii * distance edge in - (*Printf.printf "start : %i \n" start;*) - if start < 0 then 0 else start - | None -> 0 - ) preds in + match find (G.E.src edge) schedule None with + | Some t -> + let start = t + dep_latency edge - ii * distance edge in + (*Printf.printf "start : %i \n" start;*) + if start < 0 then 0 else start + | None -> 0 + ) preds in List.fold_left (fun max e -> if max > e then max else e) 0 starts - + let resource_conflict time mrt ii = match Array.get mrt (time mod ii) with - | None -> false - | Some v -> true - + | None -> false + | Some v -> true + let rec scan_time time maxtime mrt ii = - if time <= maxtime - then - begin - if resource_conflict time mrt ii - then scan_time (time + 1) maxtime mrt ii - else Some time - end - else None - + if time <= maxtime + then + begin + if resource_conflict time mrt ii + then scan_time (time + 1) maxtime mrt ii + else Some time + end + else None + let finished ddg schedule = let unscheduled = G.fold_vertex (fun node l -> - match find node schedule None with - | Some v -> l - | None -> node :: l - ) ddg [] in + match find node schedule None with + | Some v -> l + | None -> node :: l + ) ddg [] in (* Printf.printf "R %i R \n" (List.length unscheduled); *) if List.length unscheduled = 0 then true else false let bad_successors ddg schedule node ii = let succs = G.succ_e ddg node in (* Le succs_ddg initial *) -(* let reftime = NI.find node schedule in *) -(* let succs_sched = NI.fold (fun node time succs -> *) -(* if time > reftime then node :: succs else succs *) -(* ) schedule [] in *) -(* let succs = List.filter (fun edge -> List.mem (G.E.dst edge) succs_sched) succs_ddg in*) + (* let reftime = NI.find node schedule in *) + (* let succs_sched = NI.fold (fun node time succs -> *) + (* if time > reftime then node :: succs else succs *) + (* ) schedule [] in *) + (* let succs = List.filter (fun edge -> List.mem (G.E.dst edge) succs_sched) succs_ddg in*) List.fold_right (fun edge bad -> - match find (G.E.dst edge) schedule None with - | Some t -> - if unpack (NI.find node schedule) + dep_latency edge - ii * distance edge > t - then (G.E.dst edge) :: bad - else bad - | None -> bad - ) succs [] - + match find (G.E.dst edge) schedule None with + | Some t -> + if unpack (NI.find node schedule) + dep_latency edge - ii * distance edge > t + then (G.E.dst edge) :: bad + else bad + | None -> bad + ) succs [] + let get_condition ddg = let cond = G.fold_vertex (fun node cond -> - if is_cond node then Some node else cond - ) ddg None in + if is_cond node then Some node else cond + ) ddg None in match cond with - | Some cond -> cond - | None -> failwith "The loop does not contain a condition. Aborting\n" + | Some cond -> cond + | None -> failwith "The loop does not contain a condition. Aborting\n" let modulo_schedule heightr ddg min_ii max_interval = - + let ii = ref (min_ii - 1) in let notfound = ref true in let sched = ref NI.empty in @@ -115,50 +115,50 @@ let modulo_schedule heightr ddg min_ii max_interval = (* Printf.printf "tmin (%s) = %i \n" (string_of_node h) mintime; *) let maxtime = mintime + !ii -1 in let time = - match scan_time mintime maxtime mrt !ii with - | Some t -> t - | None -> (*Printf.printf "backtrack" ; *) - if mintime = 0 then 1 + find h !lasttime 0 - else max mintime (1 + find h !lasttime 0) + match scan_time mintime maxtime mrt !ii with + | Some t -> t + | None -> (*Printf.printf "backtrack" ; *) + if mintime = 0 then 1 + find h !lasttime 0 + else max mintime (1 + find h !lasttime 0) in (* Printf.printf "Chosen time for %s : %i \n" (string_of_node h) time; *) schedtime := NI.add h (Some time) !schedtime; lasttime := NI.add h time !lasttime; - + let killed = bad_successors ddg !schedtime h !ii in List.iter (fun n -> (* Printf.printf "Killing %s" (string_of_node n) ; *)schedtime := NI.add n None !schedtime) killed; - + begin - match Array.get mrt (time mod !ii) with - | None -> Array.set mrt (time mod !ii) (Some h) - | Some n -> - begin - (*Printf.printf "Deleting : %s \n" (string_of_node n); *) - (* Printf.printf "."; *) - schedtime := NI.add n None !schedtime; - Array.set mrt (time mod !ii) (Some h) - end + match Array.get mrt (time mod !ii) with + | None -> Array.set mrt (time mod !ii) (Some h) + | Some n -> + begin + (*Printf.printf "Deleting : %s \n" (string_of_node n); *) + (* Printf.printf "."; *) + schedtime := NI.add n None !schedtime; + Array.set mrt (time mod !ii) (Some h) + end end; (* if finished ddg !schedtime then Printf.printf "Fini ! \n" *) - + done; - + let success = G.fold_vertex (fun node b -> - b && - match find node !schedtime None with - | Some _ -> true - | None -> false - ) ddg true in - + b && + match find node !schedtime None with + | Some _ -> true + | None -> false + ) ddg true in + if success then (notfound := false; sched := !schedtime); - + done; - + if (not !notfound) then (!sched,!ii) else failwith "IMS failure" - - + + let res_m_ii ddg = G.nb_vertex ddg @@ -166,13 +166,12 @@ let pipeliner ddg heightr = let mii = res_m_ii ddg in let (schedule,ii) = modulo_schedule heightr ddg mii (10 * mii) in (NI.fold (fun n v map -> - match v with - | Some v -> NI.add n v map - | None -> failwith "pipeliner: schedule unfinished" - ) schedule NI.empty,ii) + match v with + | Some v -> NI.add n v map + | None -> failwith "pipeliner: schedule unfinished" + ) schedule NI.empty,ii) let print_schedule sched = NI.iter (fun node time -> - Printf.fprintf SPDebug.dc "%s |---> %i \n" (string_of_node node) time - ) sched - + Printf.fprintf SPDebug.dc "%s |---> %i \n" (string_of_node node) time + ) sched diff --git a/src/SoftwarePipelining/SPMVE.ml b/src/SoftwarePipelining/SPMVE.ml index 2eb4929..28381c1 100644 --- a/src/SoftwarePipelining/SPMVE.ml +++ b/src/SoftwarePipelining/SPMVE.ml @@ -14,7 +14,7 @@ open SPBasic open SPIMS module Mult = Map.Make (struct type t = reg let compare = compare end) - + let size_of_map1 m = NI.fold (fun key v size -> size + 1) m 0 @@ -23,36 +23,36 @@ let size_of_map2 m = let sched_max_time sched = NI.fold (fun node time max -> - if time > max then time else max - ) sched 0 + if time > max then time else max + ) sched 0 let print_table t s = Printf.fprintf SPDebug.dc "%s : \n" s; let string_of_node_ev node = match node with - | Some node -> string_of_node node - | None -> "_" + | Some node -> string_of_node node + | None -> "_" in Array.iteri (fun i node -> Printf.fprintf SPDebug.dc "%i :: %s \n" i (string_of_node_ev node)) t let durations ddg sched ii = - + G.fold_vertex (fun node mult -> - match written node with - | None -> mult - | Some r -> - let raw_succs = get_succs_raw ddg node in - let durations = List.map (fun succ -> - let d = NI.find succ sched - NI.find node sched in - if d >= 0 then d - else ((sched_max_time sched - NI.find node sched) + NI.find succ sched) - ) raw_succs in - let duration = List.fold_left (fun max e -> if max > e then max else e) 0 durations in - Mult.add r ((duration / ii) + 1) mult (* cette division est surement fdausse*) - ) ddg Mult.empty + match written node with + | None -> mult + | Some r -> + let raw_succs = get_succs_raw ddg node in + let durations = List.map (fun succ -> + let d = NI.find succ sched - NI.find node sched in + if d >= 0 then d + else ((sched_max_time sched - NI.find node sched) + NI.find succ sched) + ) raw_succs in + let duration = List.fold_left (fun max e -> if max > e then max else e) 0 durations in + Mult.add r ((duration / ii) + 1) mult (* cette division est surement fdausse*) + ) ddg Mult.empty let minimizer qi ur = - + let rec fill n = if n <= ur then n :: fill (n + 1) else [] in @@ -62,22 +62,22 @@ let minimizer qi ur = let l = List.filter (fun e -> snd e = 0) l in let l = List.map fst l in List.fold_left (fun min e -> if min < e then min else e) ur l - + let multiplicity ddg sched ii = let qs = durations ddg sched ii in -(* Printf.printf "Quantite de variables necessaires : \n"; *) -(* Mult.iter (fun key mu -> print_reg key ; Printf.printf " |-> %i\n" mu) qs; *) + (* Printf.printf "Quantite de variables necessaires : \n"; *) + (* Mult.iter (fun key mu -> print_reg key ; Printf.printf " |-> %i\n" mu) qs; *) let unroll = Mult.fold (fun reg mult max -> - if mult > max then mult else max - ) qs 0 in + if mult > max then mult else max + ) qs 0 in let mult = Mult.fold (fun reg mult mult -> - Mult.add reg (minimizer (Mult.find reg qs) unroll) mult - ) qs Mult.empty + Mult.add reg (minimizer (Mult.find reg qs) unroll) mult + ) qs Mult.empty in (mult,unroll) - + let mve_kernel t ddg sched ii mult unroll = - + let regs = Array.make ii (fresh_regs 0) in for i = 0 to (ii - 1) do let fregs = fresh_regs unroll in @@ -89,103 +89,103 @@ let mve_kernel t ddg sched ii mult unroll = let used_regs = ref [] in let index r i = Mult.find r mult - ( ((i / ii) + 1) mod Mult.find r mult) in -(* let pos i node inst = *) -(* let separation = *) -(* let b= NI.find node sched - NI.find inst sched in *) -(* if b >= 0 then b *) -(* else ((sched_max_time sched - NI.find inst sched) + NI.find node sched) *) -(* in *) -(* (i + separation) mod (ii * unroll) in *) + (* let pos i node inst = *) + (* let separation = *) + (* let b= NI.find node sched - NI.find inst sched in *) + (* if b >= 0 then b *) + (* else ((sched_max_time sched - NI.find inst sched) + NI.find node sched) *) + (* in *) + (* (i + separation) mod (ii * unroll) in *) let new_t = Array.copy t in for i = 0 to (Array.length t - 1) do (* print_table new_t "Nouvelle table"; *) match t.(i),new_t.(i) with - | Some insti, Some insti_mod -> - begin - match written insti with - | None -> () - | Some r -> - begin - let new_reg = - if Mult.find r mult = 0 then r - else regs.(i mod ii).(index r i - 1) in - if (not (List.mem (r,new_reg) !used_regs)) then used_regs := (r,new_reg) :: !used_regs; - let inst = reforge_writes insti_mod new_reg in - Printf.fprintf SPDebug.dc "Reecriture : %s --> %s \n" (string_of_node insti) (string_of_node inst); - Array.set new_t i (Some inst); - let succs = get_succs_raw ddg insti in - List.iter (fun node -> - - (* let lifetime = *) -(* let d = NI.find node sched - NI.find insti sched in *) -(* if d >= 0 then d *) -(* else ((sched_max_time sched - NI.find insti sched) + 1 + NI.find node sched) *) -(* in *) - - - (* ___Version 1___ *) - (* let lifetime = lifetime / ii in *) -(* let schedtime = *) -(* ((NI.find node sched) mod ii) (\* Position dans le premier bloc *\) *) -(* + (ii * (i / ii)) (\* Commencement du bloc ou on travail *\) *) -(* + (ii * lifetime ) (\* Decalage (Mult.find r mult - 1) *\) *) -(* + ((if (NI.find node sched mod ii) < (NI.find insti sched mod ii) then 0 else 0) * ii) *) -(* in *) - - (* Printf.printf "seed = %i - bloc = %i - slide = %i - corr = %i - id = %i \n" *) -(* ((NI.find node sched) mod ii) *) -(* (ii * (i / ii)) (ii * lifetime) *) -(* ((if (NI.find node sched mod ii) < (NI.find insti sched mod ii) then 1 else 0 ) * ii) *) -(* id; *) -(* Printf.printf "Successeur a traiter : %s ooo %i ooo\n" (string_of_node node) (Mult.find r mult); *) - - (* ___Version 2___ *) - let schedtime = - if (NI.find node sched > NI.find insti sched) - then i + (NI.find node sched - NI.find insti sched) - else i - NI.find insti sched + ii + NI.find node sched - (* let delta = NI.find insti sched - NI.find node sched in *) -(* (i - delta) + (((delta / ii) + 1) * ii) (\* (i - delta) + ii*\) *) - in - - (* then *) - - Printf.fprintf SPDebug.dc "i = %i - def = %i - use = %i - time = %i \n" - i (NI.find insti sched) (NI.find node sched) schedtime; - - - (* let id = pos i node insti in *) - let id = schedtime mod (unroll * ii) (* le tout modulo la tabl *) in - let id = (id + (unroll * ii)) mod (unroll * ii) in - Printf.fprintf SPDebug.dc "Positions to treat : %i \n" id; - let insttt = match new_t.(id) with - | Some inst -> inst - | None -> failwith "There should be an instruction" - in - let inst = reforge_reads insttt r new_reg in - Array.set new_t id (Some inst) - ) succs - end - end - | None, _ -> () - | _, None -> failwith "MVE : qqch mal compris" + | Some insti, Some insti_mod -> + begin + match written insti with + | None -> () + | Some r -> + begin + let new_reg = + if Mult.find r mult = 0 then r + else regs.(i mod ii).(index r i - 1) in + if (not (List.mem (r,new_reg) !used_regs)) then used_regs := (r,new_reg) :: !used_regs; + let inst = reforge_writes insti_mod new_reg in + Printf.fprintf SPDebug.dc "Reecriture : %s --> %s \n" (string_of_node insti) (string_of_node inst); + Array.set new_t i (Some inst); + let succs = get_succs_raw ddg insti in + List.iter (fun node -> + + (* let lifetime = *) + (* let d = NI.find node sched - NI.find insti sched in *) + (* if d >= 0 then d *) + (* else ((sched_max_time sched - NI.find insti sched) + 1 + NI.find node sched) *) + (* in *) + + + (* ___Version 1___ *) + (* let lifetime = lifetime / ii in *) + (* let schedtime = *) + (* ((NI.find node sched) mod ii) (\* Position dans le premier bloc *\) *) + (* + (ii * (i / ii)) (\* Commencement du bloc ou on travail *\) *) + (* + (ii * lifetime ) (\* Decalage (Mult.find r mult - 1) *\) *) + (* + ((if (NI.find node sched mod ii) < (NI.find insti sched mod ii) then 0 else 0) * ii) *) + (* in *) + + (* Printf.printf "seed = %i - bloc = %i - slide = %i - corr = %i - id = %i \n" *) + (* ((NI.find node sched) mod ii) *) + (* (ii * (i / ii)) (ii * lifetime) *) + (* ((if (NI.find node sched mod ii) < (NI.find insti sched mod ii) then 1 else 0 ) * ii) *) + (* id; *) + (* Printf.printf "Successeur a traiter : %s ooo %i ooo\n" (string_of_node node) (Mult.find r mult); *) + + (* ___Version 2___ *) + let schedtime = + if (NI.find node sched > NI.find insti sched) + then i + (NI.find node sched - NI.find insti sched) + else i - NI.find insti sched + ii + NI.find node sched + (* let delta = NI.find insti sched - NI.find node sched in *) + (* (i - delta) + (((delta / ii) + 1) * ii) (\* (i - delta) + ii*\) *) + in + + (* then *) + + Printf.fprintf SPDebug.dc "i = %i - def = %i - use = %i - time = %i \n" + i (NI.find insti sched) (NI.find node sched) schedtime; + + + (* let id = pos i node insti in *) + let id = schedtime mod (unroll * ii) (* le tout modulo la tabl *) in + let id = (id + (unroll * ii)) mod (unroll * ii) in + Printf.fprintf SPDebug.dc "Positions to treat : %i \n" id; + let insttt = match new_t.(id) with + | Some inst -> inst + | None -> failwith "There should be an instruction" + in + let inst = reforge_reads insttt r new_reg in + Array.set new_t id (Some inst) + ) succs + end + end + | None, _ -> () + | _, None -> failwith "MVE : qqch mal compris" done; new_t,!used_regs let crunch_and_unroll sched ii ur = let steady_s = Array.make ii None in NI.iter (fun inst time -> - Array.set steady_s (time mod ii) (Some inst) - ) sched; + Array.set steady_s (time mod ii) (Some inst) + ) sched; (* Printf.printf "Etat stable : \n"; *) -(* let string_of_node_ev node = *) -(* match node with *) -(* | Some node -> string_of_node node *) -(* | None -> "_" *) -(* in *) -(* Array.iteri (fun i node -> Printf.printf "%i :: %s \n" i (string_of_node_ev node)) steady_s; *) + (* let string_of_node_ev node = *) + (* match node with *) + (* | Some node -> string_of_node node *) + (* | None -> "_" *) + (* in *) + (* Array.iteri (fun i node -> Printf.printf "%i :: %s \n" i (string_of_node_ev node)) steady_s; *) let steady = Array.make (ii * ur) None in for i = 0 to (ur - 1) do for time = 0 to (ii - 1) do @@ -197,27 +197,27 @@ let crunch_and_unroll sched ii ur = let compute_iteration_table sched ii = let t = Array.make ii None in NI.iter (fun node time -> - Array.set t (NI.find node sched mod ii) (Some ((NI.find node sched / ii) + 1)) - ) sched; + Array.set t (NI.find node sched mod ii) (Some ((NI.find node sched / ii) + 1)) + ) sched; t let compute_prolog steady min ii unroll schedule it = - + let prolog = ref [] in let prolog_piece = ref [] in for i = (min - 1) downto 0 do - + let index = ((ii * (unroll - (min - i)))) mod (unroll * ii) in prolog_piece := []; for j = 0 to (ii - 1) do (* copie du sous tableau *) (* Printf.printf "i : %i - j : %i - index : %i \n" i j index; *) match steady.(index + j), it.(j) with - | Some inst , Some iter -> - if iter <= (i + 1) then prolog_piece := inst :: !prolog_piece; (* i + 1 au lieu de i *) - | None, _ -> () - | _, _ -> failwith "compute_prolog: quelquechose est mal compris" + | Some inst , Some iter -> + if iter <= (i + 1) then prolog_piece := inst :: !prolog_piece; (* i + 1 au lieu de i *) + | None, _ -> () + | _, _ -> failwith "compute_prolog: quelquechose est mal compris" done; prolog := List.rev (!prolog_piece) @ !prolog @@ -227,41 +227,41 @@ let compute_prolog steady min ii unroll schedule it = let compute_epilog steady min ii unroll schedule it = - + let epilog = ref [] in for i = 0 to (min - 1) do let index = (i mod unroll) * ii in for j = 0 to (ii - 1) do match steady.(index + j), it.(j) with - | Some inst , Some iter -> - if iter > (i + 1) then epilog := inst :: !epilog; - | None, _ -> () - | _, _ -> failwith "compute_prolog: quelquechose est mal compris" + | Some inst , Some iter -> + if iter > (i + 1) then epilog := inst :: !epilog; + | None, _ -> () + | _, _ -> failwith "compute_prolog: quelquechose est mal compris" done; done; List.rev (!epilog) - + let entrance = List.map (fun (a,b) -> (b,a)) let way_out prolog epilog used_regs = let l = List.rev (prolog @ epilog) in - + let rec way_out_rec l wo = match l with - | [] -> wo - | i :: l -> - begin - match written i with - | Some r -> - let mov = List.find (fun (a,b) -> r = b) used_regs in - if List.mem mov wo - then way_out_rec l wo - else way_out_rec l (mov :: wo) - | None -> way_out_rec l wo - end + | [] -> wo + | i :: l -> + begin + match written i with + | Some r -> + let mov = List.find (fun (a,b) -> r = b) used_regs in + if List.mem mov wo + then way_out_rec l wo + else way_out_rec l (mov :: wo) + | None -> way_out_rec l wo + end in - + way_out_rec l [] let mve ddg sched ii = @@ -282,11 +282,11 @@ let mve ddg sched ii = let iteration_table = compute_iteration_table sched ii in Printf.fprintf SPDebug.dc "Table d'iteration \n"; Array.iteri (fun i elt -> - match elt with - | Some elt -> - Printf.fprintf SPDebug.dc "%i : %i\n" i elt - | None -> Printf.fprintf SPDebug.dc "%i : _ \n" i - ) iteration_table; + match elt with + | Some elt -> + Printf.fprintf SPDebug.dc "%i : %i\n" i elt + | None -> Printf.fprintf SPDebug.dc "%i : _ \n" i + ) iteration_table; let prolog = compute_prolog steady_state min ii unroll sched iteration_table in let prolog = List.filter (fun e -> not (is_cond e)) prolog in let epilog = compute_epilog steady_state min ii unroll sched iteration_table in @@ -297,6 +297,3 @@ let mve ddg sched ii = List.iter (fun node -> Printf.fprintf SPDebug.dc "%s \n" (string_of_node node)) epilog; let way_out = way_out prolog epilog used_regs in (steady_state,prolog,epilog,min - 1,unroll,entrance used_regs, way_out) - - - diff --git a/src/SoftwarePipelining/SPSymbolic_evaluation.ml b/src/SoftwarePipelining/SPSymbolic_evaluation.ml index 450cda7..c99afc8 100644 --- a/src/SoftwarePipelining/SPSymbolic_evaluation.ml +++ b/src/SoftwarePipelining/SPSymbolic_evaluation.ml @@ -20,7 +20,7 @@ type symbolic_value = | Sreg of reg | Sop of operation * symbolic_value list | Sload of memory_chunk * addressing * symbolic_value list * symbolic_mem - + and symbolic_mem = | Smem | Sstore of memory_chunk * addressing * symbolic_value list * symbolic_value * symbolic_mem @@ -36,34 +36,34 @@ let initial_mem = Smem let initial_cons = Cons.empty exception Not_straight - + let find res st = try State.find res st with - | Not_found -> Sreg res + | Not_found -> Sreg res let rec get_args st = function | [] -> [] | arg::args -> find arg st :: get_args st args - + let rec symbolic_evaluation st sm cs = function | [] -> (st,sm,cs) | Inop :: l -> symbolic_evaluation st sm cs l | Iop (Omove, [src], dst) :: l -> - symbolic_evaluation (State.add dst (find src st) st) sm cs l + symbolic_evaluation (State.add dst (find src st) st) sm cs l | Iop (op, args, dst) :: l -> - let sym_val = Sop (op,get_args st args) in - symbolic_evaluation (State.add dst sym_val st) sm (Cons.add sym_val cs) l + let sym_val = Sop (op,get_args st args) in + symbolic_evaluation (State.add dst sym_val st) sm (Cons.add sym_val cs) l | Iload (chunk, mode, args, dst) :: l -> - let sym_val = Sload (chunk, mode, get_args st args, sm) in - symbolic_evaluation (State.add dst sym_val st) sm (Cons.add sym_val cs) l + let sym_val = Sload (chunk, mode, get_args st args, sm) in + symbolic_evaluation (State.add dst sym_val st) sm (Cons.add sym_val cs) l | Istore (chunk, mode, args, src) :: l -> - let sym_mem = Sstore (chunk, mode, get_args st args, find src st, sm) in - symbolic_evaluation st sym_mem cs l + let sym_mem = Sstore (chunk, mode, get_args st args, find src st, sm) in + symbolic_evaluation st sym_mem cs l | _ :: l -> raise Not_straight @@ -83,7 +83,7 @@ let string_of_osv = function type ident = int module S = Graph.Persistent.Digraph.Abstract - (struct type t = osv * ident end) + (struct type t = osv * ident end) let name_of_vertex v = let (osv,id) = S.V.label v in @@ -118,76 +118,76 @@ let counter = ref 0 let rec convert_sv_rec sv graph = incr counter; match sv with - | Sreg res -> - let node = S.V.create (Oresource (Reg res), !counter) in - let graph = S.add_vertex graph node in - (graph,node) - - | Sop (op, svl) -> - let node = S.V.create (Oop op, !counter) in - let (graph, node_l) = List.fold_right (fun sv (graph,node_l) -> - let (graph,node) = convert_sv_rec sv graph in - graph, node :: node_l - ) svl (graph,[]) in - let graph = S.add_vertex graph node in - let graph = List.fold_right (fun n graph -> - S.add_edge graph node n - ) node_l graph in - (graph,node) - - - | Sload (mc,addr,svl,sm) -> - let node = S.V.create (Oload (mc, addr), !counter) in - let (graph, node_l) = List.fold_right (fun sv (graph,node_l) -> - let (graph,node) = convert_sv_rec sv graph in - graph, node :: node_l - ) svl (graph,[]) in - let (graph,node_m) = convert_sm_rec sm graph in - let graph = S.add_vertex graph node in - let graph = List.fold_right (fun n graph -> - S.add_edge graph node n - ) node_l graph in - let graph = S.add_edge graph node node_m in - (graph,node) - + | Sreg res -> + let node = S.V.create (Oresource (Reg res), !counter) in + let graph = S.add_vertex graph node in + (graph,node) + + | Sop (op, svl) -> + let node = S.V.create (Oop op, !counter) in + let (graph, node_l) = List.fold_right (fun sv (graph,node_l) -> + let (graph,node) = convert_sv_rec sv graph in + graph, node :: node_l + ) svl (graph,[]) in + let graph = S.add_vertex graph node in + let graph = List.fold_right (fun n graph -> + S.add_edge graph node n + ) node_l graph in + (graph,node) + + + | Sload (mc,addr,svl,sm) -> + let node = S.V.create (Oload (mc, addr), !counter) in + let (graph, node_l) = List.fold_right (fun sv (graph,node_l) -> + let (graph,node) = convert_sv_rec sv graph in + graph, node :: node_l + ) svl (graph,[]) in + let (graph,node_m) = convert_sm_rec sm graph in + let graph = S.add_vertex graph node in + let graph = List.fold_right (fun n graph -> + S.add_edge graph node n + ) node_l graph in + let graph = S.add_edge graph node node_m in + (graph,node) + and convert_sm_rec sm graph = incr counter; match sm with - | Smem -> - let node = S.V.create (Oresource Mem, !counter) in - let graph = S.add_vertex graph node in - (graph,node) - - | Sstore (mc,addr,svl,sv,sm) -> - let node = S.V.create (Ostore (mc, addr), !counter) in - let (graph, node_l) = List.fold_right (fun sv (graph,node_l) -> - let (graph,node) = convert_sv_rec sv graph in - graph, node :: node_l - ) svl (graph,[]) in - let (graph, n) = convert_sv_rec sv graph in - let (graph, node_m) = convert_sm_rec sm graph in - let graph = S.add_vertex graph node in - let graph = List.fold_right (fun n graph -> - S.add_edge graph node n - ) node_l graph in - let graph = S.add_edge graph node n in - let graph = S.add_edge graph node node_m in - (graph,node) - + | Smem -> + let node = S.V.create (Oresource Mem, !counter) in + let graph = S.add_vertex graph node in + (graph,node) + + | Sstore (mc,addr,svl,sv,sm) -> + let node = S.V.create (Ostore (mc, addr), !counter) in + let (graph, node_l) = List.fold_right (fun sv (graph,node_l) -> + let (graph,node) = convert_sv_rec sv graph in + graph, node :: node_l + ) svl (graph,[]) in + let (graph, n) = convert_sv_rec sv graph in + let (graph, node_m) = convert_sm_rec sm graph in + let graph = S.add_vertex graph node in + let graph = List.fold_right (fun n graph -> + S.add_edge graph node n + ) node_l graph in + let graph = S.add_edge graph node n in + let graph = S.add_edge graph node node_m in + (graph,node) + let convert_sv sv = convert_sv_rec sv S.empty let convert_sm sm = convert_sm_rec sm S.empty let convert_sym st sm regs = let graph = State.fold (fun res sv g -> - if (not (List.mem res regs)) then g - else - let (graph,head) = convert_sv sv in - incr counter; - let src = S.V.create (Oresource (Reg res), !counter) in - let graph = S.add_vertex graph src in - let graph = S.add_edge graph src head in - Op.union g graph - ) st S.empty + if (not (List.mem res regs)) then g + else + let (graph,head) = convert_sv sv in + incr counter; + let src = S.V.create (Oresource (Reg res), !counter) in + let graph = S.add_vertex graph src in + let graph = S.add_edge graph src head in + Op.union g graph + ) st S.empty in let graph' = let (graph,head) = convert_sm sm in @@ -198,29 +198,29 @@ let convert_sym st sm regs = graph in Op.union graph graph' - + let display_st name l regs = let (st,sm,_) = symbolic_evaluation initial_state initial_mem initial_cons l in let g = convert_sym st sm regs in let addr = SPDebug.name ^ name in dot_output_ss g addr ; ignore (Sys.command ("(dot -Tpng " ^ addr ^ " -o " ^ addr ^ ".png ; rm -f " ^ addr ^ ") & ")) (* & *) - + let symbolic_equivalence (st1,sm1,cs1) (st2,sm2,cs2) regs = Printf.printf "|cs1| = %i - |cs2| = %i \n" (Cons.cardinal cs1) (Cons.cardinal cs2); (List.fold_right (fun res b -> - find res st1 = find res st2 && b - ) regs true - && sm1 = sm2 - && Cons.equal cs1 cs2) + find res st1 = find res st2 && b + ) regs true + && sm1 = sm2 + && Cons.equal cs1 cs2) let symbolic_evaluation = symbolic_evaluation initial_state initial_mem initial_cons let symbolic_condition i l = match i with - | Icond (cond,args) -> - let args = to_caml_list args in - let (st,sm,cs) = symbolic_evaluation l in - (cond,List.map (fun r -> find r st) args) - | _ -> failwith "Not a condition !\n" + | Icond (cond,args) -> + let args = to_caml_list args in + let (st,sm,cs) = symbolic_evaluation l in + (cond,List.map (fun r -> find r st) args) + | _ -> failwith "Not a condition !\n" diff --git a/src/SoftwarePipelining/SPTyping.ml b/src/SoftwarePipelining/SPTyping.ml index 16c9b01..9b9c679 100644 --- a/src/SoftwarePipelining/SPTyping.ml +++ b/src/SoftwarePipelining/SPTyping.ml @@ -520,7 +520,7 @@ let type_function f = | false -> false with | true -> check_successor f f.fn_entrypoint | false -> false with - | true -> Printf.fprintf SPDebug.dc "The code is well typed\n" - | false -> failwith "Type checking failure\n") + | true -> Printf.fprintf SPDebug.dc "The code is well typed\n" + | false -> failwith "Type checking failure\n") | None -> failwith "Type inference failure\n" *) diff --git a/src/SoftwarePipelining/SoftwarePipelining.ml b/src/SoftwarePipelining/SoftwarePipelining.ml index 12ab783..fd95134 100644 --- a/src/SoftwarePipelining/SoftwarePipelining.ml +++ b/src/SoftwarePipelining/SoftwarePipelining.ml @@ -19,37 +19,37 @@ let clean t = let rec clean_rec i = match i with - | 0 -> [] - | n -> - begin - match t.(i - 1) with - | None -> clean_rec (i - 1) - | Some inst -> inst :: clean_rec (i - 1) - end + | 0 -> [] + | n -> + begin + match t.(i - 1) with + | None -> clean_rec (i - 1) + | Some inst -> inst :: clean_rec (i - 1) + end in let l = List.rev (clean_rec (Array.length t)) in List.hd l :: (List.filter (fun e -> not (is_cond e)) (List.tl l)) let print_nodes = List.iter (fun n -> Printf.printf "%s \n" (string_of_node n)) - + (* random heuristic *) - + let find node schedule opt = try NI.find node schedule with - | Not_found -> opt + | Not_found -> opt let random ddg schedule = let unscheduled = G.fold_vertex (fun node l -> - match find node schedule None with - | Some v -> l - | None -> node :: l - ) ddg [] in + match find node schedule None with + | Some v -> l + | None -> node :: l + ) ddg [] in let bound = List.length unscheduled in Random.self_init (); List.nth unscheduled (Random.int bound) (* tought heuristics *) - + module Topo = Graph.Topological.Make (G) module Scc = Graph.Components.Make (G) @@ -63,8 +63,8 @@ let pipeliner ddg = if min <= 0 then None else Some {steady_state = steady_state; prolog = prolog; epilog = epilog; min = min; unrolling = unroll; - ramp_up = entrance; ramp_down = way_out} - + ramp_up = entrance; ramp_down = way_out} + let pipeline f = - SPBasic.apply_pipeliner f pipeliner ~debug:true + SPBasic.apply_pipeliner f pipeliner ~debug:false -- cgit