Skip to content

Profiteur timing visualisation #3951

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 17 commits into from
Jun 24, 2024
Merged

Profiteur timing visualisation #3951

Show file tree
Hide file tree
Changes from 15 commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
91c4410
initial commit
goodlyrottenapple Jun 18, 2024
b33b5f3
Add request id into logs
goodlyrottenapple Jun 20, 2024
adb6edd
Add omments
goodlyrottenapple Jun 20, 2024
8da0b3b
merge master
goodlyrottenapple Jun 20, 2024
f632743
Format with fourmolu
invalid-email-address Jun 20, 2024
f963c06
Merge branch 'master' into sam/profiteur-timing
goodlyrottenapple Jun 21, 2024
fb616af
update docs
goodlyrottenapple Jun 21, 2024
39737e9
minor fixes
goodlyrottenapple Jun 21, 2024
967a74b
fix kore-rpc-dev & tweak context log types
goodlyrottenapple Jun 21, 2024
94c74ca
update golden test
goodlyrottenapple Jun 21, 2024
816c388
remove --print-stats
goodlyrottenapple Jun 21, 2024
d0a2df4
remove unused pragma
goodlyrottenapple Jun 21, 2024
0b85265
Format with fourmolu
invalid-email-address Jun 21, 2024
de1a64e
fix formatting
goodlyrottenapple Jun 21, 2024
83eab8a
Merge branch 'master' into sam/profiteur-timing
goodlyrottenapple Jun 21, 2024
5ad2745
tweak log level names for the new timing data
goodlyrottenapple Jun 24, 2024
9a2f0de
Merge remote-tracking branch 'origin/master' into sam/profiteur-timing
goodlyrottenapple Jun 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 28 additions & 11 deletions booster/library/Booster/CLOptions.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -236,6 +236,8 @@ allowedLogLevels =
( "EquationWarnings"
, "Log warnings indicating soft-violations of conditions, i.e. exceeding the equation recursion/iteration limit "
)
, ("Timing", "Logs for timing analysis")
, ("TimingStats", "Formerly --print-stats")
]

levelToContext :: Map Text [ContextFilter]
Expand All @@ -244,49 +246,64 @@ levelToContext =
[
( "Simplify"
,
[ [ctxt| booster|kore>function*|simplification*|hook*,success|failure|abort|detail |]
, [ctxt| booster|kore>function*|simplification*,match,failure|abort |]
[ [ctxt| request*,booster|kore>function*|simplification*|hook*,success|failure|abort|detail |]
, [ctxt| request*,booster|kore>function*|simplification*,match,failure|abort |]
]
)
,
( "SimplifySuccess"
,
[ [ctxt| booster|kore>function*|simplification*|hook*,success|detail |]
[ [ctxt| request*,booster|kore>function*|simplification*|hook*,success|detail |]
]
)
,
( "Rewrite"
,
[ [ctxt| booster|kore>rewrite*,success|failure|abort|detail |]
, [ctxt| booster|kore>rewrite*,match|definedness|constraint,failure|abort |]
[ [ctxt| request*,booster|kore>rewrite*,success|failure|abort|detail |]
, [ctxt| request*,booster|kore>rewrite*,match|definedness|constraint,failure|abort |]
]
)
,
( "RewriteSuccess"
,
[ [ctxt| booster|kore>rewrite*,success|detail |]
[ [ctxt| request*,booster|kore>rewrite*,success|detail |]
]
)
,
( "SMT"
,
[ [ctxt| booster|kore>smt |]
[ [ctxt| request*,booster|kore>smt |]
]
)
,
( "Aborts"
,
[ [ctxt| booster>rewrite*,detail. |]
, [ctxt| booster>rewrite*,match|definedness|constraint,abort. |]
[ [ctxt| request*,booster>rewrite*,detail. |]
, [ctxt| request*,booster>rewrite*,match|definedness|constraint,abort. |]
, [ctxt| proxy. |]
, [ctxt| proxy,abort. |]
, [ctxt| booster>failure,abort |]
, [ctxt| request*,booster>failure,abort |]
]
)
,
( "EquationWarnings"
,
[ [ctxt| booster>(simplification *|function *)>warning |]
[ [ctxt| request*,booster>(simplification *|function *)>warning |]
]
)
,
( "Timing"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This flag could also include what is currently --print-stats (and should get its own context).

Copy link
Contributor Author

@goodlyrottenapple goodlyrottenapple Jun 21, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I decided to remove --print-stats in favour of -l TimingStats as this is more uniform with how we invoke other logging options, but putting this filer in the -l Timing option would IMO be too verbose/unsuitable if we just want the stats but not the success/abort logging needed for the new timing tool

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The code to parse --print-stats was just for backward compatibility. We can scrap it if that's not important.. (not sure who uses it except myself)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BTW run-with-tarball.sh uses --print-stats, maybe adjust that on the same PR

,
[ [ctxt| request*,booster|kore>rewrite*,success|failure|abort|detail |]
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In order to distinguish requests easily, I've added a new request <id> context. @geo2a @jberthold please let me know if this looks ok. If so, will update the docs and the other levelToContext mappings accordingly.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see why you need this ... wanted to suggest adding the ID to the execute, simplify, implies, etc contexts that we already have instead, but that would be inferior and cause issues with the sub-requests we emit.
In the same change, we can also add a CtxStartup and CtxShutdown, Startup grouping the ceil-related messages which are currently info.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I thought we already have a [ceil] context?? do we want [startup][ceil]? what would be the advantage/difference?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

i just noticed we no longer have the ceil context, @jberthold what was the reason for removing it?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As mentioned, the ceil had a double meaning, indicating a ceil rule (with ID) and indicating the ceil analysis phase (which could be included in said startup phase).
I was planning to amend that ceil issue in a follow-up but will wait for your change and what we decide.

, [ctxt| request*,booster|kore>rewrite*,match|definedness|condition,failure|abort |]
, [ctxt| request*,booster|kore>function*|simplification*,success|failure|abort|detail |]
, [ctxt| request*,booster|kore>function*|simplification*,match,failure|abort |]
]
)
,
( "TimingStats"
,
[ [ctxt| *>timing |]
]
)
]
Expand Down
5 changes: 5 additions & 0 deletions booster/library/Booster/Log.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,7 @@ import Data.Maybe (fromMaybe)
import Data.Set qualified as Set
import Data.Text (Text, pack)
import Data.Text.Encoding (decodeUtf8)
import Network.JSONRPC qualified as JSONRPC
import Prettyprinter (Pretty, pretty)
import System.Log.FastLogger (FormattedTime)
import UnliftIO (MonadUnliftIO)
Expand Down Expand Up @@ -222,6 +223,10 @@ instance ContextFor Symbol where
withContextFor s =
withContext_ (CLWithId . CtxHook $ maybe "not-hooked" decodeUtf8 s.attributes.hook)

instance ContextFor (JSONRPC.Id) where
withContextFor r =
withContext_ (CLWithId . CtxRequest $ pack $ JSONRPC.fromId r)

parseRuleId :: RewriteRule tag -> CL.UniqueId
parseRuleId = fromMaybe CL.UNKNOWN . CL.parseUId . coerce . (.attributes.uniqueId)

Expand Down
144 changes: 72 additions & 72 deletions booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden
View file
Open in desktop

Large diffs are not rendered by default.

34 changes: 14 additions & 20 deletions booster/tools/booster/Server.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE QuasiQuotes #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

{- |
Expand Down Expand Up @@ -35,6 +34,7 @@ import Data.Set qualified as Set
import Data.Text (Text)
import Data.Text qualified as Text
import Data.Text.Encoding qualified as Text (decodeUtf8, encodeUtf8)
import Network.JSONRPC qualified as JSONRPC
import Options.Applicative
import System.Clock (
Clock (..),
Expand Down Expand Up @@ -137,8 +137,7 @@ main = do
}
, proxyOptions =
ProxyOptions
{ printStats
, forceFallback
{ forceFallback
, boosterSMT
, fallbackReasons
, simplifyAtEnd
Expand All @@ -149,7 +148,6 @@ main = do
logContextsWithcustomLevelContexts =
logContexts
<> concatMap (\case LevelOther o -> fromMaybe [] $ levelToContext Map.!? o; _ -> []) customLevels
<> [[Ctxt.ctxt| *>timing |] | printStats]
contextLoggingEnabled = not (null logContextsWithcustomLevelContexts)
koreSolverOptions = translateSMTOpts smtOptions
timestampFlag = case timeStampsFormat of
Expand Down Expand Up @@ -312,10 +310,11 @@ main = do
Booster.Log.withContext CtxProxy $
Booster.Log.logMessage' ("Starting RPC server" :: Text)

let koreRespond, boosterRespond :: Respond (API 'Req) (Booster.Log.LoggerT IO) (API 'Res)
koreRespond = Kore.respond kore.serverState (ModuleName kore.mainModule) runSMT
boosterRespond =
Booster.Log.withContext CtxBooster
let koreRespond, boosterRespond :: JSONRPC.Id -> Respond (API 'Req) (Booster.Log.LoggerT IO) (API 'Res)
koreRespond reqId = Kore.respond (fromId reqId) kore.serverState (ModuleName kore.mainModule) runSMT
boosterRespond reqId =
Booster.Log.withContextFor reqId
. Booster.Log.withContext CtxBooster
. Booster.respond boosterState

proxyConfig =
Expand All @@ -332,9 +331,10 @@ main = do
jsonRpcServer
srvSettings
( \rawReq req ->
runBoosterLogger $
logRequestId (fromId $ getReqId rawReq)
>> Proxy.respondEither proxyConfig boosterRespond koreRespond req
let reqId = getReqId rawReq
in runBoosterLogger $
logRequestId reqId
>> Proxy.respondEither proxyConfig (boosterRespond reqId) (koreRespond reqId) req
)
[ Kore.handleDecidePredicateUnknown
, Booster.handleSmtError
Expand Down Expand Up @@ -362,7 +362,7 @@ main = do
Booster.Log.withContext CtxProxy $
Booster.Log.logMessage' $
Text.pack $
"Processing request " <> rid
"Processing request " <> fromId rid

isInterrupt :: AsyncException -> Maybe ()
isInterrupt UserInterrupt = Just ()
Expand Down Expand Up @@ -405,9 +405,7 @@ data CLProxyOptions = CLProxyOptions
}

data ProxyOptions = ProxyOptions
{ printStats :: Bool
-- ^ print timing statistics per request and on shutdown
, forceFallback :: Maybe Depth
{ forceFallback :: Maybe Depth
-- ^ force fallback every n-steps
, boosterSMT :: Bool
-- ^ whether to use an SMT solver in booster code (but keeping kore-rpc's SMT solver)
Expand All @@ -432,11 +430,7 @@ clProxyOptionsParser =
where
parseProxyOptions =
ProxyOptions
<$> switch
( long "print-stats"
<> help "(development) Print timing information per request and on shutdown"
)
<*> optional
<$> optional
( option
(Depth <$> auto)
( metavar "INTERIM_SIMPLIFICATION"
Expand Down
7 changes: 7 additions & 0 deletions cabal.project
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,3 +15,10 @@ source-repository-package
type: git
location: https://github.com/goodlyrottenapple/tasty-test-reporter.git
tag: b704130545aa3925a8487bd3e92f1dd5ce0512e2

source-repository-package
type: git
location: https://github.com/goodlyrottenapple/profiteur.git
tag: 7b30bbe6b2a6b72a5b4896f3a0eed5587a5bf465

constraints: profiteur +embed-data-files
6 changes: 3 additions & 3 deletions dev-tools/kore-rpc-dev/Server.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -233,12 +233,12 @@ main = do
Booster.Log.withContext CtxKore $
Booster.Log.logMessage' ("Starting RPC server" :: Text.Text)

let koreRespond :: Respond (API 'Req) (LoggerT IO) (API 'Res)
koreRespond = Kore.respond kore.serverState (ModuleName kore.mainModule) runSMT
let koreRespond :: Id -> Respond (API 'Req) (LoggerT IO) (API 'Res)
koreRespond reqId = Kore.respond (fromId reqId) kore.serverState (ModuleName kore.mainModule) runSMT
server =
jsonRpcServer
srvSettings
(const $ runBoosterLogger . respond koreRespond)
(\rawReq -> runBoosterLogger . respond (koreRespond $ getReqId rawReq))
[Kore.handleDecidePredicateUnknown, handleErrorCall, handleSomeException]
interruptHandler _ = do
when (logLevel >= LevelInfo) $
Expand Down
17 changes: 17 additions & 0 deletions dev-tools/package.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,23 @@ executables:
- text
ghc-options:
- -rtsopts
time-profile:
source-dirs: time-profile
main: Main.hs
dependencies:
- aeson
- base
- bytestring
- containers
- directory
- filepath
- kore-rpc-types
- profiteur
- text
- unordered-containers
- vector
ghc-options:
- -rtsopts
parsetest-binary:
source-dirs: parsetest-binary
main: ParsetestBinary.hs
Expand Down
59 changes: 59 additions & 0 deletions dev-tools/time-profile/Main.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
{- | Stand-alone parser executable for extracting timing information from JSON context logs

Copyright : (c) Runtime Verification, 2022
License : BSD-3-Clause
-}
module Main (
main,
) where

import Data.Aeson (decode)
import Data.ByteString.Lazy.Char8 qualified as BS
import Data.Maybe (mapMaybe)
import Profiteur
import Profiteur.Main (writeReport)
import System.Environment (getArgs)
import System.IO qualified as IO

{- | Utility for parsing and extracting timing information from context logs,
produced by running the booster binary with `-l Timing --log-format json --log-timestamps --timestamp-format nanosecond`.
This tool collects the timing per each context level and uses the profiteur library to generate an HTML report of the timing information
Call via `timing <path>.log`
-}
main :: IO ()
main =
getArgs >>= \case
files
| "-h" `elem` files || "--help" `elem` files -> do
putStrLn
"This tool parses the JSON contextual logs with timestamps and generates a time profile."
putStrLn "Call via `time-profile <path>.log`"
putStrLn
"To produce the correct context logs, run kore-rpc-booster with `-l Timing --log-format json --log-timestamps --timestamp-format nanosecond`"
[profFile] -> do
logs <- mapMaybe decode . BS.lines <$> BS.readFile profFile

let (timings, ruleMap) = case logs of
m : ms -> collectTiming mempty m ms
[] -> mempty
timing = foldr (((<>)) . fmap (,Count 1) . computeTimes) (TimeMap mempty) timings
htmlFile = profFile ++ ".html"
IO.withBinaryFile htmlFile IO.WriteMode $ \h -> do
-- produce a timing map mirroring the context levels, roughly:
-- main -> request n -> kore|booster -> execute|simplify|implies -> term rid -> rewrite id|simplification id|equation id -> success|failure
writeReport h profFile $ toNodeMap timing ruleMap

let htmlAggregateFile = profFile ++ ".aggregate.html"
IO.withBinaryFile htmlAggregateFile IO.WriteMode $ \h -> do
writeReport h profFile $
-- produce an agregate profile of all the number and total time spent trying each rewrite rule. The structure is:
-- main -> request n -> rewrite id -> kore|booster
toNodeMap (aggregateRewriteRules aggregateRewriteRulesPerRequest timing) ruleMap

let htmlAggregateFile2 = profFile ++ ".aggregate2.html"
IO.withBinaryFile htmlAggregateFile2 IO.WriteMode $ \h -> do
writeReport h profFile $
-- produce an agregate profile of all the number and total time spent trying each rewrite rule. The structure is:
-- main -> request n -> kore|booster -> rewrite id
toNodeMap (aggregateRewriteRules aggregateRewriteRulesPerRequest2 timing) ruleMap
_ -> error "invalid arguments"
Loading
Loading