diff options
Diffstat (limited to 'src/hls/Schedule.ml')
-rw-r--r-- | src/hls/Schedule.ml | 97 |
1 files changed, 66 insertions, 31 deletions
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index 613236f..94225fa 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -26,6 +26,7 @@ open AST open Kildall open Op open RTLBlockInstr +open Predicate open RTLBlock open HTL open Verilog @@ -87,14 +88,25 @@ end)(struct let default = 0 end) +module DFGSimp = Graph.Persistent.Graph.Concrete(struct + type t = int * instr + let compare = compare + let equal = (=) + let hash = Hashtbl.hash + end) + +let convert dfg = + DFG.fold_vertex (fun v g -> DFGSimp.add_vertex g v) dfg DFGSimp.empty + |> DFG.fold_edges (fun v1 v2 g -> DFGSimp.add_edge (DFGSimp.add_edge g v1 v2) v2 v1) dfg + let reg r = sprintf "r%d" (P.to_int r) -let print_pred r = sprintf "p%d" (Nat.to_int r) +let print_pred r = sprintf "p%d" (P.to_int r) let print_instr = function | RBnop -> "" | RBload (_, _, _, _, r) -> sprintf "load(%s)" (reg r) | RBstore (_, _, _, _, r) -> sprintf "store(%s)" (reg r) - | RBsetpred (_, _, p) -> sprintf "setpred(%s)" (print_pred p) + | RBsetpred (_, _, _, p) -> sprintf "setpred(%s)" (print_pred p) | RBop (_, op, args, d) -> (match op, args with | Omove, _ -> "mov" @@ -203,6 +215,8 @@ module DFGDot = Graph.Graphviz.Dot(struct include DFG end) +module DFGDfs = Graph.Traverse.Dfs(DFG) + module IMap = Map.Make (struct type t = int @@ -341,7 +355,7 @@ let rec find_all_next_dst_read i dst i' curr = | RBload (_, _, _, rs, _) :: curr' -> check_dst rs curr' | RBstore (_, _, _, rs, src) :: curr' -> check_dst (src :: rs) curr' | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr' - | RBsetpred (_, rs, _) :: curr' -> check_dst rs curr' + | RBsetpred (_, _, rs, _) :: curr' -> check_dst rs curr' let drop i lst = let rec drop' i' lst' = @@ -400,10 +414,11 @@ let accumulate_WAW_mem_deps instrs dfg curri = let rec in_predicate p p' = match p' with - | Pvar p'' -> Nat.to_int p = Nat.to_int p'' - | Pnot p'' -> in_predicate p p'' + | Plit p'' -> P.to_int p = P.to_int (snd p'') | Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2 | Por (p1, p2) -> in_predicate p p1 || in_predicate p p2 + | Ptrue -> false + | Pfalse -> false let get_predicate = function | RBop (p, _, _, _) -> p @@ -413,7 +428,7 @@ let get_predicate = function let rec next_setpred p i = function | [] -> None - | RBsetpred (_, _, p') :: rst -> + | RBsetpred (_, _, _, p') :: rst -> if in_predicate p' p then Some i else @@ -446,7 +461,7 @@ let accumulate_RAW_pred_deps instrs dfg curri = let accumulate_WAR_pred_deps instrs dfg curri = let i, curr = curri in match curr with - | RBsetpred (_, _, p) -> ( + | RBsetpred (_, _, _, p) -> ( match next_preduse p 0 (take i instrs |> List.rev) with | None -> dfg | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) @@ -455,8 +470,8 @@ let accumulate_WAR_pred_deps instrs dfg curri = let accumulate_WAW_pred_deps instrs dfg curri = let i, curr = curri in match curr with - | RBsetpred (_, _, p) -> ( - match next_setpred (Pvar p) 0 (take i instrs |> List.rev) with + | RBsetpred (_, _, _, p) -> ( + match next_setpred (Plit (true, p)) 0 (take i instrs |> List.rev) with | None -> dfg | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) | _ -> dfg @@ -499,18 +514,18 @@ let assigned_vars vars = function | RBop (_, _, _, dst) -> dst :: vars | RBload (_, _, _, _, dst) -> dst :: vars | RBstore (_, _, _, _, _) -> vars - | RBsetpred (_, _, _) -> vars + | RBsetpred (_, _, _, _) -> vars let get_pred = function | RBnop -> None | RBop (op, _, _, _) -> op | RBload (op, _, _, _, _) -> op | RBstore (op, _, _, _, _) -> op - | RBsetpred (_, _, _) -> None + | RBsetpred (_, _, _, _) -> None let independant_pred p p' = - match sat_pred_temp (Nat.of_int 100000) (Pand (p, p')) with - | Some None -> true + match sat_pred_simple (Pand (p, p')) with + | None -> true | _ -> false let check_dependent op1 op2 = @@ -720,22 +735,22 @@ let parse_soln (tree, bbtree) s = else (tree, bbtree)) let solve_constraints constr = - let oc = open_out "lpsolve.txt" in + let (fn, oc) = Filename.open_temp_file "vericert_" "_lp_solve" in fprintf oc "%s\n" (print_lp constr); close_out oc; - Str.split (Str.regexp_string "\n") (read_process "lp_solve lpsolve.txt") - |> drop 3 - |> List.fold_left parse_soln (IMap.empty, IMap.empty) + let res = Str.split (Str.regexp_string "\n") (read_process ("lp_solve " ^ fn)) + |> drop 3 + |> List.fold_left parse_soln (IMap.empty, IMap.empty) + in + Sys.remove fn; res let subgraph dfg l = let dfg' = List.fold_left (fun g v -> DFG.add_vertex g v) DFG.empty l in List.fold_left (fun g v -> List.fold_left (fun g' v' -> let edges = DFG.find_all_edges dfg v v' in - List.fold_left (fun g'' e -> - DFG.add_edge_e g'' e - ) g' edges + List.fold_left DFG.add_edge_e g' edges ) g l ) dfg' l @@ -755,6 +770,21 @@ let combine_bb_schedule schedule s = let i, st = s in IMap.update st (update_schedule i) schedule +(**let add_el dfg i l = + List.*) + +let check_in el = + List.exists (List.exists ((=) el)) + +let all_dfs dfg = + let roots = DFG.fold_vertex (fun v li -> + if DFG.in_degree dfg v = 0 then v :: li else li + ) dfg [] in + let dfg' = DFG.fold_edges (fun v1 v2 g -> DFG.add_edge g v2 v1) dfg dfg in + List.fold_left (fun a el -> + if check_in el a then a else + (DFGDfs.fold_component (fun v l -> v :: l) [] dfg' el) :: a) [] roots + let range s e = List.init (e - s) (fun i -> i) |> List.map (fun x -> x + s) @@ -773,23 +803,29 @@ let transf_rtlpar c c' schedule = let i_sched_tree = List.fold_left combine_bb_schedule IMap.empty i_sched in - (*let body = IMap.to_seq i_sched_tree |> List.of_seq |> List.map snd + let body = IMap.to_seq i_sched_tree |> List.of_seq |> List.map snd |> List.map (List.map (fun x -> (x, List.nth bb_body' x))) - in*) - let body2 = List.fold_left (fun x b -> + in + (*let body2 = List.fold_left (fun x b -> match IMap.find_opt b i_sched_tree with | Some i -> i :: x | None -> [] :: x ) [] (range (fst bb_st_e) (snd bb_st_e + 1)) |> List.map (List.map (fun x -> (x, List.nth bb_body' x))) |> List.rev - in + in*) (*let final_body = List.map (fun x -> subgraph dfg x |> order_instr) body in*) let final_body2 = List.map (fun x -> subgraph dfg x - |> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x []) - |> List.rev) body2 + |> (fun x -> + all_dfs x + |> List.map (subgraph x) + |> List.map (fun y -> + TopoDFG.fold (fun i l -> snd i :: l) y [] + |> List.rev))) body + (*|> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x []) + |> List.rev) body2*) in - { bb_body = List.map (fun x -> [x]) final_body2; + { bb_body = final_body2; bb_exit = ctrl_flow } in @@ -799,7 +835,7 @@ let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) = let debug = true in let transf_graph (_, dfg, _) = dfg in let c' = PTree.map1 (fun x -> gather_bb_constraints false x |> transf_graph) c in - (*let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg (second o)) c' else PTree.empty in*) + (*let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg o) c' else PTree.empty in*) let cgraph = PTree.elements c' |> List.map (function (x, y) -> (P.to_int x, y)) |> List.fold_left (gather_cfg_constraints c) G.empty @@ -809,7 +845,7 @@ let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) = close_out graph; let schedule' = solve_constraints cgraph in (**IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';*) - (*printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*) + (**printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*) transf_rtlpar c c' schedule' let rec find_reachable_states c e = @@ -831,7 +867,6 @@ let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function = { fn_sig = f.fn_sig; fn_params = f.fn_params; fn_stacksize = f.fn_stacksize; - fn_code = List.fold_left (add_to_tree scheduled) PTree.empty reachable; - fn_funct_units = f.fn_funct_units; + fn_code = scheduled (*List.fold_left (add_to_tree scheduled) PTree.empty reachable*); fn_entrypoint = f.fn_entrypoint } |