Implement better booster logging #3826
Conversation
goodlyrottenapple
changed the title
| @@ -113,13 +110,12 @@ respond stateVar = | |||
| ] | |||
| Right (pat, substitution, unsupported) -> do | |||
| unless (null unsupported) $ do | |||
| withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ | |||
There was a problem hiding this comment.
I think I have an idea how to avoid duplicating the log message here. As I understand, we only have to have duplicates for warnings. Then we could create a special variant of the logMessage function, say logWarning, which would append [warning] at the tail of the context. We than make a static glob pattern *warning that is enabled by default.
There was a problem hiding this comment.
I love it! Let's get it merged once we've run the performance tests to make sure there are no accidents.
We should update README.md with a rough grammar of these context expressions and an example (just using the one form the PR description).
I've left comment about an idea on how we could recover warning and error-level messages without duplicating them. We can try it out in a follow-up.
|
looks like there might be a bit of a slowdown in kevm:
|
|
5% is OK if this is the information we need. We should check Kontrol as well, make sure it's not any more. |
|
It would be great for Kontrol if you could also include the timestamps of each log entry! Also, from what I see, can some |
|
FWIW, from the PR description it seems that, if a term is simplified multiple times, it gets the same hash/identifier. If it's reasonable, it would be nice to have a way to differentiate the various simplification attempts, perhaps a counter, e.g. instead of |
From the log above, something like |
Yes, I think this is something we can add, however the library we use for logging atm is not well suited for logging with timestamps. I can try to hack something in, but the performance may not be stellar. @jberthold perhaps we should switch to using fast-logger?
Yes, that could be a problem. Would be great if you have a tarball with such configuration for me to try. We could either truncate the log if it is an issue, or one can use |
| (rewriteStep cutLabels terminalLabels pat') | ||
| (withPatternContext pat' $ rewriteStep cutLabels terminalLabels pat') | ||
| >>= \case | ||
| Right (RewriteFinished mlbl uniqueId single, cache) -> do | ||
| whenJust mlbl $ \lbl -> | ||
| emitRewriteTrace $ RewriteSingleStep lbl uniqueId pat' single | ||
| updateCache cache | ||
| incrementCounter | ||
| doSteps False single | ||
| Right (terminal@(RewriteTerminal lbl uniqueId single), _cache) -> do | ||
| Right (terminal@(RewriteTerminal lbl uniqueId single), _cache) -> withPatternContext pat' $ do | ||
| emitRewriteTrace $ RewriteSingleStep lbl uniqueId pat' single |
There was a problem hiding this comment.
(nit) Maybe instead of repeating withPatternContext pat' , we could group the \case under the first one, too?
withPatternContext pat' $ do
result <- rewriteStep cutLabels ...
case result of
Right (RewriteFinished ...) -> do ...
(do-notation to avoid bracketing a humongous case expression)
There was a problem hiding this comment.
that won't work because we don't want to put withPatternContext pat' $ around a recursive call to doSteps. Otherwise we will get a massive chain of [execute][term ...]...[term ...], one [term ...] for each iteration of the loop
|
Maybe the PR description should go into a file in |
| withContext "abort" $ logMessage ("Recursion limit exceeded" :: Text) | ||
| logWarnNS "booster" "Recursion limit exceeded" |
There was a problem hiding this comment.
👍 Good to have this as a new warning.
When I looked at the CI results for this PR I noticed that the new test derived from Petar's issue is emitting a large number of those Recursion limit exceeded
We could point the user to the --equation-max-recursion parameter (assuming the name is stable).
…e diffing the output against the golden file
Combines #3833 and #3831 - in Kore, implement rendering of oneline logs prefixed with the context stack, in the spirit of #3826 - add `--log-format <standard|oneline|json> (default:oneline)` to `kore-rpc-booster`. - to recover the old behaviour of `-l Rewrite` and friends, use `--log-format standard`, i.e. `kore-rpc-booster --log-format standard -l Rewrite` - if any `--log-context` is passed, the log format is effectively override to be `oneline` - in `booster/tools/booster/Server.hs`, construct a log action to be passed to Kore. If no `--log-context` options are passed, then the old `-l RewriteKore` and fields levels still work with `--log-format standard`. If `--log-context` is passed, then the complete set of proxy-compatible Kore log entries is enabled, and the filtering is done using the glob context filter late in the colog pipeline. Things to do in a follow-up: - json logging is inconsistent, both the interface and the implementation: - to get simplification JSON logs from both Booster and Kore, we currently need to give two options: `kore-rpc-booster --log-format json -l SimplifyJson`, which is not ideal. We need to remove `-l SimplifyJson` and forward the log format to Booster instead. - To implement the previous item in a clean way, we actually need to stop emitting the logs at `SimplifyJson` level and instead render the regular log items as json. - file logging is inconsistent. It is currently not possible to redirect Booster's contextual logs into a file. - the performance of context filtering in Kore is likely terrible, since we match the while log message, as a string, against the glob pattern. There is not penalty if the contextual logging is off however. --------- Co-authored-by: github-actions <[email protected]> Co-authored-by: Jost Berthold <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
This PR structured logs which allow us to more easily trace rewriting and simplifications:
To turn on this new logging, pass
--log-context "booster*"to the rpc server. If this produces too much loging, we can filter the logs as they are being emitted via a glob syntax filter. e.g.--log-context "*success"will only log all successful matches/rewrites/simplifications and--log-context "*rewrite*match*success"will only log successful matches with a rewrite rule. Conversely, we can also use--not-log-context "*detail"to supress pretty printing terms/rule locations or--not-log-context "*failure"to hide all failures or a combination, such as--log-context "*success*" --not-log-context "*constraint*" --not-log-context "*simplify*"to log any successes not inside a constraint or simplification context.Logging contexts
[booster]top level context signifying computation in the booster backend.
[kore]will be used as top-level context in the kore backend[execute]/[add-module]/[get-model]top-level (right below
[booster]) contexts corresponding to rpc calls[term <hash>]nested context tying any logs within to a particular term. We use the internal hash of a term and pretty print each new term inside a
[detail]context, e.g.:then we can have e.g.
[simplify]top-level or nested context signfying the simplification phase of the whole configuration, either when a simplify request is received i.e. context
[booster][simplify]or inside the execute request when unification is unclear and the booster attempts to simplify the configuration before re-trying to apply rewrite rules:[rewrite <hash>]/[simplification <hash>]/[function <hash>]signifies we are in a context of attemitng to apply a rewrite/simplification/function rule. The
<hash>used is the rule's unique id, truncated to the first 7 letters. We also emit a nested[detail]context, specifying the rule label/location for convenience:[constraint]nested context, signifying evaluation/simplification of a constraint, usually a
requiresclause of a rule.[match]nested context, for running the matching algorithm. usual logs include:
[failure]/[abort]both nested contexts indicate a failure. roughly speaking,
[failure]is an indicator that a rule does not apply, whereas an[abort]is usually indicative of the booster being unable/unsure about proceeding and often falls back to the old backend, tho this is more complicated in equation application, whereabortsmay be recoverable from. perhaps we need slightly different labels, tho it will be obvious that a failure/abort happened inside a function/simplification application from the preceeding context(s).[success]context used for printing successful match or rewrite. will usually have the following shapes:
rewritten one term into another:
rewritten a subterm inside a term:
succesfully matched:
[smt]nested context for any smt operations
[llvm]log any calls to the llvm simplifier here. usually it will be of the form: