Profiling

Kore profiling

Kore profiling produces a report of time spent in various stages of execution at the Kore level. Run the backend with the -l RTS option:

env GHCRTS='-l' kprove ...

This option will produce a file named kore-exec.eventlog in the current directory. Use the -ol RTS option to change the output filename:

env GHCRTS='-l -olsome-other-name.eventlog' kprove ...

The eventlog file must be digested with kore-prof to produce a profile:

kore-prof kore-exec.eventlog >kore-exec.json

The resulting profile is suitable for speedscope. If the profile is very large, speedscope may be slow. We can filter the profile entries with --matching and --not-matching:

# Show only entries containing the string ":transit",
# i.e. top-level transitions in the proof.
kore-prof kore-exec.eventlog --matching ':transit' >kore-exec.json

# Hide entries containing the string "computeValidJump".
kore-prof kore-exec.eventlog --not-matching 'computeValidJump' >kore-exec.json

In practice, speedscope can handle profiles up to several hundred megabytes if there are no deep recursive function calls.

Haskell profiling

Haskell profiling produces a report of time and allocation in Haskell functions. There is a performance penalty; expect the profiled program to run 3x longer. The report is very detailed, but sometimes it is too detailed to be useful. Haskell profiling does not require extra tools.

These instructions require you to build the backend separately from the K frontend. Clone kframework/kore and build with profiling:

stack build --profile --copy-bins

The profiling-enabled executables will be copied to .build/kore/bin, which you should put on your PATH. Use the GHCRTS environment variable to set flags for the GHC runtime system, for example,

# Run krun with detailed profiling
env GHCRTS='-P' krun ...

Remember that krun will look in its own installation directory for kore-exec before it looks on PATH, so your K frontend build should not include the Haskell backend. The profiling report will be written to the file kore-exec.prof; the report will be overwritten by subsequent runs. You can use the timeout command to limit run time, but send the INT signal so that the GHC RTS has time to write the report before it exits:

timeout -s INT 10m env GHCRTS='-P' krun ...

The report is useful on its own, but there are some tools available to present different views:

• profiteur: Browser-based interactive viewer
• profiterole: Different tabular summaries