Skip to content

Commit

Permalink
3863 llvm term cache (#3882)
Browse files Browse the repository at this point in the history
This PR introduces a cache for the terms returned from calls to
`Booster.LLVM.Internal.API.simplify`. Unpacking now uses a term store
for the unpacked terms, and recognises shared terms by a shallow index
into this store, using `TermF Int` as the map key (where the `Int` are
indexes of symbol application/injection arguments in the term store).

In small targeted tests using requests from MX-backend proofs , memory
consumption was noticeably reduced, also resulting in better
performance.

Currently, the cache only lives for the duration of one LLVM call (not
across different calls), no global variables or unsafe IO is required.

Fixes #3863
  • Loading branch information
jberthold authored May 22, 2024
1 parent 0f31483 commit 8b7ed67
Show file tree
Hide file tree
Showing 3 changed files with 216 additions and 94 deletions.
2 changes: 1 addition & 1 deletion booster/library/Booster/LLVM/Internal.hs
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ import System.Posix.DynamicLinker qualified as Linker

import Booster.LLVM.TH (dynamicBindings)
import Booster.Pattern.Base
import Booster.Pattern.Binary hiding (Block)
import Booster.Pattern.Binary
import Booster.Pattern.Util (sortOfTerm)
import Booster.Trace
import Booster.Trace qualified as Trace
Expand Down
7 changes: 2 additions & 5 deletions booster/library/Booster/Pattern/ApplyEquations.hs
Original file line number Diff line number Diff line change
Expand Up @@ -501,12 +501,9 @@ llvmSimplify term = do
withTermContext result $
emitEquationTrace t Nothing (Just "LLVM") Nothing $
Success result
toCache LLVM t result
pure result
| otherwise = do
result <- cb t
toCache LLVM t result
pure result
| otherwise =
cb t

----------------------------------------
-- Interface functions
Expand Down
Loading

0 comments on commit 8b7ed67

Please sign in to comment.