From 51e3a17d2e65b095861c243807f4e8d76c60ea0e Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 17 Dec 2020 10:02:23 +0000 Subject: Add Software pipelining stage by tristan et al. --- src/SoftwarePipelining/SPBase_types.ml | 143 ++++ src/SoftwarePipelining/SPBasic.ml | 834 ++++++++++++++++++++++++ src/SoftwarePipelining/SPBasic.mli | 67 ++ src/SoftwarePipelining/SPDebug.ml | 25 + src/SoftwarePipelining/SPIMS.ml | 178 +++++ src/SoftwarePipelining/SPIMS.mli | 22 + src/SoftwarePipelining/SPMVE.ml | 302 +++++++++ src/SoftwarePipelining/SPMVE.mli | 17 + src/SoftwarePipelining/SPSymbolic_evaluation.ml | 225 +++++++ src/SoftwarePipelining/SPTyping.ml | 528 +++++++++++++++ src/SoftwarePipelining/SPTyping.mli | 15 + src/SoftwarePipelining/SoftwarePipelining.ml | 73 +++ 12 files changed, 2429 insertions(+) create mode 100644 src/SoftwarePipelining/SPBase_types.ml create mode 100644 src/SoftwarePipelining/SPBasic.ml create mode 100644 src/SoftwarePipelining/SPBasic.mli create mode 100644 src/SoftwarePipelining/SPDebug.ml create mode 100644 src/SoftwarePipelining/SPIMS.ml create mode 100644 src/SoftwarePipelining/SPIMS.mli create mode 100644 src/SoftwarePipelining/SPMVE.ml create mode 100644 src/SoftwarePipelining/SPMVE.mli create mode 100644 src/SoftwarePipelining/SPSymbolic_evaluation.ml create mode 100644 src/SoftwarePipelining/SPTyping.ml create mode 100644 src/SoftwarePipelining/SPTyping.mli create mode 100644 src/SoftwarePipelining/SoftwarePipelining.ml (limited to 'src/SoftwarePipelining') diff --git a/src/SoftwarePipelining/SPBase_types.ml b/src/SoftwarePipelining/SPBase_types.ml new file mode 100644 index 0000000..3e339c3 --- /dev/null +++ b/src/SoftwarePipelining/SPBase_types.ml @@ -0,0 +1,143 @@ +(***********************************************************************) +(* *) +(* Compcert Extensions *) +(* *) +(* Jean-Baptiste Tristan *) +(* *) +(* All rights reserved. This file is distributed under the terms *) +(* described in file ../../LICENSE. *) +(* *) +(***********************************************************************) + + +open Camlcoq +open Op +open Registers +open Mem +open AST + +type ('a,'b) sum = ('a,'b) Datatypes.sum + +type instruction = + | Inop + | Iop of operation * reg CList.list * reg + | Iload of memory_chunk * addressing * reg CList.list * reg + | Istore of memory_chunk * addressing * reg CList.list * reg + | Icall of signature * (reg, ident) sum * reg CList.list * reg + | Itailcall of signature * (reg, ident) sum * reg CList.list + | Ialloc of reg * reg + | Icond of condition * reg CList.list + | Ireturn of reg Datatypes.option + +type resource = Reg of reg | Mem + +let inst_coq_to_caml = function + | RTL.Inop succ -> Inop + | RTL.Iop (op, args, dst, succ) -> Iop (op, args, dst) + | RTL.Iload (chunk, mode, args, dst, succ) -> Iload (chunk, mode, args, dst) + | RTL.Istore (chunk, mode, args, src, succ) -> Istore (chunk, mode, args, src) + | RTL.Icall (sign, id, args, dst, succ) -> Icall (sign, id, args, dst) + | RTL.Itailcall (sign, id, args) -> Itailcall (sign, id, args) + | RTL.Ialloc (dst, size, succ) -> Ialloc (dst, size) + | RTL.Icond (cond, args, succ1, succ2) -> Icond (cond, args) + | RTL.Ireturn (res) -> Ireturn (res) + +let inst_caml_to_coq i (links : RTL.node list) = + match i,links with + | Inop,[p] -> RTL.Inop p + | Iop (op, args, dst),[p] -> RTL.Iop (op, args, dst,p) + | Iload (chunk, mode, args, dst),[p] -> RTL.Iload (chunk, mode, args,dst,p) + | Istore (chunk, mode, args, src),[p] -> RTL.Istore (chunk, mode, args, src,p) + | Icall (sign, id, args, dst),[p] -> RTL.Icall (sign, id, args, dst,p) + | Itailcall (sign, id, args),[] -> RTL.Itailcall (sign, id, args) + | Ialloc (dst, size),[p] -> RTL.Ialloc (dst, size,p) + | Icond (cond, args),[p1;p2] -> RTL.Icond (cond,args,p1,p2) + | Ireturn (res),[] -> RTL.Ireturn res + | _,_ -> failwith "Echec lors de la conversion des instrucitons internes vers compcert" + + +let print_inst node = string_of_int (snd node) + +let to_int = fun n -> Int32.to_int (camlint_of_positive n) +let to_binpos = fun n -> positive_of_camlint (Int32.of_int n) + +let rec string_of_args args = + match args with + | CList.Coq_nil -> "" + | CList.Coq_cons (arg,args) -> "r" ^ (string_of_int (to_int arg)) ^ " " ^ string_of_args args + +let string_of_z z = string_of_int (Int32.to_int (Camlcoq.camlint_of_z z)) + +let string_of_comparison = function + | Integers.Ceq -> "eq" + | Integers.Cne -> "ne" + | Integers.Clt -> "lt" + | Integers.Cle -> "le" + | Integers.Cgt -> "gt" + | Integers.Cge -> "ge" + +let string_of_cond = function + | Ccomp c -> Printf.sprintf "comp %s" (string_of_comparison c) + | Ccompu c -> Printf.sprintf "compu %s" (string_of_comparison c) + | Ccompimm (c,i) -> Printf.sprintf "compimm %s %s" (string_of_comparison c) (string_of_z i) + | Ccompuimm (c,i) -> Printf.sprintf "compuimm %s %s" (string_of_comparison c) (string_of_z i) + | Ccompf c -> Printf.sprintf "compf %s" (string_of_comparison c) + | Cnotcompf c -> Printf.sprintf "notcompf %s" (string_of_comparison c) + | Cmaskzero i -> Printf.sprintf "maskzero %s" (string_of_z i) + | Cmasknotzero i -> Printf.sprintf "masknotzero %s" (string_of_z i) + +let string_of_op = function + | Omove -> "move" + | Ointconst i -> Printf.sprintf "intconst %s" (string_of_z i) + | Ofloatconst f -> Printf.sprintf "floatconst %s" (string_of_float f) + | Oaddrsymbol (id,i) -> Printf.sprintf "addrsymbol %s %s" (string_of_int (to_int id)) (string_of_z i) + | Oaddrstack i -> Printf.sprintf "addrstack %s" (string_of_z i) + | Ocast8signed -> "cast8signed" + | Ocast8unsigned -> "cast8unsigned" + | Ocast16signed -> "cast16signed" + | Ocast16unsigned -> "cast16unsigned" + | Oadd -> "add" + | Oaddimm i -> Printf.sprintf "addimm %s" (string_of_z i) + | Osub -> "sub" + | Osubimm i -> Printf.sprintf "subimm %s" (string_of_z i) + | Omul -> "mul" + | Omulimm i -> Printf.sprintf "mulimm %s" (string_of_z i) + | Odiv -> "div" + | Odivu -> "divu" + | Oand -> "and" + | Oandimm i -> Printf.sprintf "andimm %s" (string_of_z i) + | Oor -> "or" + | Oorimm i -> Printf.sprintf "orimm %s" (string_of_z i) + | Oxor -> "xor" + | Oxorimm i -> Printf.sprintf "xorimm %s" (string_of_z i) + | Onand -> "nand" + | Onor -> "nor" + | Onxor -> "nxor" + | Oshl -> "shl" + | Oshr -> "shr" + | Oshrimm i -> Printf.sprintf "shrimm %s" (string_of_z i) + | Oshrximm i -> Printf.sprintf "shrximm %s" (string_of_z i) + | Oshru -> "shru" + | Orolm (i,j) -> Printf.sprintf "rolm %s %s" (string_of_z i) (string_of_z j) + | Onegf -> "negf" + | Oabsf -> "absf" + | Oaddf -> "addf" + | Osubf -> "subf" + | Omulf -> "mulf" + | Odivf -> "divf" + | Omuladdf -> "muladdf" + | Omulsubf -> "mulsubf" + | Osingleoffloat -> "singleoffloat" + | Ointoffloat -> "intoffloat" + | Ointuoffloat -> "intuoffloat" + | Ofloatofint -> "floatofint" + | Ofloatofintu -> "floatofintu" + | Ocmp c -> Printf.sprintf "cmpcmpcmp" + +let rec to_coq_list = function + | [] -> CList.Coq_nil + | e :: l -> CList.Coq_cons (e,(to_coq_list l)) + +let rec to_caml_list = function + | CList.Coq_nil -> [] + | CList.Coq_cons (e,l) -> e :: to_caml_list l diff --git a/src/SoftwarePipelining/SPBasic.ml b/src/SoftwarePipelining/SPBasic.ml new file mode 100644 index 0000000..b070e3c --- /dev/null +++ b/src/SoftwarePipelining/SPBasic.ml @@ -0,0 +1,834 @@ +(***********************************************************************) +(* *) +(* Compcert Extensions *) +(* *) +(* Jean-Baptiste Tristan *) +(* *) +(* All rights reserved. This file is distributed under the terms *) +(* described in file ../../LICENSE. *) +(* *) +(***********************************************************************) + + +open Lengauer +open RTL +open Camlcoq +open Graph.Pack.Digraph +open Op +open Registers +open Mem +open AST +open Base_types +open Symbolic_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) +module Topo = Graph.Topological.Make (G) +module Index = Map.Make (struct type t = int let compare = compare end) + +let string_of_instruction node = + match G.V.label node with + | (Inop,n) -> Printf.sprintf "%i nop" n + | (Iop (op, args, dst),n) -> Printf.sprintf "%i r%i := %s %s" n (to_int dst) (string_of_op op) (string_of_args args) + | (Iload (chunk, mode, args, dst),n) -> Printf.sprintf "%i r%i := load %s" n (to_int dst) (string_of_args args) + | (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) + | (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 + +let string_of_node = string_of_instruction + +module Display = struct + include G + let vertex_name v = print_inst (V.label v) + let graph_attributes _ = [] + let default_vertex_attributes _ = [] + let vertex_attributes v = [`Label (string_of_instruction v)] + let default_edge_attributes _ = [] + let edge_attributes e = [`Label (string_of_int (G.E.label e))] + let get_subgraph _ = None +end +module Dot_ = Graph.Graphviz.Dot(Display) + +let dot_output g f = + let oc = open_out f in + Dot_.output_graph oc g; + close_out oc + +let display g name = + let addr = Debug.name ^ name in + dot_output g addr ; + 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*) + +let convert f = + + let make_node inst key = + let inst = inst_coq_to_caml inst in + G.V.create (inst, to_int key) + 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) + in + + let succ = RTL.successors f in + let rec link n succs g = + match succs with + | CList.Coq_nil -> g + | CList.Coq_cons (pos,CList.Coq_nil) -> + G.add_edge g (Index.find (to_int n) index) (Index.find (to_int pos) index) + | CList.Coq_cons (pos1, (CList.Coq_cons (pos2,CList.Coq_nil))) -> + 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 (succ key) g + ) 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 + + + + +(* dominator_tree calcule l arbre de domination grace au code de FP *) +let dominator_tree f = + + let module X = + struct + type node = G.V.t + let n = G.nb_vertex f.graph + let index (node : G.V.t) = snd(G.V.label node) - 1 + let successors fu n = + List.iter fu (G.succ f.graph n) + let predecessors fu n = + List.iter fu (G.pred f.graph n) + let start = f.start + end + in + + let module Y = Lengauer.Run (X) + + in + + Y.dominator + + + +(* detect_loops, find the loops in the graph and returns the list of nodes in it, + in dominating order !!! This is of great importance, we suppose that it is ordered + when we build the dependency graph *) +let detect_loops graph dom_tree = + + let rec is_dominating v1 v2 l = (* does v1 dominates v2 *) + match dom_tree v2 with + | None -> None + | Some v -> if v1 = v then Some (v :: l) else is_dominating v1 v (v :: l) + in + + G.fold_edges (fun v1 v2 loops -> + 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)) + +let print_instruction node = + match G.V.label node with + | (Inop,n) -> Printf.printf "%i : Inop \n" n + | (Iop (op, args, dst),n) -> Printf.printf "%i : Iop \n" n + | (Iload (chunk, mode, args, dst),n) -> Printf.printf "%i : Iload \n" n + | (Istore (chunk, mode, args, src),n) -> Printf.printf "%i : Istore \n" n + | (Icall (sign, id, args, dst),n) -> Printf.printf "%i : Icall \n" n + | (Itailcall (sign, id, args),n) -> Printf.printf "%i : Itailcall \n" n + | (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" + +let is_variant r loop = + List.fold_right (fun node b -> + 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 + in + + let is_branching node = + match fst (G.V.label node) with + | Icond _ -> true + | _ -> false + in + + let is_nop node = + match fst (G.V.label node) with + | Inop -> true + | _ -> false + in + + let is_OK_aux l = + List.fold_right (fun n b -> is_acceptable n && b) l true + in + + 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 :: [] -> not (is_variant r loop) + | 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 loop with + | v1 :: v2 :: l -> 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 + +(* 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 + +let rec to_res l = + match l with + | CList.Coq_nil -> [] + | CList.Coq_cons (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" + +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" + +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 + 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 + 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 *) +(* this is rather technical so we give many comments *) + +(* let n1 = G.V.create (Iop ((Ointconst ur),to_coq_list [],r1),next_pc) in *) +(* let next_pc = next_pc + 1 in *) +(* let n2 = G.V.create (Iop (Odiv,to_coq_list [bound;r1],r2),next_pc) in *) +(* let next_pc = next_pc + 1 in *) +(* let n3 = G.V.create (Iop ((Omulimm ur),to_coq_list [r2],r3),next_pc) in *) +(* let next_pc = next_pc + 1 in *) +(* let n4 = G.V.create (Iop (Osub,to_coq_list [bound;r3],r4),next_pc) in *) +(* let next_pc = next_pc + 1 in *) +(* let n5 = G.V.create (Iop (Omove,to_coq_list [r3],bound),next_pc) in (\* retouchee, [r3],bound *\) *) + + +let patch_graph graph entry lastone loop bound min ur r1 r2 r3 r4 next_pc prolog epilog ramp_up ramp_down = + + (* 1. Break the edge that enters the loop, except for the backedge *) + let preds_e = G.pred_e graph entry in + let wannabes = List.map G.E.src preds_e in + 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 + let graph = G.add_vertex graph cond in + let next_pc = next_pc + 1 in + + (* 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 + let n2 = G.V.create (Iop (Odiv,to_coq_list [bound;r1],r2),next_pc) in + let next_pc = next_pc + 1 in + let n3 = G.V.create (Iop (Omove,to_coq_list [bound],r4),next_pc) in + let next_pc = next_pc + 1 in + let n4 = G.V.create (Iop ((Omulimm ur ),to_coq_list [r2],r3),next_pc) in + let next_pc = next_pc + 1 in + let n5 = G.V.create (Iop ((Oaddimm (Camlcoq.z_of_camlint (Int32.of_int (-1)))),to_coq_list [r3],bound),next_pc) in (* retouchee, [r3],bound *) + let next_pc = next_pc + 1 in + let graph = G.add_vertex graph n1 in + let graph = G.add_vertex graph n2 in + let graph = G.add_vertex graph n3 in + let graph = G.add_vertex graph n4 in + let graph = G.add_vertex graph n5 in + let graph = G.add_edge_e graph (G.E.create cond 2 n1) in + let graph = G.add_edge graph n1 n2 in + 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 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 + 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 (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 + + (* 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,CList.Coq_cons (b,CList.Coq_nil),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 next_pc = next_pc + 1 in + + let ramp_down = List.map (fun (a,b) -> Iop (Omove,CList.Coq_cons (b,CList.Coq_nil),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 next_pc = next_pc + 1 in *) + + (* Creation des proloque et epilogue *) + + let graph = link prolog graph pipe_cond in + let graph = link ramp_up graph (List.hd prolog) in + let graph = link epilog graph (List.hd ramp_down) in + let graph = link ramp_down graph n6 in + + + let graph = G.add_edge graph n5 (List.hd ramp_up) in + let graph = G.add_edge_e graph (G.E.create pipe_cond 1 (List.hd epilog)) in + let graph = G.add_edge_e graph (G.E.create pipe_cond 2 (List.hd pipeline)) in + + (* 8. Retour sur la boucle classique *) + let graph = G.add_edge graph n6 entry in + + graph + +let regs_of_node node = + match G.V.label node with + | (Inop,n) -> [] + | (Iop (op, args, dst),n) -> dst :: (to_caml_list args) + | (Iload (chunk, mode, args, dst),n) -> dst :: (to_caml_list args) + | (Istore (chunk, mode, args, src),n) -> src :: (to_caml_list args) + | (Icall (sign, id, args, dst),n) -> dst :: (to_caml_list args) + | (Itailcall (sign, id, args),n) -> (to_caml_list args) + | (Ialloc (dst, size),n) -> [dst] + | (Icond (cond, args),n) -> (to_caml_list args) + | (Ireturn (res),n) -> match res with Datatypes.Some res -> [res] | _ -> [] + +let max_reg_of_graph graph params = + Printf.fprintf Debug.dc "Calcul du registre de depart.\n"; + let regs = G.fold_vertex (fun node regs -> + (regs_of_node node) @ regs + ) graph [] in + let regs = regs @ params in + let max_reg = List.fold_right (fun reg max -> + Printf.fprintf Debug.dc "%i " (Int32.to_int (Camlcoq.camlint_of_positive reg)); + if Int32.compare (Camlcoq.camlint_of_positive reg) max > 0 + then (Camlcoq.camlint_of_positive reg) + else max + ) regs Int32.zero in + + Printf.fprintf Debug.dc "MAX REG = %i\n" (Int32.to_int max_reg); + BinPos.coq_Psucc (Camlcoq.positive_of_camlint 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 borene 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 + +let substitute_pipeline graph loop steady_state prolog epilog min unrolling ru rd params = + let n1 = max_reg_of_graph graph params in + let n2 = (BinPos.coq_Psucc n1) in + let n3 = (BinPos.coq_Psucc n2) in + let n4 = (BinPos.coq_Psucc n3) in + let way_in = (List.hd loop) in + let way_out = (List.hd (List.rev loop)) in + let bound = (get_bound (List.hd (List.tl loop)) loop) in + let min = (Camlcoq.z_of_camlint (Int32.of_int min)) in + let unrolling = (Camlcoq.z_of_camlint (Int32.of_int 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 + let loops = List.filter (fun loop -> is_pipelinable (snd (loop))) loops in + 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} + +let delete_indexes l = List.map (fun e -> fst (G.V.label e) ) l + +type reg = Registers.reg + +let fresh = ref BinPos.Coq_xH + +let distance e = + match G.E.label e with + | 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" + +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 + +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)) + +let rec reforge_args args oldr newr = + match args with + | CList.Coq_nil -> CList.Coq_nil + | CList.Coq_cons (e,l) -> CList.Coq_cons ((if e = oldr then newr else e), (reforge_args l oldr newr)) + +let rec mem_args args r = + match args with + | CList.Coq_nil -> false + | CList.Coq_cons (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 + +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)) + +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 + 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" + +let fresh_regs n = + let t = Array.make n (BinPos.Coq_xH) in + for i = 0 to (n - 1) do + Array.set t i (!fresh); + fresh := BinPos.coq_Psucc !fresh + done; + t + +let print_reg r = Printf.fprintf Debug.dc "%i " (Int32.to_int (Camlcoq.camlint_of_positive r)) + +let is_cond node = + match fst (G.V.label node) with + | 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 [] + +let make_moves = List.map (fun (a,b) -> Iop (Omove,CList.Coq_cons (b,CList.Coq_nil),a)) + +let rec repeat l n = + match n with + | 0 -> [] + | n -> l @ repeat l (n-1) + +let fv = ref 0 + +let apply_pipeliner f p ?(debug=false) = + Printf.fprintf Debug.dc "******************** NEW FUNCTION ***********************\n"; + let cfg = convert f in + incr fv; + if debug then display cfg.graph ("input" ^ (string_of_int !fv)); + let loops = get_loops cfg in + 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 Debug.dc "__________________ NEW LOOP ____________________\n"; + Printf.printf "Pipelinable loop: "; + incr lv; + fresh := (BinPos.coq_Psucc + (BinPos.coq_Psucc + (BinPos.coq_Psucc + (BinPos.coq_Psucc + (BinPos.coq_Psucc + (max_reg_of_graph graph (to_caml_list f.fn_params) + )))))); + Printf.fprintf Debug.dc "FRESH = %i \n" + (Int32.to_int (Camlcoq.camlint_of_positive !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.tl loop)) in + let bt = (List.tl (delete_indexes pipe.steady_state)) in + let cond1 = fst (G.V.label (List.hd (List.tl 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 Debug.dc "pbte\n"; + List.iter (fun e -> + Printf.fprintf Debug.dc "%s\n" + (string_of_node (G.V.create (e,0))) + ) (p @ bt @ e); + Printf.fprintf Debug.dc "bu\n"; + List.iter (fun e -> Printf.fprintf Debug.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 = Camlcoq.positive_of_camlint (Int32.of_int (get_nextpc (graph))) + } in + Typing.type_function tg_to_type; + + tg diff --git a/src/SoftwarePipelining/SPBasic.mli b/src/SoftwarePipelining/SPBasic.mli new file mode 100644 index 0000000..03b3a97 --- /dev/null +++ b/src/SoftwarePipelining/SPBasic.mli @@ -0,0 +1,67 @@ +(***********************************************************************) +(* *) +(* Compcert Extensions *) +(* *) +(* Jean-Baptiste Tristan *) +(* *) +(* All rights reserved. This file is distributed under the terms *) +(* described in file ../../LICENSE. *) +(* *) +(***********************************************************************) + + +open Graph.Pack.Digraph + +(* DATA DEPENDENCY GRAPHS *) +module G : Graph.Sig.P + +(* We abstract the register type to make sure that the user won't mess up *) +type reg + +(* The scheduling should return a value of type pipeline *) +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 +} + +(* Operations on ddg *) + +val display : G.t -> string -> unit +val apply_pipeliner : RTL.coq_function -> (G.t -> pipeline option) -> ?debug:bool -> RTL.code +val get_succs_raw : G.t -> G.V.t -> G.V.t list + +(* Operations on instructions, the nodes of the data dependency graph *) + +val string_of_node : G.V.t -> string +val latency : G.V.t -> int +val reforge_reads : G.V.t -> reg -> reg -> G.V.t +val reforge_writes : G.V.t -> reg -> G.V.t +val written : G.V.t -> reg option +val is_cond : G.V.t -> bool + +(* Operations on dependencies, the edges of the data dependency graph *) + +type et = IntraRAW | IntraWAW | IntraWAR | InterRAW | InterWAW | InterWAR + +val edge_type : G.E.t -> et +val distance : G.E.t -> int + +(* Getting fresh registers, int is the number of required registers *) + +val fresh_regs : int -> reg array +val print_reg : reg -> unit + + + + + + + + + + diff --git a/src/SoftwarePipelining/SPDebug.ml b/src/SoftwarePipelining/SPDebug.ml new file mode 100644 index 0000000..b2ea257 --- /dev/null +++ b/src/SoftwarePipelining/SPDebug.ml @@ -0,0 +1,25 @@ +(***********************************************************************) +(* *) +(* Compcert Extensions *) +(* *) +(* Jean-Baptiste Tristan *) +(* *) +(* All rights reserved. This file is distributed under the terms *) +(* described in file ../../LICENSE. *) +(* *) +(***********************************************************************) + + +open Unix + +let tm = localtime (time ());; +let name = "../tmp/" ^ (string_of_int tm.tm_year) ^ "-" ^(string_of_int tm.tm_mon) ^ "-" ^(string_of_int tm.tm_mday) ^ + "-" ^(string_of_int tm.tm_hour) ^"-" ^(string_of_int tm.tm_min) ^ "-" ^(string_of_int tm.tm_sec) ^ "/";; +mkdir name 0o777;; +Printf.printf "Debug informations: %s \n" name ;; +let dc = open_out (name ^ "debug.log");; +let () = at_exit(fun () -> close_out dc);; + + + + diff --git a/src/SoftwarePipelining/SPIMS.ml b/src/SoftwarePipelining/SPIMS.ml new file mode 100644 index 0000000..a31f3d2 --- /dev/null +++ b/src/SoftwarePipelining/SPIMS.ml @@ -0,0 +1,178 @@ +(***********************************************************************) +(* *) +(* Compcert Extensions *) +(* *) +(* Jean-Baptiste Tristan *) +(* *) +(* All rights reserved. This file is distributed under the terms *) +(* described in file ../../LICENSE. *) +(* *) +(***********************************************************************) + + +open Graph.Pack.Digraph +open Basic + +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 + +let unpack v = + match v with + | Some v -> v + | None -> failwith "unpack abusif" + +let dep_latency edge = + match edge_type edge with + | 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 + 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 + +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 + +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 + (* 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*) + 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 [] + +let get_condition ddg = + let cond = G.fold_vertex (fun node cond -> + 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" + +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 + + let cond = get_condition ddg in + + while (!ii < max_interval && !notfound) do + (* Printf.printf "."; flush stdout; *) + ii := !ii + 1; + (* Printf.printf "NOUVEAU II %i \n" !ii; *) + let budget = ref (G.nb_vertex ddg * 10) in + let lasttime = ref NI.empty in + let schedtime = ref (NI.add cond (Some 0) NI.empty) in + let mrt = Array.make !ii None in + Array.set mrt 0 (Some cond); + + while (!budget > 0 && not (finished ddg !schedtime)) do (* Pretty inefficient *) + budget := !budget - 1; + let h = heightr ddg !schedtime in + let mintime = estart ddg !schedtime h !ii in + (* 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) + 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 + 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 + + 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 + +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) + +let print_schedule sched = + NI.iter (fun node time -> + Printf.fprintf Debug.dc "%s |---> %i \n" (string_of_node node) time + ) sched + diff --git a/src/SoftwarePipelining/SPIMS.mli b/src/SoftwarePipelining/SPIMS.mli new file mode 100644 index 0000000..bcd9ede --- /dev/null +++ b/src/SoftwarePipelining/SPIMS.mli @@ -0,0 +1,22 @@ +(***********************************************************************) +(* *) +(* Compcert Extensions *) +(* *) +(* Jean-Baptiste Tristan *) +(* *) +(* All rights reserved. This file is distributed under the terms *) +(* described in file ../../LICENSE. *) +(* *) +(***********************************************************************) + + +open Graph.Pack.Digraph +open Basic + +module NI : Map.S with type key = Basic.G.V.t + +(* piepeliner takes a data dependency graph and returns a schedule with an initiation interval + fails if cannot find any schedule *) +val pipeliner : G.t -> (G.t -> int option NI.t -> G.V.t) -> int NI.t * int + +val print_schedule : int NI.t -> unit diff --git a/src/SoftwarePipelining/SPMVE.ml b/src/SoftwarePipelining/SPMVE.ml new file mode 100644 index 0000000..a4efb49 --- /dev/null +++ b/src/SoftwarePipelining/SPMVE.ml @@ -0,0 +1,302 @@ +(***********************************************************************) +(* *) +(* Compcert Extensions *) +(* *) +(* Jean-Baptiste Tristan *) +(* *) +(* All rights reserved. This file is distributed under the terms *) +(* described in file ../../LICENSE. *) +(* *) +(***********************************************************************) + + +open Basic +open IMS + +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 + +let size_of_map2 m = + Mult.fold (fun key v size -> size + 1) m 0 + +let sched_max_time sched = + NI.fold (fun node time max -> + if time > max then time else max + ) sched 0 + +let print_table t s = + Printf.fprintf Debug.dc "%s : \n" s; + let string_of_node_ev node = + match node with + | Some node -> string_of_node node + | None -> "_" + in + Array.iteri (fun i node -> Printf.fprintf Debug.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 + +let minimizer qi ur = + + let rec fill n = + if n <= ur then n :: fill (n + 1) else [] + in + + let l = fill qi in + let l = List.map (fun e -> (e,ur mod e)) l in + 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; *) + let unroll = Mult.fold (fun reg mult max -> + 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 + 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 + Array.iter print_reg fregs; + Printf.fprintf Debug.dc "\n"; + Array.set regs i fregs + done; + + 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 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 Debug.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 Debug.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 Debug.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; + (* 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 steady = Array.make (ii * ur) None in + for i = 0 to (ur - 1) do + for time = 0 to (ii - 1) do + Array.set steady (time + i * ii) (steady_s.(time)) + done + done; + steady + +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; + 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" + done; + + prolog := List.rev (!prolog_piece) @ !prolog + done; + + !prolog + + +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" + 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 + in + + way_out_rec l [] + +let mve ddg sched ii = + assert (size_of_map1 sched = G.nb_vertex ddg); + Printf.fprintf Debug.dc "L'intervalle d'initiation est de : %i \n" ii; + Printf.fprintf Debug.dc "L'ordonnancement est le suivant : \n"; + print_schedule sched; + let (mult,unroll) = multiplicity ddg sched ii in + let unroll = unroll in (* changer pour tester, default doit etre egal a unroll *) + Printf.fprintf Debug.dc "Table de multiplicite : \n"; + Mult.iter (fun key mu -> print_reg key ; Printf.fprintf Debug.dc " |-> %i\n" mu) mult; + Printf.fprintf Debug.dc "Taux de deroulement de : %i \n" unroll; + let steady_state = crunch_and_unroll sched ii unroll in + let (steady_state,used_regs) = mve_kernel steady_state ddg sched ii mult unroll in + print_table steady_state "Table finale"; + let min = ((sched_max_time sched) / ii) + 1 in + Printf.fprintf Debug.dc "min : %i \n" min; + let iteration_table = compute_iteration_table sched ii in + Printf.fprintf Debug.dc "Table d'iteration \n"; + Array.iteri (fun i elt -> + match elt with + | Some elt -> + Printf.fprintf Debug.dc "%i : %i\n" i elt + | None -> Printf.fprintf Debug.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 + let epilog = List.filter (fun e -> not (is_cond e)) epilog in + Printf.fprintf Debug.dc "Prologue: \n"; + List.iter (fun node -> Printf.fprintf Debug.dc "%s \n" (string_of_node node)) prolog; + Printf.fprintf Debug.dc "Epilogue: \n"; + List.iter (fun node -> Printf.fprintf Debug.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/SPMVE.mli b/src/SoftwarePipelining/SPMVE.mli new file mode 100644 index 0000000..418a3ab --- /dev/null +++ b/src/SoftwarePipelining/SPMVE.mli @@ -0,0 +1,17 @@ +(***********************************************************************) +(* *) +(* Compcert Extensions *) +(* *) +(* Jean-Baptiste Tristan *) +(* *) +(* All rights reserved. This file is distributed under the terms *) +(* described in file ../../LICENSE. *) +(* *) +(***********************************************************************) + + +open Basic +open IMS + +val mve : G.t -> int NI.t -> int -> + (G.V.t option) array * G.V.t list * G.V.t list * int * int * (reg * reg) list * (reg * reg) list diff --git a/src/SoftwarePipelining/SPSymbolic_evaluation.ml b/src/SoftwarePipelining/SPSymbolic_evaluation.ml new file mode 100644 index 0000000..eba5707 --- /dev/null +++ b/src/SoftwarePipelining/SPSymbolic_evaluation.ml @@ -0,0 +1,225 @@ +(***********************************************************************) +(* *) +(* Compcert Extensions *) +(* *) +(* Jean-Baptiste Tristan *) +(* *) +(* All rights reserved. This file is distributed under the terms *) +(* described in file ../../LICENSE. *) +(* *) +(***********************************************************************) + + +open Registers +open Op +open AST +open Base_types + +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 + +module State = Map.Make (struct type t = reg let compare = compare end) + +module Cons = Set.Make (struct type t = symbolic_value let compare = compare end) + +type symbolic_state = symbolic_value State.t * Cons.t + +let initial_state = State.empty +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 + +let rec get_args st = function + | CList.Coq_nil -> [] + | CList.Coq_cons (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, CList.Coq_cons (src,CList.Coq_nil), dst) :: 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 + + | 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 + + | 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 + + | _ :: l -> raise Not_straight + +type osv = + | Oresource of resource + | Oop of operation + | Oload of memory_chunk * addressing + | Ostore of memory_chunk * addressing + +let string_of_osv = function + | Oresource (Reg r) -> Printf.sprintf "reg %i" (Int32.to_int (Camlcoq.camlint_of_positive r)) + | Oresource Mem -> "mem" + | Oop op -> string_of_op op + | Oload (mc,addr) -> "load" + | Ostore (mc,addr) -> "store" + +type ident = int + +module S = Graph.Persistent.Digraph.Abstract + (struct type t = osv * ident end) + +let name_of_vertex v = + let (osv,id) = S.V.label v in + Printf.sprintf "%i" id + +let string_of_vertex v = + let (osv,_) = S.V.label v in + Printf.sprintf "%s" (string_of_osv osv) + +module DisplayTree = struct + include S + let vertex_name v = name_of_vertex v + let graph_attributes _ = [] + let default_vertex_attributes _ = [] + let vertex_attributes v = [`Label (string_of_vertex v)] + let default_edge_attributes _ = [] + let edge_attributes _ = [] + let get_subgraph _ = None +end +module DotTree = Graph.Graphviz.Dot(DisplayTree) + +let dot_output_ss g f = + let oc = open_out f in + DotTree.output_graph oc g; + close_out oc + +module Build = Graph.Builder.P (S) +module Op = Graph.Oper.Make (Build) + +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) + +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) + +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 + in + let graph' = + let (graph,head) = convert_sm sm in + incr counter; + let src = S.V.create (Oresource Mem, !counter) in + let graph = S.add_vertex graph src in + let graph = S.add_edge graph src head in + 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 = Debug.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) + +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" diff --git a/src/SoftwarePipelining/SPTyping.ml b/src/SoftwarePipelining/SPTyping.ml new file mode 100644 index 0000000..f4e1f51 --- /dev/null +++ b/src/SoftwarePipelining/SPTyping.ml @@ -0,0 +1,528 @@ +(***********************************************************************) +(* *) +(* Compcert Extensions *) +(* *) +(* Jean-Baptiste Tristan *) +(* *) +(* All rights reserved. This file is distributed under the terms *) +(* described in file ../../LICENSE. *) +(* *) +(***********************************************************************) + + +open Datatypes +open CList +open Camlcoq +open Maps +open AST +open Op +open Registers +open RTL + +open Conventions +open Coqlib +open Errors +open Specif + + + +exception Type_error of string + +let env = ref (PTree.empty : typ PTree.t) + +let set_type r ty = + match PTree.get r !env with + | None -> env := PTree.set r ty !env + | Some ty' -> if ty <> ty' then + begin + Printf.fprintf Debug.dc "Failed to type register : %i " (Int32.to_int (Camlcoq.camlint_of_positive r)); + raise (Type_error "type mismatch") + end + +let rec set_types rl tyl = + match rl, tyl with + | Coq_nil, Coq_nil -> () + | Coq_cons(r1, rs), Coq_cons(ty1, tys) -> set_type r1 ty1; set_types rs tys + | _, _ -> raise (Type_error "arity mismatch") + +(* First pass: process constraints of the form typeof(r) = ty *) + +let type_instr retty (Coq_pair(pc, i)) = + Printf.fprintf Debug.dc "typage de l'instruction : %i \n" (Int32.to_int (Camlcoq.camlint_of_positive pc)); + match i with + | Inop(_) -> + () + | Iop(Omove, _, _, _) -> + () + | Iop(op, args, res, _) -> + let (Coq_pair(targs, tres)) = type_of_operation op in + set_types args targs; set_type res tres + | Iload(chunk, addr, args, dst, _) -> + set_types args (type_of_addressing addr); + set_type dst (type_of_chunk chunk) + | Istore(chunk, addr, args, src, _) -> + set_types args (type_of_addressing addr); + set_type src (type_of_chunk chunk) + | Icall(sg, ros, args, res, _) -> + begin try + begin match ros with + | Coq_inl r -> set_type r Tint + | Coq_inr _ -> () + end; + set_types args sg.sig_args; + set_type res (match sg.sig_res with None -> Tint | Some ty -> ty) + with Type_error msg -> + let name = + match ros with + | Coq_inl _ -> "" + | Coq_inr id -> extern_atom id in + raise(Type_error (Printf.sprintf "type mismatch in Icall(%s): %s" + name msg)) + end + | Itailcall(sg, ros, args) -> + begin try + begin match ros with + | Coq_inl r -> set_type r Tint + | Coq_inr _ -> () + end; + set_types args sg.sig_args; + if sg.sig_res <> retty then + raise (Type_error "mismatch on return type") + with Type_error msg -> + let name = + match ros with + | Coq_inl _ -> "" + | Coq_inr id -> extern_atom id in + raise(Type_error (Printf.sprintf "type mismatch in Itailcall(%s): %s" + name msg)) + end + | Ialloc(arg, res, _) -> + set_type arg Tint; set_type res Tint + | Icond(cond, args, _, _) -> + set_types args (type_of_condition cond) + | Ireturn(optres) -> + begin match optres, retty with + | None, None -> () + | Some r, Some ty -> set_type r ty + | _, _ -> raise (Type_error "type mismatch in Ireturn") + end + +let type_pass1 retty instrs = + coqlist_iter (type_instr retty) instrs + +(* Second pass: extract move constraints typeof(r1) = typeof(r2) + and solve them iteratively *) + +let rec extract_moves = function + | Coq_nil -> [] + | Coq_cons(Coq_pair(pc, i), rem) -> + match i with + | Iop(Omove, Coq_cons(r1, Coq_nil), r2, _) -> + (r1, r2) :: extract_moves rem + | Iop(Omove, _, _, _) -> + raise (Type_error "wrong Omove") + | _ -> + extract_moves rem + +let changed = ref false + +let rec solve_moves = function + | [] -> [] + | (r1, r2) :: rem -> + match (PTree.get r1 !env, PTree.get r2 !env) with + | Some ty1, Some ty2 -> + if ty1 = ty2 + then (changed := true; solve_moves rem) + else raise (Type_error "type mismatch in Omove") + | Some ty1, None -> + env := PTree.set r2 ty1 !env; changed := true; solve_moves rem + | None, Some ty2 -> + env := PTree.set r1 ty2 !env; changed := true; solve_moves rem + | None, None -> + (r1, r2) :: solve_moves rem + +let rec iter_solve_moves mvs = + changed := false; + let mvs' = solve_moves mvs in + if !changed then iter_solve_moves mvs' + +let type_pass2 instrs = + iter_solve_moves (extract_moves instrs) + +let typeof e r = + match PTree.get r e with Some ty -> ty | None -> Tint + +let infer_type_environment f instrs = + try + env := PTree.empty; + set_types f.fn_params f.fn_sig.sig_args; + type_pass1 f.fn_sig.sig_res instrs; + type_pass2 instrs; + let e = !env in + env := PTree.empty; + Some(typeof e) + with Type_error msg -> + Printf.eprintf "Error during RTL type inference: %s\n" msg; + None + +(** val typ_eq : typ -> typ -> bool **) + +let typ_eq t1 t2 = + match t1 with + | Tint -> (match t2 with + | Tint -> true + | Tfloat -> false) + | Tfloat -> (match t2 with + | Tint -> false + | Tfloat -> true) + +(** val opt_typ_eq : typ option -> typ option -> bool **) + +let opt_typ_eq t1 t2 = + match t1 with + | Some x -> (match t2 with + | Some t -> typ_eq x t + | None -> false) + | None -> (match t2 with + | Some t -> false + | None -> true) + +(** val check_reg : regenv -> reg -> typ -> bool **) + +let check_reg env r ty = + match typ_eq (env r) ty with + | true -> true + | false -> false + +(** val check_regs : regenv -> reg list -> typ list -> bool **) + +let rec check_regs env rl tyl = + match rl with + | Coq_nil -> + (match tyl with + | Coq_nil -> true + | Coq_cons (t, l) -> false) + | Coq_cons (r1, rs) -> + (match tyl with + | Coq_nil -> false + | Coq_cons (ty, tys) -> + (match typ_eq (env r1) ty with + | true -> check_regs env rs tys + | false -> false)) + +(** val check_op : regenv -> operation -> reg list -> reg -> bool **) + +let check_op env op args res0 = + let Coq_pair (targs, tres) = type_of_operation op in + (match check_regs env args targs with + | true -> + (match typ_eq (env res0) tres with + | true -> true + | false -> false) + | false -> false) + +(** val check_successor : coq_function -> node -> bool **) + +let check_successor funct s = + match Maps.PTree.get s funct.fn_code with + | Some i -> true + | None -> false + +(** val check_instr : coq_function -> regenv -> instruction -> bool **) + +let check_instr funct env = function + | Inop s -> check_successor funct s + | Iop (op, args, res0, s) -> + (match op with + | Omove -> + (match args with + | Coq_nil -> false + | Coq_cons (arg, l) -> + (match l with + | Coq_nil -> + (match typ_eq (env arg) (env res0) with + | true -> check_successor funct s + | false -> false) + | Coq_cons (r, l0) -> false)) + | Ointconst i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ofloatconst f -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oaddrsymbol (i0, i1) -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oaddrstack i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ocast8signed -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ocast8unsigned -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ocast16signed -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ocast16unsigned -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oadd -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oaddimm i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Osub -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Osubimm i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Omul -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Omulimm i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Odiv -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Odivu -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oand -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oandimm i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oor -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oorimm i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oxor -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oxorimm i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Onand -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Onor -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Onxor -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oshl -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oshr -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oshrimm i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oshrximm i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oshru -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Orolm (i0, i1) -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Onegf -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oabsf -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oaddf -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Osubf -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Omulf -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Odivf -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Omuladdf -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Omulsubf -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Osingleoffloat -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ointoffloat -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ointuoffloat -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ofloatofint -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ofloatofintu -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ocmp c -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false)) + | Iload (chunk, addr, args, dst, s) -> + (match check_regs env args (type_of_addressing addr) with + | true -> + (match typ_eq (env dst) (type_of_chunk chunk) with + | true -> check_successor funct s + | false -> false) + | false -> false) + | Istore (chunk, addr, args, src, s) -> + (match check_regs env args (type_of_addressing addr) with + | true -> + (match typ_eq (env src) (type_of_chunk chunk) with + | true -> check_successor funct s + | false -> false) + | false -> false) + | Icall (sig0, ros, args, res0, s) -> + (match match ros with + | Coq_inl r -> + (match typ_eq (env r) Tint with + | true -> check_regs env args sig0.sig_args + | false -> false) + | Coq_inr s0 -> check_regs env args sig0.sig_args with + | true -> + (match typ_eq (env res0) (proj_sig_res sig0) with + | true -> check_successor funct s + | false -> false) + | false -> false) + | Itailcall (sig0, ros, args) -> + (match match match ros with + | Coq_inl r -> + (match typ_eq (env r) Tint with + | true -> check_regs env args sig0.sig_args + | false -> false) + | Coq_inr s -> check_regs env args sig0.sig_args with + | true -> + proj_sumbool + (opt_typ_eq sig0.sig_res funct.fn_sig.sig_res) + | false -> false with + | true -> tailcall_is_possible sig0 + | false -> false) + | Ialloc (arg, res0, s) -> + (match typ_eq (env arg) Tint with + | true -> + (match typ_eq (env res0) Tint with + | true -> check_successor funct s + | false -> false) + | false -> false) + | Icond (cond, args, s1, s2) -> + (match match check_regs env args (type_of_condition cond) with + | true -> check_successor funct s1 + | false -> false with + | true -> check_successor funct s2 + | false -> false) + | Ireturn optres -> + (match optres with + | Some r -> + (match funct.fn_sig.sig_res with + | Some t -> + (match typ_eq (env r) t with + | true -> true + | false -> false) + | None -> false) + | None -> + (match funct.fn_sig.sig_res with + | Some t -> false + | None -> true)) + +(** val check_params_norepet : reg list -> bool **) + +let check_params_norepet params = + match list_norepet_dec Registers.Reg.eq params with + | true -> true + | false -> false + +(** val check_instrs : coq_function -> regenv -> (node, instruction) prod + list -> bool **) + +let rec check_instrs funct env = function + | Coq_nil -> true + | Coq_cons (p, rem) -> + let Coq_pair (pc, i) = p in + (match check_instr funct env i with + | true -> check_instrs funct env rem + | false -> false) + +(** val type_function : coq_function -> unit **) + +let type_function f = + let instrs = Maps.PTree.elements f.fn_code in + match infer_type_environment f instrs with + | Some env -> + (match match match match check_regs env f.fn_params + f.fn_sig.sig_args with + | true -> check_params_norepet f.fn_params + | false -> false with + | true -> check_instrs f env instrs + | false -> false with + | true -> check_successor f f.fn_entrypoint + | false -> false with + | true -> Printf.fprintf Debug.dc "The code is well typed\n" + | false -> failwith "Type checking failure\n") + | None -> failwith "Type inference failure\n" + diff --git a/src/SoftwarePipelining/SPTyping.mli b/src/SoftwarePipelining/SPTyping.mli new file mode 100644 index 0000000..c231ddd --- /dev/null +++ b/src/SoftwarePipelining/SPTyping.mli @@ -0,0 +1,15 @@ +(***********************************************************************) +(* *) +(* Compcert Extensions *) +(* *) +(* Jean-Baptiste Tristan *) +(* *) +(* All rights reserved. This file is distributed under the terms *) +(* described in file ../../LICENSE. *) +(* *) +(***********************************************************************) + + + +val type_function : RTL.coq_function -> unit + diff --git a/src/SoftwarePipelining/SoftwarePipelining.ml b/src/SoftwarePipelining/SoftwarePipelining.ml new file mode 100644 index 0000000..eeb2dfd --- /dev/null +++ b/src/SoftwarePipelining/SoftwarePipelining.ml @@ -0,0 +1,73 @@ +(***********************************************************************) +(* *) +(* Compcert Extensions *) +(* *) +(* Jean-Baptiste Tristan *) +(* *) +(* All rights reserved. This file is distributed under the terms *) +(* described in file ../../LICENSE. *) +(* *) +(***********************************************************************) + + +open Basic +open IMS +open MVE +open RTL + +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 + 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 + +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 + 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) + +let order = ref [] + +let pipeliner ddg = + order := List.flatten (Scc.scc_list ddg); + let (sched,ii) = IMS.pipeliner ddg random in + let (steady,prolog,epilog,min,unroll,entrance,way_out) = MVE.mve ddg sched ii in + let steady_state = clean steady in + 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} + + +let main f = + Basic.apply_pipeliner f pipeliner ~debug:false + + + -- cgit