From 57dd7d55dceaa898b641a11398fa9a7254684105 Mon Sep 17 00:00:00 2001 From: Anton Lorenzen Date: Mon, 1 Apr 2024 12:16:30 +0100 Subject: [PATCH] Revert "feat: add comments and remove quadratic behaviour in ExpandResetReuse" This reverts commit 79ae165341810cbc21bf2481886b74ec9c71cb5d. --- src/Lean/Compiler/IR/ExpandResetReuse.lean | 154 ++++++++++++--------- 1 file changed, 90 insertions(+), 64 deletions(-) diff --git a/src/Lean/Compiler/IR/ExpandResetReuse.lean b/src/Lean/Compiler/IR/ExpandResetReuse.lean index 1aa90d9fbb1f..a927b3adf69d 100644 --- a/src/Lean/Compiler/IR/ExpandResetReuse.lean +++ b/src/Lean/Compiler/IR/ExpandResetReuse.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura, Anton Lorenzen +Authors: Leonardo de Moura -/ prelude import Lean.Compiler.IR.CompilerM @@ -9,10 +9,7 @@ import Lean.Compiler.IR.NormIds import Lean.Compiler.IR.FreeVars namespace Lean.IR.ExpandResetReuse - -/-- Mapping from variable to projections. - We use this in reuse specialization to avoid setting fields that are already set. --/ +/-- Mapping from variable to projections -/ abbrev ProjMap := HashMap VarId Expr namespace CollectProjMap abbrev Collector := ProjMap → ProjMap @@ -42,15 +39,7 @@ structure Context where abbrev Mask := Array (Option VarId) -/-- Auxiliary function for eraseProjIncFor. - Traverse bs left to right to find pairs of - ``` - let z := proj[i] y - inc z n c - ``` - If `n=1` remove the `inc` instruction and if `n>1` replace `inc z n c` with `inc z (n-1) c`. - Additionally, we track the variables `z` that have been found in the mask. --/ +/-- Auxiliary function for eraseProjIncFor -/ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (keep : Array FnBody) : Array FnBody × Mask := let done (_ : Unit) := (bs ++ keep.reverse, mask) let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop mask (keep.push b) @@ -82,7 +71,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke | _ => done () | _ => done () -/-- Try to erase one `inc` instruction on projections of `y` occurring in the tail of `bs`. +/-- Try to erase `inc` instructions on projections of `y` occurring in the tail of `bs`. Return the updated `bs` and a bit mask specifying which `inc`s have been removed. -/ def eraseProjIncFor (n : Nat) (y : VarId) (bs : Array FnBody) : Array FnBody × Mask := eraseProjIncForAux y bs (mkArray n none) #[] @@ -93,8 +82,6 @@ abbrev M := ReaderT Context (StateM Nat) def mkFreshJoinPoint : M JoinPointId := modifyGet fun n => ({ idx := n }, n + 1) -/-- If the reused cell is unique, we can reuse its memory. - Then we have to manually release all fields that are not live. -/ def releaseUnreadFields (y : VarId) (mask : Mask) : M (FnBody → FnBody) := mask.size.foldM (init := id) fun i b => match mask.get! i with @@ -103,6 +90,9 @@ def releaseUnreadFields (y : VarId) (mask : Mask) : M (FnBody → FnBody) := let fld ← mkFresh pure (FnBody.vdecl fld IRType.object (Expr.proj i y) ∘ (FnBody.dec fld 1 true false ∘ b)) +def setFields (y : VarId) (zs : Array Arg) (b : FnBody) : FnBody := + zs.size.fold (init := b) fun i b => FnBody.set y i (zs.get! i) b + /-- Given `set x[i] := y`, return true iff `y := proj[i] x` -/ def isSelfSet (ctx : Context) (x : VarId) (i : Nat) (y : Arg) : Bool := match y with @@ -112,12 +102,6 @@ def isSelfSet (ctx : Context) (x : VarId) (i : Nat) (y : Arg) : Bool := | _ => false | _ => false -/-- Set fields of `y` to `zs`. We avoid assignments that are already set. -/ -def setFields (ctx : Context) (y : VarId) (zs : Array Arg) (b : FnBody) : FnBody := - zs.size.fold (init := b) fun i b => - if isSelfSet ctx y i (zs.get! i) then b - else FnBody.set y i (zs.get! i) b - /-- Given `uset x[i] := y`, return true iff `y := uproj[i] x` -/ def isSelfUSet (ctx : Context) (x : VarId) (i : Nat) (y : VarId) : Bool := match ctx.projMap.find? y with @@ -130,12 +114,29 @@ def isSelfSSet (ctx : Context) (x : VarId) (n : Nat) (i : Nat) (y : VarId) : Boo | some (Expr.sproj m j w) => n == m && j == i && w == x | _ => false -/-- The empty reuse token returned for non-unique cells. -/ +/-- Remove unnecessary `set/uset/sset` operations -/ +partial def removeSelfSet (ctx : Context) : FnBody → FnBody + | FnBody.set x i y b => + if isSelfSet ctx x i y then removeSelfSet ctx b + else FnBody.set x i y (removeSelfSet ctx b) + | FnBody.uset x i y b => + if isSelfUSet ctx x i y then removeSelfSet ctx b + else FnBody.uset x i y (removeSelfSet ctx b) + | FnBody.sset x n i y t b => + if isSelfSSet ctx x n i y then removeSelfSet ctx b + else FnBody.sset x n i y t (removeSelfSet ctx b) + | FnBody.setTag x c b => FnBody.setTag x c (removeSelfSet ctx b) + | e => e + +/- New version of `mkFastPath` that uses drop-specialisation and reuse-specialisation + instead of expanding the resets to avoid code blowup. +-/ + def null := Expr.lit (LitVal.num 0) -/-- Create a new join point, where the declaration `v` obtains a function that will generate - a jump to the join point with the variable as an argument. We optimize the case, where - the binding is just a return and float it into the declaration. -/ +/- Create a new join point, where the declaration `v` obtains a function that will generate + a jump to the join point with the variable as an argument. We optimize the case, where + the binding is just a return and float it into the declaration. -/ def mkJoin (x : VarId) (t : IRType) (b : FnBody) (v : (VarId → FnBody) → FnBody) : M FnBody := match b with | FnBody.ret _ => @@ -143,39 +144,69 @@ def mkJoin (x : VarId) (t : IRType) (b : FnBody) (v : (VarId → FnBody) → FnB | _ => do let j ← mkFreshJoinPoint let z ← mkFresh - -- We use the given VarId for the joinpoint, which avoids the need to rename the tokens. - -- This is especially important since otherwise the ProjectionMap would find projections - -- out of the old variables and thus break reuse specialization. return FnBody.jdecl j #[mkParam z false t] (b.replaceVar x z) (v (fun z => mkJmp j #[Arg.var z])) -/-- Reuse specialization. -/ -def specializeReuse (reused token : VarId) (c : CtorInfo) (u : Bool) (t : IRType) (xs : Array Arg) (b : FnBody) : M FnBody := do +/- Reuse specialisation -/ +def tryReuse (reused token : VarId) (c : CtorInfo) (u : Bool) (t : IRType) (xs : Array Arg) (b : FnBody) : M FnBody := do let ctx ← read let null? ← mkFresh - let newAlloc ← mkFresh + let z ← mkFresh mkJoin reused t b fun jmp => (FnBody.vdecl null? IRType.uint8 (Expr.isNull token) (mkIf null? - (FnBody.vdecl newAlloc t (Expr.ctor c xs) - (jmp newAlloc)) - ((if u then FnBody.setTag token c.cidx else id) - (setFields ctx token xs - (jmp token))))) + (FnBody.vdecl z t (Expr.ctor c xs) + (jmp z)) + (removeSelfSet ctx + ((if u then FnBody.setTag token c.cidx else id) + (setFields token xs + (jmp token)))))) + +/- Apply reuse specialisation for a reuse instruction -/ +partial def reuseToTryReuse (x y : VarId) : FnBody → M FnBody + | FnBody.dec z n c p b => + if x == z then return FnBody.del y b + else do + let b ← reuseToTryReuse x y b + return FnBody.dec z n c p b + | FnBody.vdecl z t v b => + match v with + | Expr.reuse w c u zs => + if x == w then + tryReuse z y c u t zs b + else do + let b ← reuseToTryReuse x y b + return FnBody.vdecl z t v b + | _ => do + let b ← reuseToTryReuse x y b + return FnBody.vdecl z t v b + | FnBody.case tid z zType alts => do + let alts ← alts.mapM fun alt => alt.mmodifyBody (reuseToTryReuse x y) + return FnBody.case tid z zType alts + | FnBody.jdecl j xs v b => do + let v ← reuseToTryReuse x y v + let b ← reuseToTryReuse x y b + return FnBody.jdecl j xs v b + | e => + if e.isTerminal then return e + else do + let (instr, b) := e.split + let b ← reuseToTryReuse x y b + return instr.setBody b -/-- Increment all live children and decrement y. -/ def adjustReferenceCountsSlowPath (y : VarId) (mask : Mask) (b : FnBody) := let b := FnBody.dec y 1 true false b mask.foldl (init := b) fun b m => match m with | some z => FnBody.inc z 1 true false b | none => b -/- Drop specialization -/ -def specializeReset (token oldAlloc : VarId) (mask : Mask) (b : FnBody) : M FnBody := do +/- Drop specialisation -/ +def tryReset (token oldAlloc : VarId) (mask : Mask) (b : FnBody) : M FnBody := do let shared? ← mkFresh let z2 ← mkFresh let fastPath ← releaseUnreadFields oldAlloc mask + let b ← reuseToTryReuse token token b mkJoin token IRType.object b fun jmp => (FnBody.vdecl shared? IRType.uint8 (Expr.isShared oldAlloc) (mkIf shared? @@ -184,38 +215,33 @@ def specializeReset (token oldAlloc : VarId) (mask : Mask) (b : FnBody) : M FnBo (jmp z2))) (fastPath (jmp oldAlloc)))) -partial def searchAndSpecialize : FnBody → Array FnBody → Array VarId → M FnBody - | FnBody.vdecl x _ (Expr.reset n y) b, bs, tokens => do - let (bs, mask) := eraseProjIncFor n y bs - let b ← searchAndSpecialize b #[] (tokens.push x) - let b ← specializeReset x y mask b - return reshape bs b - | FnBody.vdecl z t (Expr.reuse w c u zs) b, bs, tokens => do - let b ← searchAndSpecialize b #[] tokens - let b ← specializeReuse z w c u t zs b - return reshape bs b - | FnBody.dec z n c p b, bs, tokens => - if Array.contains tokens z then return FnBody.del z b - else do - let b ← searchAndSpecialize b #[] tokens - return reshape bs (FnBody.dec z n c p b) - | FnBody.jdecl j xs v b, bs, tokens => do - let v ← searchAndSpecialize v #[] tokens - let b ← searchAndSpecialize b #[] tokens +mutual +partial def specialize (bs : Array FnBody) (x : VarId) (n : Nat) (y : VarId) (b : FnBody) : M FnBody := do + let (bs, mask) := eraseProjIncFor n y bs + let b ← tryReset x y mask b + searchAndExpand b bs + +partial def searchAndExpand : FnBody → Array FnBody → M FnBody + | FnBody.vdecl x _ (Expr.reset n y) b, bs => + specialize bs x n y b + | FnBody.jdecl j xs v b, bs => do + let v ← searchAndExpand v #[] + let b ← searchAndExpand b #[] return reshape bs (FnBody.jdecl j xs v b) - | FnBody.case tid x xType alts, bs, tokens => do - let alts ← alts.mapM fun alt => alt.mmodifyBody fun b => searchAndSpecialize b #[] tokens + | FnBody.case tid x xType alts, bs => do + let alts ← alts.mapM fun alt => alt.mmodifyBody fun b => searchAndExpand b #[] return reshape bs (FnBody.case tid x xType alts) - | b, bs, tokens => + | b, bs => if b.isTerminal then return reshape bs b - else searchAndSpecialize b.body (push bs b) tokens + else searchAndExpand b.body (push bs b) +end def main (d : Decl) : Decl := match d with | .fdecl (body := b) .. => let m := mkProjMap d let nextIdx := d.maxIndex + 1 - let bNew := (searchAndSpecialize b #[] #[] { projMap := m }).run' nextIdx + let bNew := (searchAndExpand b #[] { projMap := m }).run' nextIdx d.updateBody! bNew | d => d