diff options
-rw-r--r-- | scheduling/BTLScheduleraux.ml | 221 | ||||
-rw-r--r-- | scheduling/BTLaux.ml | 8 | ||||
-rw-r--r-- | scheduling/BTLtoRTLaux.ml | 4 | ||||
-rw-r--r-- | scheduling/RTLtoBTLaux.ml | 19 |
4 files changed, 231 insertions, 21 deletions
diff --git a/scheduling/BTLScheduleraux.ml b/scheduling/BTLScheduleraux.ml new file mode 100644 index 00000000..699538ca --- /dev/null +++ b/scheduling/BTLScheduleraux.ml @@ -0,0 +1,221 @@ +open AST +open Maps +open Registers +open BTL +open DebugPrint +open RTLcommonaux +open InstructionScheduler +open PrepassSchedulingOracleDeps + +let use_alias_analysis () = false + +let build_constraints_and_resources (opweights : opweights) insts btl = + let last_reg_reads : int list PTree.t ref = ref PTree.empty + and last_reg_write : (int * int) PTree.t ref = ref PTree.empty + and last_mem_reads : int list ref = ref [] + and last_mem_write : int option ref = ref None + and last_branch : int option ref = ref None + and last_non_pipelined_op : int array = + Array.make opweights.nr_non_pipelined_units (-1) + and latency_constraints : latency_constraint list ref = ref [] + and resources = ref [] in + let add_constraint instr_from instr_to latency = + assert (instr_from <= instr_to); + assert (latency >= 0); + if instr_from = instr_to then + if latency = 0 then () + else + failwith "PrepassSchedulingOracle.get_dependencies: negative self-loop" + else + latency_constraints := + { instr_from; instr_to; latency } :: !latency_constraints + and get_last_reads reg = + match PTree.get reg !last_reg_reads with Some l -> l | None -> [] + in + let add_input_mem i = + if not (use_alias_analysis ()) then ( + (* Read after write *) + (match !last_mem_write with None -> () | Some j -> add_constraint j i 1); + last_mem_reads := i :: !last_mem_reads) + and add_output_mem i = + if not (use_alias_analysis ()) then ( + (* Write after write *) + (match !last_mem_write with None -> () | Some j -> add_constraint j i 1); + (* Write after read *) + List.iter (fun j -> add_constraint j i 0) !last_mem_reads; + last_mem_write := Some i; + last_mem_reads := []) + and add_input_reg i reg = + (* Read after write *) + (match PTree.get reg !last_reg_write with + | None -> () + | Some (j, latency) -> add_constraint j i latency); + last_reg_reads := PTree.set reg (i :: get_last_reads reg) !last_reg_reads + and add_output_reg i latency reg = + (* Write after write *) + (match PTree.get reg !last_reg_write with + | None -> () + | Some (j, _) -> add_constraint j i 1); + (* Write after read *) + List.iter (fun j -> add_constraint j i 0) (get_last_reads reg); + last_reg_write := PTree.set reg (i, latency) !last_reg_write; + last_reg_reads := PTree.remove reg !last_reg_reads + in + let add_input_regs i regs = List.iter (add_input_reg i) regs + and irreversible_action i = + match !last_branch with None -> () | Some j -> add_constraint j i 1 + in + let set_branch i = + irreversible_action i; + last_branch := Some i + and add_non_pipelined_resources i resources = + Array.iter2 + (fun latency last -> + if latency >= 0 && last >= 0 then add_constraint last i latency) + resources last_non_pipelined_op; + Array.iteri + (fun rsc latency -> if latency >= 0 then last_non_pipelined_op.(rsc) <- i) + resources + in + Array.iteri + (fun i inst -> + (* TODO gourdinl liveins for Bcond *) + match inst with + | Bnop _ -> + let rs = Array.map (fun _ -> 0) opweights.pipelined_resource_bounds in + resources := rs :: !resources + | Bop (op, lr, rd, _) -> + add_non_pipelined_resources i + (opweights.non_pipelined_resources_of_op op (List.length lr)); + if Op.is_trapping_op op then irreversible_action i; + add_input_regs i lr; + add_output_reg i (opweights.latency_of_op op (List.length lr)) rd; + let rs = opweights.resources_of_op op (List.length lr) in + resources := rs :: !resources + | Bload (trap, chk, addr, lr, rd, _) -> + if trap = TRAP then irreversible_action i; + add_input_mem i; + add_input_regs i lr; + add_output_reg i + (opweights.latency_of_load trap chk addr (List.length lr)) + rd; + let rs = opweights.resources_of_load trap chk addr (List.length lr) in + resources := rs :: !resources + | Bstore (chk, addr, lr, src, _) -> + irreversible_action i; + add_input_regs i lr; + add_input_reg i src; + add_output_mem i; + let rs = opweights.resources_of_store chk addr (List.length lr) in + resources := rs :: !resources + | Bcond (cond, lr, BF (Bgoto s, _), Bnop _, _) -> + (* TODO gourdinl test with/out this line *) + let live = (get_some @@ PTree.get s btl).input_regs in + add_input_regs i (Regset.elements live); + set_branch i; + add_input_mem i; + add_input_regs i lr; + let rs = opweights.resources_of_cond cond (List.length lr) in + resources := rs :: !resources + | Bcond (_, _, _, _, _) -> + failwith "get_simple_dependencies: invalid Bcond" + | BF (_, _) -> failwith "get_simple_dependencies: BF" + | Bseq (_, _) -> failwith "get_simple_dependencies: Bseq") + insts; + (!latency_constraints, Array.of_list (List.rev !resources)) + +let define_problem (opweights : opweights) ibf btl = + let simple_deps, resources = + build_constraints_and_resources opweights ibf btl + in + { + max_latency = -1; + resource_bounds = opweights.pipelined_resource_bounds; + instruction_usages = resources; + latency_constraints = + (* if (use_alias_analysis ()) + then (get_alias_dependencies seqa) @ simple_deps + else *) + simple_deps; + } + +let zigzag_scheduler problem early_ones = + let nr_instructions = get_nr_instructions problem in + assert (nr_instructions = Array.length early_ones); + match list_scheduler problem with + | Some fwd_schedule -> + let fwd_makespan = fwd_schedule.(Array.length fwd_schedule - 1) in + let constraints' = ref problem.latency_constraints in + Array.iteri + (fun i is_early -> + if is_early then + constraints' := + { + instr_from = i; + instr_to = nr_instructions; + latency = fwd_makespan - fwd_schedule.(i); + } + :: !constraints') + early_ones; + validated_scheduler reverse_list_scheduler + { problem with latency_constraints = !constraints' } + | None -> None + +let prepass_scheduler_by_name name problem early_ones = + match name with + | "zigzag" -> zigzag_scheduler problem early_ones + | _ -> scheduler_by_name name problem + +let schedule_sequence insts btl = + let opweights = OpWeights.get_opweights () in + try + if Array.length insts <= 1 then None + else + let nr_instructions = Array.length insts in + let problem = define_problem opweights insts btl in + match + prepass_scheduler_by_name + !Clflags.option_fprepass_sched + problem + (Array.map + (fun inst -> + match inst with Bcond (_, _, _, _, _) -> true | _ -> false) + insts) + with + | None -> + Printf.printf "no solution in prepass scheduling\n"; + None + | Some solution -> + let positions = Array.init nr_instructions (fun i -> i) in + Array.sort + (fun i j -> + let si = solution.(i) and sj = solution.(j) in + if si < sj then -1 else if si > sj then 1 else i - j) + positions; + Some positions + with Failure s -> + Printf.printf "failure in prepass scheduling: %s\n" s; + None + +let flatten_blk_basics ibf = + let ib = ibf.entry in + let rec traverse_blk ib = + match ib with + | BF (_, _) + | Bcond (_, _, BF (Bgoto _, _), BF (Bgoto _, _), _) -> [] + | Bseq (ib1, ib2) -> + traverse_blk ib1 @ traverse_blk ib2 + | _ -> [ib] + in + Array.of_list (traverse_blk ib) + +let btl_scheduler btl entry = + List.iter (fun (n,ibf) -> + let bseq = flatten_blk_basics ibf in + match schedule_sequence bseq btl with + | Some positions -> + Array.iter (fun p -> debug "%d " p) positions + | None -> () + ) (PTree.elements btl); + (*let seqs = get_sequences seqs in*) + () diff --git a/scheduling/BTLaux.ml b/scheduling/BTLaux.ml index e8758f61..ca34c21c 100644 --- a/scheduling/BTLaux.ml +++ b/scheduling/BTLaux.ml @@ -1,9 +1,3 @@ -open Registers - type inst_info = { mutable inumb : int; mutable pcond : bool option } -type block_info = { - mutable bnumb : int; - mutable visited : bool; - mutable output_regs : Regset.t; -} +type block_info = { mutable bnumb : int; mutable visited : bool } diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml index 521f6ef2..42c20942 100644 --- a/scheduling/BTLtoRTLaux.ml +++ b/scheduling/BTLtoRTLaux.ml @@ -63,9 +63,9 @@ let translate_function code entry = Some ( Iload (trap, chk, addr, lr, rd, get_ib_num (get_some k)), get_inumb iinfo ) - | Bstore (chk, addr, lr, rd, iinfo) -> + | Bstore (chk, addr, lr, src, iinfo) -> Some - ( Istore (chk, addr, lr, rd, get_ib_num (get_some k)), + ( Istore (chk, addr, lr, src, get_ib_num (get_some k)), get_inumb iinfo ) | BF (Bcall (sign, fn, lr, rd, s), iinfo) -> next_nodes := s :: !next_nodes; diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml index 07e7a9d9..e932d766 100644 --- a/scheduling/RTLtoBTLaux.ml +++ b/scheduling/RTLtoBTLaux.ml @@ -1,11 +1,11 @@ open Maps open RTL open BTL -open Registers open PrintBTL open RTLcommonaux open DebugPrint open BTLaux +open BTLScheduleraux let undef_node = -1 @@ -13,7 +13,7 @@ let mk_iinfo _inumb _pcond = { inumb = _inumb; pcond = _pcond } let def_iinfo = { inumb = undef_node; pcond = None } -let mk_binfo _bnumb _output_regs = { bnumb = _bnumb; visited = false; output_regs = _output_regs } +let mk_binfo _bnumb = { bnumb = _bnumb; visited = false } let encaps_final inst osucc = match inst with @@ -33,9 +33,9 @@ let translate_inst (iinfo: BTL.inst_info) inst is_final = | Iload (trap, chk, addr, lr, rd, s) -> osucc := Some s; Bload (trap, chk, addr, lr, rd, iinfo) - | Istore (chk, addr, lr, rd, s) -> + | Istore (chk, addr, lr, src, s) -> osucc := Some s; - Bstore (chk, addr, lr, rd, iinfo) + Bstore (chk, addr, lr, src, iinfo) | Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s), iinfo) | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr), iinfo) | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s), iinfo) @@ -60,7 +60,6 @@ let translate_function code entry join_points liveness = else ( reached := PTree.set e true !reached; let next_nodes = ref [] in - let last = ref None in let rec build_btl_block n = let inst = get_some @@ PTree.get n code in let psucc = predicted_successor inst in @@ -91,7 +90,6 @@ let translate_function code entry join_points liveness = | _ -> Bseq (translate_inst iinfo inst false, build_btl_block s)) | None -> debug "BLOCK END.\n"; - last := Some inst; next_nodes := !next_nodes @ successors_inst inst; translate_inst iinfo inst true in @@ -99,12 +97,7 @@ let translate_function code entry join_points liveness = let succs = !next_nodes in let inputs = get_some @@ PTree.get e liveness in - let blk_last_successors = successors_inst (get_some @@ !last) in - let list_input_regs = List.map ( - fun n -> get_some @@ PTree.get n liveness - ) blk_last_successors in - let outputs = List.fold_left Regset.union Regset.empty list_input_regs in - let bi = mk_binfo (p2i e) outputs in + let bi = mk_binfo (p2i e) in let ibf = { entry = ib; input_regs = inputs; binfo = bi } in btl_code := PTree.set e ibf !btl_code; List.iter build_btl_tree succs) @@ -119,6 +112,8 @@ let rtl2btl (f : RTL.coq_function) = let liveness = analyze f in let btl = translate_function code entry join_points liveness in let dm = PTree.map (fun n i -> n) btl in + (* TODO gourdinl move elsewhere *) + btl_scheduler btl entry; debug "Entry %d\n" (p2i entry); debug "RTL Code: "; print_code code; |