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. --- tools/compiler_expand.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tools') diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 54946366..febb0282 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -50,8 +50,8 @@ PARTIAL, Always, Require, (Some "Unused globals"), "Unusedglob" let post_rtl_passes = [| - PARTIAL, Always, Require, (Some "Register allocation"), "Allocation", (Print "LTL"); - TOTAL, Always, Require, (Some "Branch tunneling"), "Tunneling", Noprint; + PARTIAL, Always, Require, (Some "Register allocation"), "Allocation", (Print "LTL 1"); + PARTIAL, Always, Require, (Some "Branch tunneling"), "Tunneling", (Print "LTL 2"); PARTIAL, Always, Require, (Some "CFG linearization"), "Linearize", Noprint; TOTAL, Always, Require, (Some "Label cleanup"), "CleanupLabels", Noprint; PARTIAL, (Option "debug"), Require, (Some "Debugging info for local variables"), "Debugvar", Noprint; -- cgit From a0cc099cb27ef311b6e8fd4ce85001a1d390db8a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 19 Nov 2020 17:09:16 +0100 Subject: merge nouveau tunneling --- tools/compiler_expand.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tools') diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index a6ae9b1f..04d29214 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -53,7 +53,7 @@ let post_rtl_passes = PARTIAL, Always, Require, (Some "RTLpath generation"), "RTLpathLivegen", Noprint; PARTIAL, Always, Require, (Some "Prepass scheduling"), "RTLpathScheduler", Noprint; TOTAL, Always, Require, (Some "Projection to RTL"), "RTLpath", (Print (Printf.sprintf "RTL %d" ((Array.length rtl_passes) + 1))); - PARTIAL, Always, Require, (Some "Register allocation"), "Allocation", (Print "LTL"); + PARTIAL, Always, Require, (Some "Register allocation"), "Allocation", (Print "LTL 1"); PARTIAL, Always, Require, (Some "Branch tunneling"), "Tunneling", (Print "LTL 2"); PARTIAL, Always, Require, (Some "CFG linearization"), "Linearize", Noprint; TOTAL, Always, Require, (Some "Label cleanup"), "CleanupLabels", Noprint; -- cgit From abae3de5118a4741ae1c2350a3e75b6e0a84a57d Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 2 Dec 2020 15:36:17 +0100 Subject: Slight perf improvement --- tools/compiler_expand.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tools') diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 04d29214..8d4f4f0b 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -25,10 +25,10 @@ TOTAL, Always, Require, (Some "Renumbering"), "Renumber"; PARTIAL, (Option "optim_CSE"), Require, (Some "CSE"), "CSE"; PARTIAL, Always, NoRequire, (Some "Static Prediction + inverting conditions"), "Staticpredict"; PARTIAL, Always, NoRequire, (Some "Unrolling one iteration out of innermost loops"), "Unrollsingle"; -TOTAL, Always, NoRequire, (Some "Renumbering pre unrolling"), "Renumber"; -PARTIAL, Always, NoRequire, (Some "Unrolling the body of innermost loops"), "Unrollbody"; TOTAL, Always, NoRequire, (Some "Renumbering pre tail duplication"), "Renumber"; PARTIAL, Always, NoRequire, (Some "Performing tail duplication"), "Tailduplicate"; +TOTAL, Always, NoRequire, (Some "Renumbering pre unrolling"), "Renumber"; +PARTIAL, Always, NoRequire, (Some "Unrolling the body of innermost loops"), "Unrollbody"; TOTAL, Always, NoRequire, (Some "Renumbering pre constprop"), "Renumber"; TOTAL, (Option "optim_constprop"), Require, (Some "Constant propagation"), "Constprop"; TOTAL, Always, NoRequire, (Some "Renumbering pre CSE"), "Renumber"; -- cgit