Skip to content

Conversation

@jberthold
Copy link
Member

  • include hook <NAME> log contexts in -l Simplify and -l SimplifySuccess
  • log timing statistics with a log context proxy,timing
Example JSON output for `--log-context proxy`
{"context":["proxy"],"message":"Loading definition from resources/log-simplify-json.kore, main module \"IMP-VERIFICATION\""}
{"context":["proxy"],"message":"Starting RPC server"}
{"context":["proxy"],"message":"Processing request 4"}
{"context":["proxy"],"message":"Starting execute request"}
{"context":["proxy"],"message":"Booster Aborted at Depth {getNat = 10}"}
{"context":["proxy"],"message":"Simplifying booster state and falling back to Kore"}
{"context":["proxy"],"message":"Simplifying execution state"}
{"context":["proxy","timing"],"message":{"kore-time":34017.38,"method":"SimplifyM","time":43152.727999999996}}
{"context":["proxy"],"message":"Executing fall-back request"}
{"context":["proxy","timing","kore"],"message":{"kore-time":37633.786,"method":"ExecuteM","time":37633.786}}
{"context":["proxy","abort"],"message":"Booster aborted, kore yields Branching"}
{"context":["proxy"],"message":"Kore Branching at Depth {getNat = 0}"}
{"context":["proxy"],"message":"Simplifying state in Branching result"}
{"context":["proxy"],"message":"Simplifying execution state"}
{"context":["proxy","timing"],"message":{"kore-time":33663.381,"method":"SimplifyM","time":43049.642}}
{"context":["proxy"],"message":"Simplifying execution state"}
{"context":["proxy","timing"],"message":{"kore-time":33558.555,"method":"SimplifyM","time":42640.443}}
{"context":["proxy"],"message":"Simplifying execution state"}
{"context":["proxy","timing"],"message":{"kore-time":34078.823,"method":"SimplifyM","time":43215.810999999994}}
{"context":["proxy","abort","detail"],"message":"Kore simplification: Diff (< before - > after)\n<syntactic difference only>"}
{"context":["proxy","timing"],"message":{"kore-time":37633.786,"method":"ExecuteM","time":51747.152}}
{"context":["proxy"],"message":"Server shutting down"}
{"context":["proxy","timing"],"message":[["ExecuteM",{"average":51747.152,"count":1,"kore-average":37633.786,"kore-max":37633.786,"kore-total":37633.786,"max-val":51747.152,"min-val":51747.152,"stddev":0,"total":51747.152}],["SimplifyM",{"average":43014.655999999995,"count":4,"kore-average":33829.53475,"kore-max":34078.823,"kore-total":135318.139,"max-val":43215.810999999994,"min-val":42640.443,"stddev":224.0460894407471,"total":172058.62399999998}]]}
Example text output: (as before)
[proxy] Processing request 4
[proxy] Starting execute request
[proxy] Booster Aborted at Depth {getNat = 10}
[proxy] Simplifying booster state and falling back to Kore
[proxy] Simplifying execution state
[proxy][timing] Performed SimplifyM in 42.907ms (33.585ms kore time)
[proxy] Executing fall-back request
[proxy][timing][kore] Kore fall-back in 37.303ms
[proxy][abort] Booster aborted, kore yields Branching
[proxy] Kore Branching at Depth {getNat = 0}
[proxy] Simplifying state in Branching result
[proxy] Simplifying execution state
[proxy][timing] Performed SimplifyM in 42.253ms (32.774ms kore time)
[proxy] Simplifying execution state
[proxy][timing] Performed SimplifyM in 41.732ms (32.446ms kore time)
[proxy] Simplifying execution state
[proxy][timing] Performed SimplifyM in 42.379ms (33.301ms kore time)
[proxy][abort][detail] Kore simplification: Diff (< before - > after)
<syntactic difference only>
[proxy][timing] Performed ExecuteM in 50.100ms (37.303ms kore time)
[proxy] Server shutting down
[proxy][timing] ---------------------------
RPC request time statistics
---------------------------
ExecuteM: 
    Requests: 1
    Total time: 50.100ms
    Average time per request: 50.100ms (+- 0.0μs), range [50.100ms, 50.100ms]
    Total time in kore-rpc code: 37.303ms
    Average time per request in kore-rpc code: 37.303ms, max 37.303ms
SimplifyM: 
    Requests: 4
    Total time: 0.17s
    Average time per request: 42.318ms (+- 0.418ms), range [41.732ms, 42.907ms]
    Total time in kore-rpc code: 0.13s
    Average time per request in kore-rpc code: 33.027ms, max 33.585ms

@jberthold jberthold requested review from geo2a and goodlyrottenapple and removed request for goodlyrottenapple June 21, 2024 04:36
echo "arguments=$*"

diff="git diff --no-index"
diff="git --no-pager diff --no-index"
Copy link
Contributor

Choose a reason for hiding this comment

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

👍

@jberthold jberthold marked this pull request as ready for review June 21, 2024 08:03
@rv-jenkins rv-jenkins merged commit ac6c535 into master Jun 21, 2024
@rv-jenkins rv-jenkins deleted the HOTFIX-moah-logging-tweaks branch June 21, 2024 08:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants