From 9e1268915a43c9668b0e6dda5426ba47d6b4870b Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 20 May 2020 17:57:54 +0200 Subject: RTL -> RTLpath -> RTL --- driver/Compiler.v | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 499feff2..37bb54f7 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -39,6 +39,7 @@ Require Tailcall. Require Inlining. Require Renumber. Require Duplicate. +Require RTLpath RTLpathLivegen. Require Constprop. Require CSE. Require ForwardMoves. @@ -152,6 +153,9 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 11) @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 12) + @@@ time "RTLpath generation" RTLpathLivegen.transf_program + @@ time "RTL projection" RTLpath.program_RTL + @@ print (print_RTL 13) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -263,6 +267,8 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) ::: mkpass Unusedglobproof.match_prog + ::: mkpass RTLpathLivegen.match_prog + ::: mkpass RTLpath.match_program_RTL ::: mkpass Allocproof.match_prog ::: mkpass Tunnelingproof.match_prog ::: mkpass Linearizeproof.match_prog @@ -310,7 +316,9 @@ Proof. destruct (partial_if optim_redundancy Deadcode.transf_program p13ter) as [p14|e] eqn:P14; simpl in T; try discriminate. set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. - destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. + destruct (RTLpathLivegen.transf_program p15) as [p15_1|e] eqn:P15_1; simpl in T; try discriminate. + set (p15_2 := RTLpath.program_RTL p15_1) in *. + destruct (Allocation.transf_program p15_2) as [p16|e] eqn:P16; simpl in T; try discriminate. set (p17 := Tunneling.tunnel_program p16) in *. destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. set (p19 := CleanupLabels.transf_program p18) in *. @@ -335,6 +343,8 @@ Proof. exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. exists p15; split. apply Unusedglobproof.transf_program_match; auto. + exists p15_1; split. apply RTLpathLivegen.transf_program_match; auto. + exists p15_2; split. apply RTLpath.transf_program_match; auto. exists p16; split. apply Allocproof.transf_program_match; auto. exists p17; split. apply Tunnelingproof.transf_program_match. exists p18; split. apply Linearizeproof.transf_program_match; auto. @@ -392,7 +402,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p25)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p27)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -429,6 +439,10 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. eapply compose_forward_simulations. eapply Unusedglobproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply RTLpathLivegen.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply RTLpath.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Allocproof.transf_program_correct; eassumption. eapply compose_forward_simulations. -- cgit From d46e96ef6c0287d6892bfc7d2272b7473f5e4979 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 28 May 2020 16:36:11 +0200 Subject: Branching stub scheduler --- driver/Compiler.v | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 37bb54f7..07889ae5 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -39,7 +39,7 @@ Require Tailcall. Require Inlining. Require Renumber. Require Duplicate. -Require RTLpath RTLpathLivegen. +Require RTLpath RTLpathLivegen RTLpathScheduler. Require Constprop. Require CSE. Require ForwardMoves. @@ -154,6 +154,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 12) @@@ time "RTLpath generation" RTLpathLivegen.transf_program + @@@ time "RTLpath scheduling" RTLpathScheduler.transf_program @@ time "RTL projection" RTLpath.program_RTL @@ print (print_RTL 13) @@@ time "Register allocation" Allocation.transf_program @@ -268,6 +269,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) ::: mkpass Unusedglobproof.match_prog ::: mkpass RTLpathLivegen.match_prog + ::: mkpass RTLpathScheduler.match_prog ::: mkpass RTLpath.match_program_RTL ::: mkpass Allocproof.match_prog ::: mkpass Tunnelingproof.match_prog @@ -317,8 +319,9 @@ Proof. set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. destruct (RTLpathLivegen.transf_program p15) as [p15_1|e] eqn:P15_1; simpl in T; try discriminate. - set (p15_2 := RTLpath.program_RTL p15_1) in *. - destruct (Allocation.transf_program p15_2) as [p16|e] eqn:P16; simpl in T; try discriminate. + destruct (RTLpathScheduler.transf_program p15_1) as [p15_2|e] eqn:P15_2; simpl in T; try discriminate. + set (p15_3 := RTLpath.program_RTL p15_2) in *. + destruct (Allocation.transf_program p15_3) as [p16|e] eqn:P16; simpl in T; try discriminate. set (p17 := Tunneling.tunnel_program p16) in *. destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. set (p19 := CleanupLabels.transf_program p18) in *. @@ -344,7 +347,8 @@ Proof. exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. exists p15; split. apply Unusedglobproof.transf_program_match; auto. exists p15_1; split. apply RTLpathLivegen.transf_program_match; auto. - exists p15_2; split. apply RTLpath.transf_program_match; auto. + exists p15_2; split. apply RTLpathScheduler.transf_program_match; auto. + exists p15_3; split. apply RTLpath.transf_program_match; auto. exists p16; split. apply Allocproof.transf_program_match; auto. exists p17; split. apply Tunnelingproof.transf_program_match. exists p18; split. apply Linearizeproof.transf_program_match; auto. @@ -402,7 +406,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p27)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p28)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -441,6 +445,8 @@ Ltac DestructM := eapply Unusedglobproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply RTLpathLivegen.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply RTLpathScheduler.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply RTLpath.transf_program_correct; eassumption. eapply compose_forward_simulations. -- cgit From d5f3ee00bb93b07f6f1a5859750cac345ed261aa Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 9 Jun 2020 17:32:11 +0200 Subject: RTLpathSchedulerproof.all_fundef_liveness_ok is a hypothesis again --- driver/Compiler.vexpand | 2 ++ 1 file changed, 2 insertions(+) (limited to 'driver') diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 3285a012..8aaa40c6 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -298,6 +298,8 @@ EXPAND_ASM_SEMANTICS EXPAND_RTL_FORWARD_SIMULATIONS eapply compose_forward_simulations. eapply RTLpathLivegenproof.transf_program_correct; eassumption. + pose proof RTLpathLivegenproof.all_fundef_liveness_ok as X. + refine (modusponens _ _ (X _ _ _) _); eauto. intro. eapply compose_forward_simulations. eapply RTLpathSchedulerproof.transf_program_correct; eassumption. eapply compose_forward_simulations. -- cgit From d37a9db8edb9c38c79940d9a3d647430a4c4d3e5 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Jul 2020 09:31:10 +0200 Subject: use a command-line option --- driver/Clflags.ml | 1 + driver/Driver.ml | 4 +++- 2 files changed, 4 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index eb21b3f8..fc5d9e45 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -36,6 +36,7 @@ let option_fredundancy = ref true let option_fduplicate = ref (-1) let option_finvertcond = ref true let option_ftracelinearize = ref false +let option_fprepass = ref false let option_fpostpass = ref true let option_fpostpass_sched = ref "list" let option_fifconversion = ref true diff --git a/driver/Driver.ml b/driver/Driver.ml index 90afb812..6accc22b 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -204,7 +204,8 @@ Processing options: -fcse3-glb Refine CSE3 information using greatest lower bounds [on] -fmove-loop-invariants Perform loop-invariant code motion [off] -fredundancy Perform redundancy elimination [on] - -fpostpass Perform postpass scheduling (only for K1 architecture) [on] + -fprepass Perform prepass scheduling (only for K1 architecture) [off] + -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= Perform postpass scheduling with the specified optimization [list] (=list: list scheduling, =ilp: ILP, =greedy: just packing bundles) -fduplicate Perform tail duplication to form superblocks on predicted traces @@ -419,6 +420,7 @@ let cmdline_actions = @ f_opt "cse3-glb" option_fcse3_glb @ f_opt "move-loop-invariants" option_fmove_loop_invariants @ f_opt "redundancy" option_fredundancy + @ f_opt "prepass" option_fprepass @ f_opt "postpass" option_fpostpass @ [ Exact "-fduplicate", Integer (fun n -> option_fduplicate := n) ] @ f_opt "invertcond" option_finvertcond -- cgit From eea5640e55890538fa43c3d5672853a0ae015b9c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 Jul 2020 11:00:15 +0200 Subject: command line selection of prepass scheduler --- driver/Clflags.ml | 1 + driver/Driver.ml | 3 +++ 2 files changed, 4 insertions(+) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index fc5d9e45..829af76a 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -37,6 +37,7 @@ let option_fduplicate = ref (-1) let option_finvertcond = ref true let option_ftracelinearize = ref false let option_fprepass = ref false +let option_fprepass_sched = ref "list" let option_fpostpass = ref true let option_fpostpass_sched = ref "list" let option_fifconversion = ref true diff --git a/driver/Driver.ml b/driver/Driver.ml index 6accc22b..fef9c166 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -205,6 +205,8 @@ Processing options: -fmove-loop-invariants Perform loop-invariant code motion [off] -fredundancy Perform redundancy elimination [on] -fprepass Perform prepass scheduling (only for K1 architecture) [off] + -fprepass= Perform postpass scheduling with the specified optimization [list] + (=list: list scheduling, =ilp: ILP, =greedy: just packing bundles) -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= Perform postpass scheduling with the specified optimization [list] (=list: list scheduling, =ilp: ILP, =greedy: just packing bundles) @@ -425,6 +427,7 @@ let cmdline_actions = @ [ Exact "-fduplicate", Integer (fun n -> option_fduplicate := n) ] @ f_opt "invertcond" option_finvertcond @ f_opt "tracelinearize" option_ftracelinearize + @ f_opt_str "prepass" option_fprepass option_fprepass_sched @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once -- cgit From 4764b4e2cf2fedb6165e4bf31d549f1df4e4a347 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 22 Oct 2020 13:38:45 +0200 Subject: -mtune= --- driver/Clflags.ml | 2 ++ driver/Driver.ml | 4 +++- 2 files changed, 5 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index d5f3aca5..a817b56a 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -42,6 +42,8 @@ let option_funrollsingle = ref 0 (* unroll a single iteration of innermost loops let option_funrollbody = ref 0 (* unroll the body of innermost loops of size n *) (* Scheduling *) +let option_mtune = ref "" + let option_fprepass = ref false let option_fprepass_sched = ref "list" diff --git a/driver/Driver.ml b/driver/Driver.ml index e5fc78f8..62e586f0 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -204,7 +204,8 @@ Processing options: -fcse3-glb Refine CSE3 information using greatest lower bounds [on] -fmove-loop-invariants Perform loop-invariant code motion [off] -fredundancy Perform redundancy elimination [on] - -fprepass Perform prepass scheduling (only for K1 architecture) [off] + -mtune= Type of CPU (for scheduling on some architectures) + -fprepass Perform prepass scheduling (only on some architectures) [off] -fprepass= Perform postpass scheduling with the specified optimization [list] (=list: list scheduling, =ilp: ILP, =greedy: just packing bundles) -fpostpass Perform postpass scheduling (only for K1 architecture) [on] @@ -420,6 +421,7 @@ let cmdline_actions = @ f_opt "cse3-glb" option_fcse3_glb @ f_opt "move-loop-invariants" option_fmove_loop_invariants @ f_opt "redundancy" option_fredundancy + @ [ Exact "-mtune", String (fun s -> option_mtune := s) ] @ f_opt "prepass" option_fprepass @ f_opt "postpass" option_fpostpass @ [ Exact "-ftailduplicate", Integer (fun n -> option_ftailduplicate := n) ] -- cgit From df9957ed3c48e3013f063fdf289eb75767fa6594 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 27 Oct 2020 11:48:42 +0100 Subject: deactivate LICM by default --- driver/Clflags.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index a817b56a..e9b0dade 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -100,7 +100,7 @@ let option_div_i32 = ref "stsud" let option_div_i64 = ref "stsud" let option_fcoalesce_mem = ref true let option_fforward_moves = ref false -let option_fmove_loop_invariants = ref true +let option_fmove_loop_invariants = ref false let option_fnontrap_loads = ref true let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 -- cgit From 09eed5e98d88260942d7860aec983c539faeac35 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 16 Nov 2020 07:04:13 +0100 Subject: Tunneling: improved elimination of conditions Previously, the elimination of useless conditions done in the 2nd pass of the tunneling introduced some new "nop" instructions that were not eliminated. This commit solves this issue by anticipating the elimination of conditions in the 1st pass of the tunneling, the 2nd pass being unchanged. In case of cycles in the CFG, the full elimination of useless conditions may require several iterations in the 1st pass. Moreover, in the simulation proof, the measure counting the number of eliminated steps from each node, needs to be adapted according to the modifications on the 1st pass. Hence, this measure results from a quite complex fixpoint computation: proving its properties would be very difficult. This leads us to introduce an oracle, implementing the first pass and producing the expected measure. A certified verifier directly checks that the measure provided by the oracle satisfies the properties expected by the simulation proof. Introducing this oracle/verifier pair has here the following advantage: - the proof is simpler than the original one (e.g. having a certified union-find structure is no more necessary for this pass). - the oracle is very efficient, by using imperative data-structure to compute memoized fixpoints. At runtime, the overhead induced by the verifier computations (and the actual computation of the measure) seems largely compensated by the gains obtained through the imperative oracle. --- driver/Compiler.vexpand | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 00db9b36..3acec956 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -54,7 +54,7 @@ Require Import Compopts. Parameter print_Clight: Clight.program -> unit. Parameter print_Cminor: Cminor.program -> unit. Parameter print_RTL: Z -> RTL.program -> unit. -Parameter print_LTL: LTL.program -> unit. +Parameter print_LTL: Z -> LTL.program -> unit. Parameter print_Mach: Mach.program -> unit. Local Open Scope string_scope. -- cgit