From bbe5cf63b26d492f8a537968a7c994709aa1e7fc Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 16 Nov 2022 10:24:46 -0800 Subject: [PATCH] perf: pick cache size coprime to pointer alignment --- src/Lean/Util/FindExpr.lean | 2 +- src/Lean/Util/FoldConsts.lean | 2 +- src/Lean/Util/ReplaceExpr.lean | 4 ++-- src/Lean/Util/ReplaceLevel.lean | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Lean/Util/FindExpr.lean b/src/Lean/Util/FindExpr.lean index ecc4e924c3..db6d64896d 100644 --- a/src/Lean/Util/FindExpr.lean +++ b/src/Lean/Util/FindExpr.lean @@ -10,7 +10,7 @@ namespace Expr namespace FindImpl -abbrev cacheSize : USize := 8192 +abbrev cacheSize : USize := 8192 - 1 structure State where keys : Array Expr -- Remark: our "unsafe" implementation relies on the fact that `()` is not a valid Expr diff --git a/src/Lean/Util/FoldConsts.lean b/src/Lean/Util/FoldConsts.lean index 4ef9038f05..044b36f30d 100644 --- a/src/Lean/Util/FoldConsts.lean +++ b/src/Lean/Util/FoldConsts.lean @@ -10,7 +10,7 @@ namespace Lean namespace Expr namespace FoldConstsImpl -abbrev cacheSize : USize := 8192 +abbrev cacheSize : USize := 8192 - 1 structure State where visitedTerms : Array Expr -- Remark: cache based on pointer address. Our "unsafe" implementation relies on the fact that `()` is not a valid Expr diff --git a/src/Lean/Util/ReplaceExpr.lean b/src/Lean/Util/ReplaceExpr.lean index e1c59c87da..853fc717c0 100644 --- a/src/Lean/Util/ReplaceExpr.lean +++ b/src/Lean/Util/ReplaceExpr.lean @@ -10,7 +10,7 @@ namespace Expr namespace ReplaceImpl -@[inline] def cacheSize : USize := 8192 +@[inline] def cacheSize : USize := 8192 - 1 structure Cache where -- First cacheSize elements are the keys. @@ -23,7 +23,7 @@ unsafe def Cache.new : Cache := @[inline] unsafe def Cache.keyIdx (key : Expr) : USize := - (ptrAddrUnsafe key >>> 4) % cacheSize + ptrAddrUnsafe key % cacheSize @[inline] unsafe def Cache.resultIdx (key : Expr) : USize := diff --git a/src/Lean/Util/ReplaceLevel.lean b/src/Lean/Util/ReplaceLevel.lean index 1185838ad6..df3c57b35a 100644 --- a/src/Lean/Util/ReplaceLevel.lean +++ b/src/Lean/Util/ReplaceLevel.lean @@ -23,7 +23,7 @@ namespace Expr namespace ReplaceLevelImpl -abbrev cacheSize : USize := 8192 +abbrev cacheSize : USize := 8192 - 1 structure State where keys : Array Expr -- Remark: our "unsafe" implementation relies on the fact that `()` is not a valid Expr