From 7ae1fb0faea68ce5cfe04a232e49659247c244e9 Mon Sep 17 00:00:00 2001 From: "nicolas.nardino" Date: Fri, 4 Jun 2021 14:24:07 +0200 Subject: Passing info of live regs to scheduler: beginning --- aarch64/PostpassSchedulingOracle.ml | 1 + aarch64/PrepassSchedulingOracle.ml | 4 +++- 2 files changed, 4 insertions(+), 1 deletion(-) (limited to 'aarch64') diff --git a/aarch64/PostpassSchedulingOracle.ml b/aarch64/PostpassSchedulingOracle.ml index cde3e7a7..a9737088 100644 --- a/aarch64/PostpassSchedulingOracle.ml +++ b/aarch64/PostpassSchedulingOracle.ml @@ -507,6 +507,7 @@ let build_problem bb = { max_latency = -1; resource_bounds = opweights.pipelined_resource_bounds; + live_regs_entry = Registers.Regset.empty; (* PLACEHOLDER *) instruction_usages = instruction_usages bb; latency_constraints = latency_constraints bb; } diff --git a/aarch64/PrepassSchedulingOracle.ml b/aarch64/PrepassSchedulingOracle.ml index 2c3eb14f..1fd12a6a 100644 --- a/aarch64/PrepassSchedulingOracle.ml +++ b/aarch64/PrepassSchedulingOracle.ml @@ -410,6 +410,7 @@ let define_problem (opweights : opweights) seqa = let simple_deps = get_simple_dependencies opweights seqa in { max_latency = -1; resource_bounds = opweights.pipelined_resource_bounds; + live_regs_entry = Regset.empty; (* PLACEHOLDER *) instruction_usages = Array.map (resources_of_instruction opweights) (Array.map fst seqa); latency_constraints = (* if (use_alias_analysis ()) @@ -439,7 +440,8 @@ let prepass_scheduler_by_name name problem early_ones = | "zigzag" -> zigzag_scheduler problem early_ones | _ -> scheduler_by_name name problem -let schedule_sequence (seqa : (instruction*Regset.t) array) = +let schedule_sequence (seqa : (instruction*Regset.t) array) + (live_regs_entry : Registers.Regset.t)= let opweights = OpWeights.get_opweights () in try if (Array.length seqa) <= 1 -- cgit From 98a7a04258f2cf6caf9f18925cbeeae2f5b17be4 Mon Sep 17 00:00:00 2001 From: "nicolas.nardino" Date: Fri, 4 Jun 2021 16:56:32 +0200 Subject: computing live regs at sb entry from its live output regs --- aarch64/PrepassSchedulingOracle.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'aarch64') diff --git a/aarch64/PrepassSchedulingOracle.ml b/aarch64/PrepassSchedulingOracle.ml index 1fd12a6a..a743fb68 100644 --- a/aarch64/PrepassSchedulingOracle.ml +++ b/aarch64/PrepassSchedulingOracle.ml @@ -406,11 +406,11 @@ let get_alias_dependencies seqa = !deps;; *) -let define_problem (opweights : opweights) seqa = +let define_problem (opweights : opweights) (live_entry_regs : Regset.t) seqa = let simple_deps = get_simple_dependencies opweights seqa in { max_latency = -1; resource_bounds = opweights.pipelined_resource_bounds; - live_regs_entry = Regset.empty; (* PLACEHOLDER *) + live_regs_entry = live_entry_regs; instruction_usages = Array.map (resources_of_instruction opweights) (Array.map fst seqa); latency_constraints = (* if (use_alias_analysis ()) @@ -451,7 +451,7 @@ let schedule_sequence (seqa : (instruction*Regset.t) array) let nr_instructions = Array.length seqa in (if !Clflags.option_debug_compcert > 6 then Printf.printf "prepass scheduling length = %d\n" (Array.length seqa)); - let problem = define_problem opweights seqa in + let problem = define_problem opweights live_regs_entry seqa in (if !Clflags.option_debug_compcert > 7 then (print_sequence stdout (Array.map fst seqa); print_problem stdout problem)); -- cgit From 1701e43316ee8e69e794a025a8c9979af6bb8c93 Mon Sep 17 00:00:00 2001 From: "nicolas.nardino" Date: Thu, 10 Jun 2021 16:31:51 +0200 Subject: Work on new schedluer Renamed a test file, wrote function to compute pressure deltas, Still need to pass the info in some way; beginning of the actual scheduler function --- aarch64/Machregsaux.ml | 4 +++ aarch64/Machregsaux.mli | 2 ++ aarch64/PostpassSchedulingOracle.ml | 3 +- aarch64/PrepassSchedulingOracle.ml | 55 +++++++++++++++++++++++++++++++++++-- 4 files changed, 60 insertions(+), 4 deletions(-) (limited to 'aarch64') diff --git a/aarch64/Machregsaux.ml b/aarch64/Machregsaux.ml index 41db3bd4..15fb08ca 100644 --- a/aarch64/Machregsaux.ml +++ b/aarch64/Machregsaux.ml @@ -19,3 +19,7 @@ let class_of_type = function | AST.Tint | AST.Tlong -> 0 | AST.Tfloat | AST.Tsingle -> 1 | AST.Tany32 | AST.Tany64 -> assert false + +(* number of available registers per class *) +(* TODO: add this to all archs *) +let nr_regs = [| 29; 32 |] diff --git a/aarch64/Machregsaux.mli b/aarch64/Machregsaux.mli index 01b0f9fd..8487a557 100644 --- a/aarch64/Machregsaux.mli +++ b/aarch64/Machregsaux.mli @@ -15,3 +15,5 @@ val is_scratch_register: string -> bool val class_of_type: AST.typ -> int + +val nr_regs : int array diff --git a/aarch64/PostpassSchedulingOracle.ml b/aarch64/PostpassSchedulingOracle.ml index a9737088..834d42f5 100644 --- a/aarch64/PostpassSchedulingOracle.ml +++ b/aarch64/PostpassSchedulingOracle.ml @@ -507,7 +507,8 @@ let build_problem bb = { max_latency = -1; resource_bounds = opweights.pipelined_resource_bounds; - live_regs_entry = Registers.Regset.empty; (* PLACEHOLDER *) + live_regs_entry = Registers.Regset.empty; (* unused here *) + typing = (fun x -> AST.Tint); (* unused here *) instruction_usages = instruction_usages bb; latency_constraints = latency_constraints bb; } diff --git a/aarch64/PrepassSchedulingOracle.ml b/aarch64/PrepassSchedulingOracle.ml index a743fb68..6d445f10 100644 --- a/aarch64/PrepassSchedulingOracle.ml +++ b/aarch64/PrepassSchedulingOracle.ml @@ -201,6 +201,52 @@ let get_simple_dependencies (opweights : opweights) (seqa : (instruction*Regset. end seqa; !latency_constraints;; +let get_pressure_deltas (seqa : (instruction * Regset.t) array) + (typing : RTLtyping.regenv) + : int array array = + let nr_types_regs = Array.length Machregsaux.nr_regs in + let ret = Array.init (Array.length seqa) (fun i -> + Array.make nr_types_regs 0) in + Array.iteri (fun i (instr, liveins) -> match instr with + | Iop (_, args, dest, _) | Iload (_, _, _, args, dest, _) -> + ret.(i).(Machregsaux.class_of_type (typing dest)) <- + if List.mem dest args then 0 + else 1 + | Istore (_, _, _, src, _) -> + ret.(i).(Machregsaux.class_of_type (typing src)) <- + -1 + | Icall (_, fn, args, dest, _) -> + ret.(i).(Machregsaux.class_of_type (typing dest)) <- + if List.mem dest + (match fn with + | Datatypes.Coq_inl reg -> reg::args + | _ -> args) + then 0 else 1 + | Ibuiltin (_, args, dest, _) -> + let rec arg_l list = function + | AST.BA r -> r::list + | AST.BA_splitlong (hi, lo) | AST.BA_addptr (hi, lo) -> + arg_l (arg_l list lo) hi + | _ -> list + in + let l = (List.fold_left arg_l [] args) in + let rec dest_l = function + | AST.BR r -> + let t = Machregsaux.class_of_type (typing r) in + ret.(i).(t) <- + (if List.mem r l + then 0 else 1) + ret.(i).(t) + | AST.BR_splitlong (hi, lo) -> + dest_l hi; + dest_l lo + | _ -> () + in + dest_l dest + | _ -> () + ) seqa; + ret + + let resources_of_instruction (opweights : opweights) = function | Inop _ -> Array.map (fun _ -> 0) opweights.pipelined_resource_bounds | Iop(op, inputs, output, _) -> @@ -406,11 +452,13 @@ let get_alias_dependencies seqa = !deps;; *) -let define_problem (opweights : opweights) (live_entry_regs : Regset.t) seqa = +let define_problem (opweights : opweights) (live_entry_regs : Regset.t) + (typing : RTLtyping.regenv) seqa = let simple_deps = get_simple_dependencies opweights seqa in { max_latency = -1; resource_bounds = opweights.pipelined_resource_bounds; live_regs_entry = live_entry_regs; + typing = typing; instruction_usages = Array.map (resources_of_instruction opweights) (Array.map fst seqa); latency_constraints = (* if (use_alias_analysis ()) @@ -441,7 +489,8 @@ let prepass_scheduler_by_name name problem early_ones = | _ -> scheduler_by_name name problem let schedule_sequence (seqa : (instruction*Regset.t) array) - (live_regs_entry : Registers.Regset.t)= + (live_regs_entry : Registers.Regset.t) + (typing : RTLtyping.regenv) = let opweights = OpWeights.get_opweights () in try if (Array.length seqa) <= 1 @@ -451,7 +500,7 @@ let schedule_sequence (seqa : (instruction*Regset.t) array) let nr_instructions = Array.length seqa in (if !Clflags.option_debug_compcert > 6 then Printf.printf "prepass scheduling length = %d\n" (Array.length seqa)); - let problem = define_problem opweights live_regs_entry seqa in + let problem = define_problem opweights live_regs_entry typing seqa in (if !Clflags.option_debug_compcert > 7 then (print_sequence stdout (Array.map fst seqa); print_problem stdout problem)); -- cgit From 2b814b1f9bb30d9c8b59a713f69bced808bca7c7 Mon Sep 17 00:00:00 2001 From: "nicolas.nardino" Date: Sat, 12 Jun 2021 10:52:59 +0200 Subject: work on the scheduler --- aarch64/PostpassSchedulingOracle.ml | 1 + aarch64/PrepassSchedulingOracle.ml | 4 +++- 2 files changed, 4 insertions(+), 1 deletion(-) (limited to 'aarch64') diff --git a/aarch64/PostpassSchedulingOracle.ml b/aarch64/PostpassSchedulingOracle.ml index 834d42f5..867341ca 100644 --- a/aarch64/PostpassSchedulingOracle.ml +++ b/aarch64/PostpassSchedulingOracle.ml @@ -509,6 +509,7 @@ let build_problem bb = resource_bounds = opweights.pipelined_resource_bounds; live_regs_entry = Registers.Regset.empty; (* unused here *) typing = (fun x -> AST.Tint); (* unused here *) + pressure_deltas = [| [| |] |] ; instruction_usages = instruction_usages bb; latency_constraints = latency_constraints bb; } diff --git a/aarch64/PrepassSchedulingOracle.ml b/aarch64/PrepassSchedulingOracle.ml index 6d445f10..19f05749 100644 --- a/aarch64/PrepassSchedulingOracle.ml +++ b/aarch64/PrepassSchedulingOracle.ml @@ -201,6 +201,7 @@ let get_simple_dependencies (opweights : opweights) (seqa : (instruction*Regset. end seqa; !latency_constraints;; + let get_pressure_deltas (seqa : (instruction * Regset.t) array) (typing : RTLtyping.regenv) : int array array = @@ -459,7 +460,8 @@ let define_problem (opweights : opweights) (live_entry_regs : Regset.t) resource_bounds = opweights.pipelined_resource_bounds; live_regs_entry = live_entry_regs; typing = typing; - instruction_usages = Array.map (resources_of_instruction opweights) (Array.map fst seqa); + pressure_deltas = get_pressure_deltas seqa typing; + instruction_usages = Array.map (resources_of_instruction opweights) (Array.map fst seqa); latency_constraints = (* if (use_alias_analysis ()) then (get_alias_dependencies seqa) @ simple_deps -- cgit From bff4e6ff0b782619b6fcc18751fa575cbb11de68 Mon Sep 17 00:00:00 2001 From: "nicolas.nardino" Date: Mon, 14 Jun 2021 17:39:58 +0200 Subject: was very wrong, fixing --- aarch64/PostpassSchedulingOracle.ml | 2 +- aarch64/PrepassSchedulingOracle.ml | 11 +++++++---- 2 files changed, 8 insertions(+), 5 deletions(-) (limited to 'aarch64') diff --git a/aarch64/PostpassSchedulingOracle.ml b/aarch64/PostpassSchedulingOracle.ml index 867341ca..6f784238 100644 --- a/aarch64/PostpassSchedulingOracle.ml +++ b/aarch64/PostpassSchedulingOracle.ml @@ -509,7 +509,7 @@ let build_problem bb = resource_bounds = opweights.pipelined_resource_bounds; live_regs_entry = Registers.Regset.empty; (* unused here *) typing = (fun x -> AST.Tint); (* unused here *) - pressure_deltas = [| [| |] |] ; + reference_counting = None; instruction_usages = instruction_usages bb; latency_constraints = latency_constraints bb; } diff --git a/aarch64/PrepassSchedulingOracle.ml b/aarch64/PrepassSchedulingOracle.ml index 19f05749..fe757c99 100644 --- a/aarch64/PrepassSchedulingOracle.ml +++ b/aarch64/PrepassSchedulingOracle.ml @@ -202,6 +202,7 @@ let get_simple_dependencies (opweights : opweights) (seqa : (instruction*Regset. !latency_constraints;; +(** useless *) let get_pressure_deltas (seqa : (instruction * Regset.t) array) (typing : RTLtyping.regenv) : int array array = @@ -454,13 +455,13 @@ let get_alias_dependencies seqa = *) let define_problem (opweights : opweights) (live_entry_regs : Regset.t) - (typing : RTLtyping.regenv) seqa = + (typing : RTLtyping.regenv) reference_counting seqa = let simple_deps = get_simple_dependencies opweights seqa in { max_latency = -1; resource_bounds = opweights.pipelined_resource_bounds; live_regs_entry = live_entry_regs; typing = typing; - pressure_deltas = get_pressure_deltas seqa typing; + reference_counting = Some reference_counting; instruction_usages = Array.map (resources_of_instruction opweights) (Array.map fst seqa); latency_constraints = (* if (use_alias_analysis ()) @@ -492,7 +493,8 @@ let prepass_scheduler_by_name name problem early_ones = let schedule_sequence (seqa : (instruction*Regset.t) array) (live_regs_entry : Registers.Regset.t) - (typing : RTLtyping.regenv) = + (typing : RTLtyping.regenv) + reference = let opweights = OpWeights.get_opweights () in try if (Array.length seqa) <= 1 @@ -502,7 +504,8 @@ let schedule_sequence (seqa : (instruction*Regset.t) array) let nr_instructions = Array.length seqa in (if !Clflags.option_debug_compcert > 6 then Printf.printf "prepass scheduling length = %d\n" (Array.length seqa)); - let problem = define_problem opweights live_regs_entry typing seqa in + let problem = define_problem opweights live_regs_entry + typing reference seqa in (if !Clflags.option_debug_compcert > 7 then (print_sequence stdout (Array.map fst seqa); print_problem stdout problem)); -- cgit From 8f399dfa9d794f2f728f523ff1aa7788cc3599b2 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 17 Jun 2021 17:04:52 +0200 Subject: fix for Risc-V --- aarch64/Machregsaux.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'aarch64') diff --git a/aarch64/Machregsaux.mli b/aarch64/Machregsaux.mli index 8487a557..23ac1c9a 100644 --- a/aarch64/Machregsaux.mli +++ b/aarch64/Machregsaux.mli @@ -16,4 +16,5 @@ val is_scratch_register: string -> bool val class_of_type: AST.typ -> int +(* Number of registers in each class *) val nr_regs : int array -- cgit From 70f5867e441e253869cb3b432af77636a186d1cb Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 16 Jul 2021 12:26:27 +0200 Subject: rm TODO --- aarch64/Machregsaux.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'aarch64') diff --git a/aarch64/Machregsaux.ml b/aarch64/Machregsaux.ml index 15fb08ca..98e461eb 100644 --- a/aarch64/Machregsaux.ml +++ b/aarch64/Machregsaux.ml @@ -21,5 +21,4 @@ let class_of_type = function | AST.Tany32 | AST.Tany64 -> assert false (* number of available registers per class *) -(* TODO: add this to all archs *) let nr_regs = [| 29; 32 |] -- cgit From 169a221104c37737f12abe79711009fc0d88ce09 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 16 Jul 2021 13:00:56 +0200 Subject: rm useless code --- aarch64/PrepassSchedulingOracle.ml | 48 -------------------------------------- 1 file changed, 48 deletions(-) (limited to 'aarch64') diff --git a/aarch64/PrepassSchedulingOracle.ml b/aarch64/PrepassSchedulingOracle.ml index fe757c99..53a81095 100644 --- a/aarch64/PrepassSchedulingOracle.ml +++ b/aarch64/PrepassSchedulingOracle.ml @@ -201,54 +201,6 @@ let get_simple_dependencies (opweights : opweights) (seqa : (instruction*Regset. end seqa; !latency_constraints;; - -(** useless *) -let get_pressure_deltas (seqa : (instruction * Regset.t) array) - (typing : RTLtyping.regenv) - : int array array = - let nr_types_regs = Array.length Machregsaux.nr_regs in - let ret = Array.init (Array.length seqa) (fun i -> - Array.make nr_types_regs 0) in - Array.iteri (fun i (instr, liveins) -> match instr with - | Iop (_, args, dest, _) | Iload (_, _, _, args, dest, _) -> - ret.(i).(Machregsaux.class_of_type (typing dest)) <- - if List.mem dest args then 0 - else 1 - | Istore (_, _, _, src, _) -> - ret.(i).(Machregsaux.class_of_type (typing src)) <- - -1 - | Icall (_, fn, args, dest, _) -> - ret.(i).(Machregsaux.class_of_type (typing dest)) <- - if List.mem dest - (match fn with - | Datatypes.Coq_inl reg -> reg::args - | _ -> args) - then 0 else 1 - | Ibuiltin (_, args, dest, _) -> - let rec arg_l list = function - | AST.BA r -> r::list - | AST.BA_splitlong (hi, lo) | AST.BA_addptr (hi, lo) -> - arg_l (arg_l list lo) hi - | _ -> list - in - let l = (List.fold_left arg_l [] args) in - let rec dest_l = function - | AST.BR r -> - let t = Machregsaux.class_of_type (typing r) in - ret.(i).(t) <- - (if List.mem r l - then 0 else 1) + ret.(i).(t) - | AST.BR_splitlong (hi, lo) -> - dest_l hi; - dest_l lo - | _ -> () - in - dest_l dest - | _ -> () - ) seqa; - ret - - let resources_of_instruction (opweights : opweights) = function | Inop _ -> Array.map (fun _ -> 0) opweights.pipelined_resource_bounds | Iop(op, inputs, output, _) -> -- cgit From cf033ec29391d5358dea1d3b25da1738957478c4 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 16 Jul 2021 18:01:03 +0200 Subject: comment for authors --- aarch64/PrepassSchedulingOracle.ml | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'aarch64') diff --git a/aarch64/PrepassSchedulingOracle.ml b/aarch64/PrepassSchedulingOracle.ml index 53a81095..e09eea13 100644 --- a/aarch64/PrepassSchedulingOracle.ml +++ b/aarch64/PrepassSchedulingOracle.ml @@ -1,3 +1,16 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* Léo Gourdin UGA, VERIMAG *) +(* Nicolas Nardino ENS-Lyon, VERIMAG *) +(* *) +(* *) +(* *************************************************************) + open AST open RTL open Maps -- cgit