From c1609735342e08c2fecdd12ce929b35005c7869b Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 25 Feb 2026 16:08:22 +0800 Subject: [PATCH 1/3] chore: add .worktrees/ to gitignore --- .gitignore | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.gitignore b/.gitignore index 9914293a6e..c1620e1fdc 100644 --- a/.gitignore +++ b/.gitignore @@ -60,3 +60,6 @@ hie.yaml # the LLVM bindings from ./booster/cbits are symlinked to the root ./cbits to make HLS work /cbits + +# git worktrees +/.worktrees/ From fdf7d9e00e8ff5e730034e5ecdb30db7cd2d4dfb Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 25 Feb 2026 21:25:03 +0800 Subject: [PATCH 2/3] feat(booster): add builtin data structure benchmark framework --- .gitignore | 3 + booster/bench/BenchData.hs | 8 + booster/bench/Main.hs | 145 ++++++++ booster/hs-backend-booster.cabal | 38 +- booster/library/Booster/Benchmark/Data.hs | 338 ++++++++++++++++++ booster/library/Booster/Benchmark/Ops.hs | 167 +++++++++ booster/package.yaml | 41 +++ booster/unit-tests/Test/Booster/Benchmarks.hs | 140 ++++++++ scripts/run-bench-profile.sh | 78 ++++ 9 files changed, 957 insertions(+), 1 deletion(-) create mode 100644 booster/bench/BenchData.hs create mode 100644 booster/bench/Main.hs create mode 100644 booster/library/Booster/Benchmark/Data.hs create mode 100644 booster/library/Booster/Benchmark/Ops.hs create mode 100644 booster/unit-tests/Test/Booster/Benchmarks.hs create mode 100755 scripts/run-bench-profile.sh diff --git a/.gitignore b/.gitignore index c1620e1fdc..af08791b55 100644 --- a/.gitignore +++ b/.gitignore @@ -57,6 +57,9 @@ hie.yaml /scripts/bug-reports /booster/test/rpc-integration/resources/*.dylib /booster/test/*/definition/*kompiled/ +/booster/benchmarks.csv +/booster/booster-bench.hp +/plan.md # the LLVM bindings from ./booster/cbits are symlinked to the root ./cbits to make HLS work /cbits diff --git a/booster/bench/BenchData.hs b/booster/bench/BenchData.hs new file mode 100644 index 0000000000..4b72b72e61 --- /dev/null +++ b/booster/bench/BenchData.hs @@ -0,0 +1,8 @@ +{- | +Re-export benchmark fixture helpers for the benchmark executable. +-} +module BenchData ( + module Booster.Benchmark.Data, +) where + +import Booster.Benchmark.Data diff --git a/booster/bench/Main.hs b/booster/bench/Main.hs new file mode 100644 index 0000000000..8f4dd8ae24 --- /dev/null +++ b/booster/bench/Main.hs @@ -0,0 +1,145 @@ +{-# LANGUAGE OverloadedRecordDot #-} + +module Main (main) where + +import BenchData +import Booster.Benchmark.Ops +import Booster.Pattern.Base +import Test.Tasty.Bench + +main :: IO () +main = + defaultMain + [ bgroup "kmap" (map kmapBenchFor benchmarkSizes) + , bgroup "kset" (map ksetBenchFor benchmarkSizes) + , bgroup "klist" (map klistBenchFor benchmarkSizes) + , pipelineBenchmarks + ] + +kmapBenchFor :: Int -> Benchmark +kmapBenchFor size = + let mapTerm = mkMapTerm size + existingKey = mkLookupExistingKey size + missingKey = mkLookupMissingKey size + insertKey = mkInsertKey size + insertValue = mkUpdatedValue (size + 1) + updateValue = mkUpdatedValue (size + 2) + duplicatePairs = case mapTerm of + KMap _ pairs _ -> pairs <> reverse pairs + _ -> [] + coreBenches = + [ bench "lookup-existing" $ nf (runMapLookup mapTerm) existingKey + , bench "lookup-missing" $ nf (runMapLookup mapTerm) missingKey + , bench "size" $ nf runMapSize mapTerm + ] + heavyBenches = + [ bench "insert" $ nf (\(m, k, v) -> runMapUpdate m k v) (mapTerm, insertKey, insertValue) + , bench "update" $ nf (\(m, k, v) -> runMapUpdate m k v) (mapTerm, existingKey, updateValue) + , bench "remove" $ nf (\(m, k) -> runMapRemove m k) (mapTerm, existingKey) + , bench "keys" $ nf runMapKeys mapTerm + , bench "values" $ nf runMapValues mapTerm + , bench "in_keys" $ nf (runMapInKeys mapTerm) existingKey + , bench "sortAndDeduplicate" $ nf (\pairs -> KMap benchmarkKMapDef pairs Nothing) duplicatePairs + ] + in bgroup + ("size-" <> show size) + (coreBenches <> whenSizeAtMost 10000 size heavyBenches) + +ksetBenchFor :: Int -> Benchmark +ksetBenchFor size = + let leftSet = mkSetTerm size + rightSet = mkSetTerm (max 1 (size `div` 2)) + probe = mkSetElement (max 1 (size `div` 3)) + duplicateElements = case leftSet of + KSet _ elements _ -> elements <> reverse elements + _ -> [] + coreBenches = + [ bench "in" $ nf (ksetIn probe) leftSet + , bench "size" $ nf ksetSize leftSet + ] + heavyBenches = + [ bench "difference" $ nf (\(l, r) -> ksetDifference l r) (leftSet, rightSet) + , bench "union" $ nf (\(l, r) -> ksetUnion l r) (leftSet, rightSet) + , bench "intersection" $ nf (\(l, r) -> ksetIntersection l r) (leftSet, rightSet) + , bench "sortAndDeduplicate" $ nf (\elements -> KSet benchmarkKSetDef elements Nothing) duplicateElements + ] + in bgroup + ("size-" <> show size) + (coreBenches <> whenSizeAtMost 10000 size heavyBenches) + +klistBenchFor :: Int -> Benchmark +klistBenchFor size = + let listTerm = mkListTerm size + concatRhs = mkListConcatRhs size + idxMiddle = size `div` 2 + idxLast = max 0 (size - 1) + rangeTrim = max 0 (size `div` 4) + coreBenches = + [ bench "get-0" $ nf (runListGet listTerm) 0 + , bench "get-middle" $ nf (runListGet listTerm) idxMiddle + , bench "get-last" $ nf (runListGet listTerm) idxLast + , bench "size" $ nf runListSize listTerm + ] + heavyBenches = + [ bench "range" $ nf (\(l, f, b) -> runListRange l f b) (listTerm, rangeTrim, rangeTrim) + , bench "concat" $ nf (\(l, r) -> runListConcat l r) (listTerm, concatRhs) + ] + in bgroup + ("size-" <> show size) + (coreBenches <> whenSizeAtMost 10000 size heavyBenches) + +pipelineBenchmarks :: Benchmark +pipelineBenchmarks = + bgroup + "pipeline" + [ bgroup "kmap-matchMaps" (map mapMatchBenchFor matchMapBenchSizes) + , bgroup "ord-term" (map ordBenchFor pipelineBenchSizes) + , bgroup "substitution" (map substitutionBenchFor pipelineBenchSizes) + , bench "full-single-rule-pipeline" $ nfIO runPipelineOnce + ] + +matchMapBenchSizes :: [Int] +matchMapBenchSizes = [10, 100, 1000] + +pipelineBenchSizes :: [Int] +pipelineBenchSizes = [10, 100, 1000, 5000] + +mapMatchBenchFor :: Int -> Benchmark +mapMatchBenchFor size = + let patternMap = mkPatternMapForMatch size + subjectMap = mkSubjectMapForMatch size + in bgroup + ("size-" <> show size) + [ bench "matchMaps" $ whnf (\(p, s) -> matchMapTerms p s) (patternMap, subjectMap) + ] + +whenSizeAtMost :: Int -> Int -> [Benchmark] -> [Benchmark] +whenSizeAtMost limit size benchmarks + | size <= limit = benchmarks + | otherwise = [] + +ordBenchFor :: Int -> Benchmark +ordBenchFor size = + let left = mkMapTerm size + right = + case mkMapTerm size of + KMap def pairs rest -> + KMap def ((mkInsertKey (size + 7), mkUpdatedValue (size + 7)) : pairs) rest + other -> other + in bgroup + ("size-" <> show size) + [ bench "derived" $ whnf (\(a, b) -> compare a b) (left, right) + , bench "hash-first" $ whnf (\(a, b) -> compareTermHashFirst a b) (left, right) + ] + +substitutionBenchFor :: Int -> Benchmark +substitutionBenchFor size = + let unchangedKeyMap = mkMapWithValueVariables size + unchangedKeySubst = mkValueSubstitution size + changedKeyMap = mkMapWithKeyVariables size + changedKeySubst = mkKeySubstitution size + in bgroup + ("size-" <> show size) + [ bench "unchanged-keys" $ nf (\(subst, term) -> substituteMap subst term) (unchangedKeySubst, unchangedKeyMap) + , bench "changed-keys" $ nf (\(subst, term) -> substituteMap subst term) (changedKeySubst, changedKeyMap) + ] diff --git a/booster/hs-backend-booster.cabal b/booster/hs-backend-booster.cabal index e3722ab1fb..66aaf41085 100644 --- a/booster/hs-backend-booster.cabal +++ b/booster/hs-backend-booster.cabal @@ -223,6 +223,11 @@ source-repository head type: git location: https://github.com/runtimeverification/hs-backend-booster +flag profiling + description: Enable profiling-friendly build options for benchmark runs. + manual: True + default: False + library exposed-modules: Booster.Builtin @@ -232,6 +237,8 @@ library Booster.Builtin.KEQUAL Booster.Builtin.LIST Booster.Builtin.MAP + Booster.Benchmark.Data + Booster.Benchmark.Ops Booster.CLOptions Booster.Definition.Attributes.Base Booster.Definition.Attributes.Reader @@ -330,6 +337,8 @@ library , unix , unliftio , unordered-containers + if flag(profiling) + ghc-options: -prof -fprof-auto default-language: Haskell2010 executable kore-rpc-booster @@ -440,7 +449,7 @@ test-suite predicates-integration test/predicates-integration default-extensions: BangPatterns DataKinds DefaultSignatures DeriveAnyClass DeriveGeneric DerivingStrategies DerivingVia DuplicateRecordFields EmptyCase FlexibleInstances FunctionalDependencies GADTs GeneralizedNewtypeDeriving ImportQualifiedPost KindSignatures LambdaCase MultiParamTypeClasses NamedFieldPuns OverloadedRecordDot OverloadedStrings PolyKinds ScopedTypeVariables StandaloneDeriving TupleSections TypeApplications TypeFamilies ViewPatterns - ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -j6 + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -j6 -rtsopts -threaded -with-rtsopts=-N build-depends: base , bytestring @@ -461,6 +470,7 @@ test-suite unit-tests type: exitcode-stdio-1.0 main-is: Driver.hs other-modules: + Test.Booster.Benchmarks Test.Booster.Builtin Test.Booster.Definition.Internalise Test.Booster.Fixture @@ -507,3 +517,29 @@ test-suite unit-tests , text , transformers default-language: Haskell2010 + +benchmark booster-bench + type: exitcode-stdio-1.0 + main-is: Main.hs + other-modules: + BenchData + Paths_hs_backend_booster + hs-source-dirs: + bench + default-extensions: + BangPatterns DataKinds DefaultSignatures DeriveAnyClass DeriveGeneric DerivingStrategies DerivingVia DuplicateRecordFields EmptyCase FlexibleInstances FunctionalDependencies GADTs GeneralizedNewtypeDeriving ImportQualifiedPost KindSignatures LambdaCase MultiParamTypeClasses NamedFieldPuns OverloadedRecordDot OverloadedStrings PolyKinds ScopedTypeVariables StandaloneDeriving TupleSections TypeApplications TypeFamilies ViewPatterns + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -j6 -rtsopts -threaded -with-rtsopts=-N + build-depends: + base + , bytestring + , containers + , deepseq + , hashable + , hs-backend-booster + , monad-logger + , tasty-bench + , text + , transformers + if flag(profiling) + ghc-options: -prof -fprof-auto + default-language: Haskell2010 diff --git a/booster/library/Booster/Benchmark/Data.hs b/booster/library/Booster/Benchmark/Data.hs new file mode 100644 index 0000000000..832211f6c8 --- /dev/null +++ b/booster/library/Booster/Benchmark/Data.hs @@ -0,0 +1,338 @@ +{-# LANGUAGE OverloadedRecordDot #-} + +{- | +Copyright : (c) Runtime Verification, 2026 +License : BSD-3-Clause + +Benchmark fixtures and synthetic data for booster benchmark suites. +-} +module Booster.Benchmark.Data ( + benchmarkSizes, + benchmarkDefinition, + benchmarkKMapDef, + benchmarkKSetDef, + benchmarkKListDef, + mkMapTerm, + mkMapWithValueVariables, + mkMapWithKeyVariables, + mkPatternMapForMatch, + mkSubjectMapForMatch, + mkValueSubstitution, + mkKeySubstitution, + mkLookupExistingKey, + mkLookupMissingKey, + mkInsertKey, + mkUpdatedValue, + mkListTerm, + mkListConcatRhs, + mkSetTerm, + mkMapKey, + mkMapValue, + mkListElement, + mkSetElement, + pipelinePatternTerm, + pipelineSubjectTerm, + pipelineRhsTerm, + validateKMap, + validateKSet, + validateKList, +) where + +import Data.ByteString.Char8 qualified as BS +import Data.Map qualified as Map +import Data.Set qualified as Set + +import Booster.Definition.Attributes.Base +import Booster.Definition.Base +import Booster.Pattern.Base + +benchmarkSizes :: [Int] +benchmarkSizes = [10, 100, 1000, 5000, 10000, 50000] + +benchmarkKMapDef :: KMapDefinition +benchmarkKMapDef = + KMapDefinition + { symbolNames = + KCollectionSymbolNames + { unitSymbolName = "Lbl'Stop'BenchMap" + , elementSymbolName = "LblBenchMapItem" + , concatSymbolName = "Lbl'Unds'BenchMap'Unds'" + } + , keySortName = "SortBenchMapKey" + , elementSortName = "SortBenchMapItem" + , mapSortName = "SortBenchMap" + } + +benchmarkKListDef :: KListDefinition +benchmarkKListDef = + KListDefinition + { symbolNames = + KCollectionSymbolNames + { unitSymbolName = "Lbl'Stop'BenchList" + , elementSymbolName = "LblBenchListItem" + , concatSymbolName = "Lbl'Unds'BenchList'Unds'" + } + , elementSortName = "SortBenchListItem" + , listSortName = "SortBenchList" + } + +benchmarkKSetDef :: KSetDefinition +benchmarkKSetDef = + KListDefinition + { symbolNames = + KCollectionSymbolNames + { unitSymbolName = "Lbl'Stop'BenchSet" + , elementSymbolName = "LblBenchSetItem" + , concatSymbolName = "Lbl'Unds'BenchSet'Unds'" + } + , elementSortName = "SortBenchSetItem" + , listSortName = "SortBenchSet" + } + +mapKeySort, mapValueSort, listElementSort, setElementSort, pipelineSort :: Sort +mapKeySort = SortApp benchmarkKMapDef.keySortName [] +mapValueSort = SortApp benchmarkKMapDef.elementSortName [] +listElementSort = SortApp benchmarkKListDef.elementSortName [] +setElementSort = SortApp benchmarkKSetDef.elementSortName [] +pipelineSort = SortApp "SortBenchTerm" [] + +mkMapKey :: Int -> Term +mkMapKey n = DomainValue mapKeySort (BS.pack ("key-" <> show n)) + +mkMapValue :: Int -> Term +mkMapValue n = DomainValue mapValueSort (BS.pack ("value-" <> show n)) + +mkListElement :: Int -> Term +mkListElement n = DomainValue listElementSort (BS.pack ("list-" <> show n)) + +mkSetElement :: Int -> Term +mkSetElement n = DomainValue setElementSort (BS.pack ("set-" <> show n)) + +mkMapTerm :: Int -> Term +mkMapTerm size = + KMap + benchmarkKMapDef + [ (mkMapKey ix, mkMapValue ix) + | ix <- [1 .. max 0 size] + ] + Nothing + +mkMapWithValueVariables :: Int -> Term +mkMapWithValueVariables size = + KMap + benchmarkKMapDef + [ (mkMapKey ix, Var (valueVariable ix)) + | ix <- [1 .. max 0 size] + ] + Nothing + +mkMapWithKeyVariables :: Int -> Term +mkMapWithKeyVariables size = + KMap + benchmarkKMapDef + [ (Var (keyVariable ix), mkMapValue ix) + | ix <- [1 .. max 0 size] + ] + Nothing + +mkPatternMapForMatch :: Int -> Term +mkPatternMapForMatch size = + KMap + benchmarkKMapDef + [ (mkMapKey ix, Var (matchValueVariable ix)) + | ix <- [1 .. max 0 size] + ] + Nothing + +mkSubjectMapForMatch :: Int -> Term +mkSubjectMapForMatch = mkMapTerm + +mkValueSubstitution :: Int -> Substitution +mkValueSubstitution size = + Map.fromList + [ (valueVariable ix, mkUpdatedValue (size + ix)) + | ix <- [1 .. max 0 size] + ] + +mkKeySubstitution :: Int -> Substitution +mkKeySubstitution size = + Map.fromList + [ (keyVariable ix, mkMapKey (size + ix)) + | ix <- [1 .. max 0 size] + ] + +mkLookupExistingKey :: Int -> Term +mkLookupExistingKey size = mkMapKey (max 1 (size `div` 2)) + +mkLookupMissingKey :: Int -> Term +mkLookupMissingKey size = + DomainValue mapKeySort (BS.pack ("missing-" <> show (max 0 size))) + +mkInsertKey :: Int -> Term +mkInsertKey size = + DomainValue mapKeySort (BS.pack ("insert-" <> show (max 0 size))) + +mkUpdatedValue :: Int -> Term +mkUpdatedValue size = + DomainValue mapValueSort (BS.pack ("updated-" <> show (max 0 size))) + +mkListTerm :: Int -> Term +mkListTerm size = + KList + benchmarkKListDef + [ mkListElement ix + | ix <- [1 .. max 0 size] + ] + Nothing + +mkListConcatRhs :: Int -> Term +mkListConcatRhs size = + let safe = max 0 size + in KList + benchmarkKListDef + [ mkListElement ix + | ix <- [safe + 1 .. (2 * safe)] + ] + Nothing + +mkSetTerm :: Int -> Term +mkSetTerm size = + KSet + benchmarkKSetDef + [ mkSetElement ix + | ix <- [1 .. max 0 size] + ] + Nothing + +pipelineVariable :: Variable +pipelineVariable = + Variable + { variableSort = pipelineSort + , variableName = "PIPELINE_X" + } + +pipelinePatternTerm :: Term +pipelinePatternTerm = + SymbolApplication benchConstructorSymbol [] [Var pipelineVariable] + +pipelineSubjectTerm :: Term +pipelineSubjectTerm = + SymbolApplication + benchConstructorSymbol + [] + [DomainValue pipelineSort "subject"] + +pipelineRhsTerm :: Term +pipelineRhsTerm = + SymbolApplication benchFunctionSymbol [] [Var pipelineVariable] + +benchmarkDefinition :: KoreDefinition +benchmarkDefinition = + (emptyKoreDefinition defaultDefAttributes) + { modules = Map.singleton "BENCH" ModuleAttributes + , sorts = Map.fromList (map mkSortDecl allSortNames) + , symbols = + Map.fromList + [ (benchConstructorSymbol.name, benchConstructorSymbol) + , (benchFunctionSymbol.name, benchFunctionSymbol) + ] + } + where + allSortNames = + [ benchmarkKMapDef.keySortName + , benchmarkKMapDef.elementSortName + , benchmarkKMapDef.mapSortName + , benchmarkKListDef.elementSortName + , benchmarkKListDef.listSortName + , benchmarkKSetDef.elementSortName + , benchmarkKSetDef.listSortName + , "SortInt" + , "SortBool" + , "SortBenchTerm" + ] + +mkSortDecl :: SortName -> (SortName, (SortAttributes, Set.Set SortName)) +mkSortDecl sortName = + ( sortName + , ( SortAttributes + { argCount = 0 + , collectionAttributes = Nothing + } + , Set.singleton sortName + ) + ) + +mkSymbolAttributes :: SymbolType -> SymbolAttributes +mkSymbolAttributes symbolType = + SymbolAttributes + { symbolType + , isIdem = IsNotIdem + , isAssoc = IsNotAssoc + , isMacroOrAlias = IsNotMacroOrAlias + , hasEvaluators = CanBeEvaluated + , collectionMetadata = Nothing + , smt = Nothing + , hook = Nothing + } + +benchConstructorSymbol :: Symbol +benchConstructorSymbol = + Symbol + { name = "benchCon" + , sortVars = [] + , argSorts = [pipelineSort] + , resultSort = pipelineSort + , attributes = mkSymbolAttributes Constructor + } + +benchFunctionSymbol :: Symbol +benchFunctionSymbol = + Symbol + { name = "benchFn" + , sortVars = [] + , argSorts = [pipelineSort] + , resultSort = pipelineSort + , attributes = mkSymbolAttributes (Function Total) + } + +valueVariable :: Int -> Variable +valueVariable ix = + Variable + { variableSort = mapValueSort + , variableName = BS.pack ("V" <> show ix) + } + +keyVariable :: Int -> Variable +keyVariable ix = + Variable + { variableSort = mapKeySort + , variableName = BS.pack ("K" <> show ix) + } + +matchValueVariable :: Int -> Variable +matchValueVariable ix = + Variable + { variableSort = mapValueSort + , variableName = BS.pack ("MV" <> show ix) + } + +validateKMap :: Term -> Bool +validateKMap (KMap def keyVals Nothing) = + def == benchmarkKMapDef + && hasUniqueKeys keyVals +validateKMap _ = False + +validateKSet :: Term -> Bool +validateKSet (KSet def elements Nothing) = + def == benchmarkKSetDef + && elements == sortAndDeduplicate elements +validateKSet _ = False + +validateKList :: Term -> Bool +validateKList (KList def _ Nothing) = def == benchmarkKListDef +validateKList _ = False + +hasUniqueKeys :: [(Term, Term)] -> Bool +hasUniqueKeys keyVals = + let keys = map fst keyVals + in length keys == Set.size (Set.fromList keys) diff --git a/booster/library/Booster/Benchmark/Ops.hs b/booster/library/Booster/Benchmark/Ops.hs new file mode 100644 index 0000000000..6314bf0167 --- /dev/null +++ b/booster/library/Booster/Benchmark/Ops.hs @@ -0,0 +1,167 @@ +{-# LANGUAGE OverloadedRecordDot #-} +{-# LANGUAGE PatternSynonyms #-} + +{- | +Copyright : (c) Runtime Verification, 2026 +License : BSD-3-Clause + +Benchmark operations layered on top of existing booster implementation paths. +-} +module Booster.Benchmark.Ops ( + runMapLookup, + runMapUpdate, + runMapRemove, + runMapInKeys, + runMapKeys, + runMapValues, + runMapSize, + runListGet, + runListSize, + runListRange, + runListConcat, + ksetIn, + ksetSize, + ksetDifference, + ksetUnion, + ksetIntersection, + matchMapTerms, + compareTermHashFirst, + substituteMap, + runPipelineOnce, +) where + +import Control.Monad.Logger (runNoLoggingT) +import Control.Monad.Trans.Except (runExcept) +import Data.ByteString (ByteString) +import Data.Map qualified as Map +import Data.Set qualified as Set +import Data.Text (Text) +import Data.Text qualified as Text + +import Booster.Benchmark.Data +import Booster.Builtin qualified as Builtin +import Booster.Builtin.INT (intTerm) +import Booster.Pattern.ApplyEquations (Direction (TopDown), evaluateTerm) +import Booster.Pattern.Base +import Booster.Pattern.Match (MatchResult (..), MatchType (Rewrite), matchTerms) +import Booster.Pattern.Substitution (substituteInTerm) +import Booster.SMT.Interface (noSolver) +import Booster.Syntax.Json.Externalise (externaliseTerm) +import Booster.Syntax.Json.Internalise ( + internaliseTerm, + pattern DisallowAlias, + pattern IgnoreSubsorts, + ) + +runMapLookup :: Term -> Term -> Either Text (Maybe Term) +runMapLookup mapTerm key = runHook "MAP.lookup" [mapTerm, key] + +runMapUpdate :: Term -> Term -> Term -> Either Text (Maybe Term) +runMapUpdate mapTerm key value = runHook "MAP.update" [mapTerm, key, value] + +runMapRemove :: Term -> Term -> Either Text (Maybe Term) +runMapRemove mapTerm key = runHook "MAP.remove" [mapTerm, key] + +runMapInKeys :: Term -> Term -> Either Text (Maybe Term) +runMapInKeys mapTerm key = runHook "MAP.in_keys" [key, mapTerm] + +runMapKeys :: Term -> Either Text (Maybe Term) +runMapKeys mapTerm = runHook "MAP.keys_list" [mapTerm] + +runMapValues :: Term -> Either Text (Maybe Term) +runMapValues mapTerm = runHook "MAP.values" [mapTerm] + +runMapSize :: Term -> Either Text (Maybe Term) +runMapSize mapTerm = runHook "MAP.size" [mapTerm] + +runListGet :: Term -> Int -> Either Text (Maybe Term) +runListGet listTerm idx = runHook "LIST.get" [listTerm, intTerm (fromIntegral idx)] + +runListSize :: Term -> Either Text (Maybe Term) +runListSize listTerm = runHook "LIST.size" [listTerm] + +runListRange :: Term -> Int -> Int -> Either Text (Maybe Term) +runListRange listTerm front back = + runHook + "LIST.range" + [ listTerm + , intTerm (fromIntegral front) + , intTerm (fromIntegral back) + ] + +runListConcat :: Term -> Term -> Either Text (Maybe Term) +runListConcat left right = runHook "LIST.concat" [left, right] + +ksetIn :: Term -> Term -> Bool +ksetIn element (KSet _ elements Nothing) = element `elem` elements +ksetIn _ _ = False + +ksetSize :: Term -> Int +ksetSize (KSet _ elements Nothing) = length elements +ksetSize _ = 0 + +ksetDifference :: Term -> Term -> Term +ksetDifference left right = + case (left, right) of + (KSet def leftElements Nothing, KSet _ rightElements Nothing) -> + KSet def (Set.toList $ Set.fromList leftElements `Set.difference` Set.fromList rightElements) Nothing + _ -> left + +ksetUnion :: Term -> Term -> Term +ksetUnion left right = + case (left, right) of + (KSet def leftElements Nothing, KSet _ rightElements Nothing) -> + KSet def (Set.toList $ Set.fromList leftElements `Set.union` Set.fromList rightElements) Nothing + _ -> left + +ksetIntersection :: Term -> Term -> Term +ksetIntersection left right = + case (left, right) of + (KSet def leftElements Nothing, KSet _ rightElements Nothing) -> + KSet def (Set.toList $ Set.fromList leftElements `Set.intersection` Set.fromList rightElements) Nothing + _ -> left + +matchMapTerms :: Term -> Term -> MatchResult +matchMapTerms = matchTerms Rewrite benchmarkDefinition + +compareTermHashFirst :: Term -> Term -> Ordering +compareTermHashFirst left right = + case compare (getAttributes left).hash (getAttributes right).hash of + EQ -> compare left right + ord -> ord + +substituteMap :: Substitution -> Term -> Term +substituteMap = substituteInTerm + +runPipelineOnce :: IO (Either Text Int) +runPipelineOnce = runNoLoggingT $ do + solver <- noSolver + let externalSubject = externaliseTerm pipelineSubjectTerm + case runExcept (internaliseTerm DisallowAlias IgnoreSubsorts Nothing benchmarkDefinition externalSubject) of + Left err -> + pure $ Left ("pipeline internalise failed: " <> Text.pack (show err)) + Right internalisedSubject -> + case matchTerms Rewrite benchmarkDefinition pipelinePatternTerm internalisedSubject of + MatchSuccess substitution -> do + let substituted = substituteInTerm substitution pipelineRhsTerm + (evaluated, _cache) <- + evaluateTerm TopDown benchmarkDefinition Nothing solver mempty mempty substituted + case evaluated of + Left err -> + pure $ Left ("pipeline evaluate failed: " <> Text.pack (show err)) + Right rewritten -> do + let externalised = externaliseTerm rewritten + pure $ Right (length (show externalised)) + other -> + pure $ Left ("pipeline match failed: " <> Text.pack (show other)) + +runHook :: ByteString -> [Term] -> Either Text (Maybe Term) +runHook hookName args = + case Map.lookup hookName Builtin.hooks of + Nothing -> + Left ("missing builtin hook: " <> Text.pack (show hookName)) + Just hook -> + firstError (runExcept (hook args)) + +firstError :: Show e => Either e a -> Either Text a +firstError = either (Left . Text.pack . show) Right diff --git a/booster/package.yaml b/booster/package.yaml index 1e39cbec2b..306032c9e4 100644 --- a/booster/package.yaml +++ b/booster/package.yaml @@ -54,6 +54,13 @@ ghc-options: - -Wpartial-fields - -Wredundant-constraints - -j6 + +flags: + profiling: + description: Enable profiling-friendly build options for benchmark runs. + manual: true + default: false + library: dependencies: - aeson @@ -105,6 +112,11 @@ library: build-tools: - happy - alex + when: + - condition: flag(profiling) + ghc-options: + - -prof + - -fprof-auto executables: kore-rpc-client: @@ -236,3 +248,32 @@ tests: - process - text - transformers + ghc-options: + - -rtsopts + - -threaded + - -with-rtsopts=-N + +benchmarks: + booster-bench: + source-dirs: bench + main: Main.hs + dependencies: + - base + - bytestring + - containers + - deepseq + - hashable + - hs-backend-booster + - monad-logger + - tasty-bench + - text + - transformers + ghc-options: + - -rtsopts + - -threaded + - -with-rtsopts=-N + when: + - condition: flag(profiling) + ghc-options: + - -prof + - -fprof-auto diff --git a/booster/unit-tests/Test/Booster/Benchmarks.hs b/booster/unit-tests/Test/Booster/Benchmarks.hs new file mode 100644 index 0000000000..7d403832d2 --- /dev/null +++ b/booster/unit-tests/Test/Booster/Benchmarks.hs @@ -0,0 +1,140 @@ +{- | +Copyright : (c) Runtime Verification, 2026 +License : BSD-3-Clause +-} +module Test.Booster.Benchmarks ( + test_benchmarks, +) where + +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit + +import Booster.Benchmark.Data +import Booster.Benchmark.Ops +import Booster.Builtin.INT (intTerm) +import Booster.Pattern.Base +import Booster.Pattern.Match (MatchResult (..)) + +test_benchmarks :: TestTree +test_benchmarks = + testGroup + "Benchmark framework" + [ generatorTests + , mapOperationTests + , setOperationTests + , listOperationTests + , pipelineTests + ] + +generatorTests :: TestTree +generatorTests = + testGroup + "Generator validity" + [ testCase "KMap generator produces unique keys" $ do + assertBool "invalid generated KMap" (validateKMap (mkMapTerm 100)) + case mkMapTerm 100 of + KMap _ pairs Nothing -> length pairs @?= 100 + other -> assertFailure $ "expected concrete KMap, got: " <> show other + , testCase "KSet generator produces sorted/de-duplicated elements" $ do + assertBool "invalid generated KSet" (validateKSet (mkSetTerm 100)) + case mkSetTerm 100 of + KSet _ elements Nothing -> length elements @?= 100 + other -> assertFailure $ "expected concrete KSet, got: " <> show other + , testCase "KList generator preserves requested size" $ do + assertBool "invalid generated KList" (validateKList (mkListTerm 100)) + case mkListTerm 100 of + KList _ elements Nothing -> length elements @?= 100 + other -> assertFailure $ "expected concrete KList, got: " <> show other + ] + +mapOperationTests :: TestTree +mapOperationTests = + testGroup + "KMap operations" + [ testCase "lookup finds existing keys and misses unknown keys" $ do + let mapTerm = mkMapTerm 10 + runMapLookup mapTerm (mkMapKey 5) @?= Right (Just (mkMapValue 5)) + runMapLookup mapTerm (mkLookupMissingKey 10) @?= Right Nothing + , testCase "update and insert via MAP.update are observable by lookup" $ do + let mapTerm = mkMapTerm 10 + targetKey = mkMapKey 5 + updatedValue = mkUpdatedValue 10 + insertedKey = mkInsertKey 10 + insertedValue = mkUpdatedValue 11 + + updated <- expectSomeTerm "MAP.update existing key" (runMapUpdate mapTerm targetKey updatedValue) + runMapLookup updated targetKey @?= Right (Just updatedValue) + + inserted <- expectSomeTerm "MAP.update new key" (runMapUpdate mapTerm insertedKey insertedValue) + runMapLookup inserted insertedKey @?= Right (Just insertedValue) + , testCase "remove drops key from map" $ do + let mapTerm = mkMapTerm 10 + targetKey = mkMapKey 3 + removed <- expectSomeTerm "MAP.remove" (runMapRemove mapTerm targetKey) + runMapLookup removed targetKey @?= Right Nothing + , testCase "matchMaps benchmark fixture succeeds" $ do + case matchMapTerms (mkPatternMapForMatch 20) (mkSubjectMapForMatch 20) of + MatchSuccess _ -> pure () + other -> assertFailure $ "expected MatchSuccess, got: " <> show other + ] + +setOperationTests :: TestTree +setOperationTests = + testGroup + "KSet operations" + [ testCase "in and size" $ do + let fullSet = mkSetTerm 10 + assertBool "expected membership" (ksetIn (mkSetElement 3) fullSet) + ksetSize fullSet @?= 10 + , testCase "difference/union/intersection" $ do + let fullSet = mkSetTerm 10 + subset = mkSetTerm 5 + ksetSize (ksetDifference fullSet subset) @?= 5 + ksetSize (ksetUnion fullSet subset) @?= 10 + ksetSize (ksetIntersection fullSet subset) @?= 5 + ] + +listOperationTests :: TestTree +listOperationTests = + testGroup + "KList operations" + [ testCase "get at front/middle/back" $ do + let listTerm = mkListTerm 10 + runListGet listTerm 0 @?= Right (Just (mkListElement 1)) + runListGet listTerm 5 @?= Right (Just (mkListElement 6)) + runListGet listTerm 9 @?= Right (Just (mkListElement 10)) + , testCase "size/range/concat" $ do + let listTerm = mkListTerm 10 + rhs = mkListConcatRhs 10 + runListSize listTerm @?= Right (Just (intTerm 10)) + runListRange listTerm 1 1 + @?= Right + ( Just + (KList benchmarkKListDef (map mkListElement [2 .. 9]) Nothing) + ) + concatenated <- expectSomeTerm "LIST.concat" (runListConcat listTerm rhs) + runListSize concatenated @?= Right (Just (intTerm 20)) + ] + +pipelineTests :: TestTree +pipelineTests = + testGroup + "Pipeline benchmark" + [ testCase "full pipeline executes successfully" $ do + outcome <- runPipelineOnce + case outcome of + Right renderedSize -> + assertBool "expected non-empty externalised output" (renderedSize > 0) + Left err -> + assertFailure ("pipeline failed: " <> show err) + ] + +expectSomeTerm :: Show t => String -> Either t (Maybe Term) -> IO Term +expectSomeTerm label = \case + Right (Just term) -> pure term + Right Nothing -> do + _ <- assertFailure (label <> " returned Nothing") + error (label <> ": unreachable") + Left err -> do + _ <- assertFailure (label <> " returned Left error: " <> show err) + error (label <> ": unreachable") diff --git a/scripts/run-bench-profile.sh b/scripts/run-bench-profile.sh new file mode 100755 index 0000000000..c42eff2763 --- /dev/null +++ b/scripts/run-bench-profile.sh @@ -0,0 +1,78 @@ +#!/usr/bin/env bash +set -euo pipefail + +# Build and run booster benchmarks with profiling options enabled. +# +# Usage: +# scripts/run-bench-profile.sh cpu +# scripts/run-bench-profile.sh heap +# scripts/run-bench-profile.sh cpu --benchmark-options="--csv benchmarks.csv" +# +# Output artifacts: +# cpu mode -> booster-bench.prof +# heap mode -> booster-bench.hp (and related heap profile outputs) + +mode="${1:-cpu}" +if [[ $# -gt 0 ]]; then + shift +fi + +benchmark_options="" +for arg in "$@"; do + case "$arg" in + --benchmark-options=*) + benchmark_options="${arg#*=}" + ;; + *) + echo "Unknown argument: $arg" >&2 + echo "Expected: --benchmark-options=..." >&2 + exit 2 + ;; + esac +done + +case "$mode" in + cpu) + rts_flags=("-p") + ;; + heap) + rts_flags=("-hc") + ;; + *) + echo "Mode must be one of: cpu, heap" >&2 + exit 2 + ;; +esac + +if command -v cabal >/dev/null 2>&1; then + cmd=(cabal bench booster-bench --flags profiling) + if [[ -n "$benchmark_options" ]]; then + cmd+=("--benchmark-options=$benchmark_options") + fi + cmd+=(-- +RTS) + cmd+=("${rts_flags[@]}") + cmd+=(-RTS) +elif command -v stack >/dev/null 2>&1; then + bench_args=() + if [[ -n "$benchmark_options" ]]; then + bench_args+=("$benchmark_options") + fi + bench_args+=(+RTS) + bench_args+=("${rts_flags[@]}") + bench_args+=(-RTS) + + cmd=( + stack bench hs-backend-booster:booster-bench + --profile + --ghc-options "-fexternal-interpreter" + --ba "${bench_args[*]}" + ) +else + echo "Neither cabal nor stack is available in PATH." >&2 + exit 127 +fi + +echo "Running profiling benchmark command:" +printf ' %q' "${cmd[@]}" +printf '\n' +"${cmd[@]}" From b7e14761d1ee54f99a808174ad35dac1d901ab3a Mon Sep 17 00:00:00 2001 From: github-actions Date: Wed, 25 Feb 2026 13:38:09 +0000 Subject: [PATCH 3/3] Format with fourmolu --- booster/bench/Main.hs | 9 ++++++--- booster/library/Booster/Benchmark/Data.hs | 7 ++++--- booster/library/Booster/Benchmark/Ops.hs | 10 ++++++++-- 3 files changed, 18 insertions(+), 8 deletions(-) diff --git a/booster/bench/Main.hs b/booster/bench/Main.hs index 8f4dd8ae24..73810f0594 100644 --- a/booster/bench/Main.hs +++ b/booster/bench/Main.hs @@ -61,7 +61,8 @@ ksetBenchFor size = [ bench "difference" $ nf (\(l, r) -> ksetDifference l r) (leftSet, rightSet) , bench "union" $ nf (\(l, r) -> ksetUnion l r) (leftSet, rightSet) , bench "intersection" $ nf (\(l, r) -> ksetIntersection l r) (leftSet, rightSet) - , bench "sortAndDeduplicate" $ nf (\elements -> KSet benchmarkKSetDef elements Nothing) duplicateElements + , bench "sortAndDeduplicate" $ + nf (\elements -> KSet benchmarkKSetDef elements Nothing) duplicateElements ] in bgroup ("size-" <> show size) @@ -140,6 +141,8 @@ substitutionBenchFor size = changedKeySubst = mkKeySubstitution size in bgroup ("size-" <> show size) - [ bench "unchanged-keys" $ nf (\(subst, term) -> substituteMap subst term) (unchangedKeySubst, unchangedKeyMap) - , bench "changed-keys" $ nf (\(subst, term) -> substituteMap subst term) (changedKeySubst, changedKeyMap) + [ bench "unchanged-keys" $ + nf (\(subst, term) -> substituteMap subst term) (unchangedKeySubst, unchangedKeyMap) + , bench "changed-keys" $ + nf (\(subst, term) -> substituteMap subst term) (changedKeySubst, changedKeyMap) ] diff --git a/booster/library/Booster/Benchmark/Data.hs b/booster/library/Booster/Benchmark/Data.hs index 832211f6c8..0a1ff70843 100644 --- a/booster/library/Booster/Benchmark/Data.hs +++ b/booster/library/Booster/Benchmark/Data.hs @@ -254,12 +254,13 @@ benchmarkDefinition = mkSortDecl :: SortName -> (SortName, (SortAttributes, Set.Set SortName)) mkSortDecl sortName = ( sortName - , ( SortAttributes + , + ( SortAttributes { argCount = 0 , collectionAttributes = Nothing } - , Set.singleton sortName - ) + , Set.singleton sortName + ) ) mkSymbolAttributes :: SymbolType -> SymbolAttributes diff --git a/booster/library/Booster/Benchmark/Ops.hs b/booster/library/Booster/Benchmark/Ops.hs index 6314bf0167..8d211d971c 100644 --- a/booster/library/Booster/Benchmark/Ops.hs +++ b/booster/library/Booster/Benchmark/Ops.hs @@ -104,7 +104,10 @@ ksetDifference :: Term -> Term -> Term ksetDifference left right = case (left, right) of (KSet def leftElements Nothing, KSet _ rightElements Nothing) -> - KSet def (Set.toList $ Set.fromList leftElements `Set.difference` Set.fromList rightElements) Nothing + KSet + def + (Set.toList $ Set.fromList leftElements `Set.difference` Set.fromList rightElements) + Nothing _ -> left ksetUnion :: Term -> Term -> Term @@ -118,7 +121,10 @@ ksetIntersection :: Term -> Term -> Term ksetIntersection left right = case (left, right) of (KSet def leftElements Nothing, KSet _ rightElements Nothing) -> - KSet def (Set.toList $ Set.fromList leftElements `Set.intersection` Set.fromList rightElements) Nothing + KSet + def + (Set.toList $ Set.fromList leftElements `Set.intersection` Set.fromList rightElements) + Nothing _ -> left matchMapTerms :: Term -> Term -> MatchResult