-
Notifications
You must be signed in to change notification settings - Fork 44
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.
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
Changes from all commits
Commits
Show all changes
17 commits
Select commit
Hold shift + click to select a range
91c4410
initial commit
goodlyrottenapple b33b5f3
Add request id into logs
goodlyrottenapple adb6edd
Add omments
goodlyrottenapple 8da0b3b
merge master
goodlyrottenapple f632743
Format with fourmolu
invalid-email-address f963c06
Merge branch 'master' into sam/profiteur-timing
goodlyrottenapple fb616af
update docs
goodlyrottenapple 39737e9
minor fixes
goodlyrottenapple 967a74b
fix kore-rpc-dev & tweak context log types
goodlyrottenapple 94c74ca
update golden test
goodlyrottenapple 816c388
remove --print-stats
goodlyrottenapple d0a2df4
remove unused pragma
goodlyrottenapple 0b85265
Format with fourmolu
invalid-email-address de1a64e
fix formatting
goodlyrottenapple 83eab8a
Merge branch 'master' into sam/profiteur-timing
goodlyrottenapple 5ad2745
tweak log level names for the new timing data
goodlyrottenapple 9a2f0de
Merge remote-tracking branch 'origin/master' into sam/profiteur-timing
goodlyrottenapple File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
144 changes: 72 additions & 72 deletions
144
booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 TimeProfile --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 TimeProfile --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" |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
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 otherlevelToContextmappings accordingly.There was a problem hiding this comment.
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
CtxStartupandCtxShutdown,Startupgrouping theceil-related messages which are currentlyinfo.There was a problem hiding this comment.
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?There was a problem hiding this comment.
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?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As mentioned, the
ceilhad a double meaning, indicating a ceil rule (with ID) and indicating the ceil analysis phase (which could be included in saidstartupphase).I was planning to amend that
ceilissue in a follow-up but will wait for your change and what we decide.