Profiling

The guide below details two ways of profiling the time performance of the Haskell backend. The main difference between Kore profiling and Haskell profiling is that Kore profiling does not require the binaries to be recompiled with profiling turned on. As a result, this profile only contains events specifically annotated/captured via traceProf. Haskell profiling, on the other hand requires compiling the Haskell backend with profiling enabled. With profiling enabled, the generated eventlog will contain much more low-level traces linked to Haskell functions.

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, --not-matching and --not-matching-children:

# 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

# Hide the children of entries containing the string "computeValidJump".
kore-prof kore-exec.eventlog --not-matching-children '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 and unlike Kore profiling requires compiling the binaries with profiling enabled. This incurs 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. No extra tools are required to get some basic performance reports but for more extensive profiling tasks, we recommend the use of speedscope, which we detail below:

These instructions require you to build the backend separately from the K frontend. Clone kframework/kore and build with profiling. For best results, we recommend building the backend with Cabal:

cabal v2-configure --enable-profiling -f-threaded
cabal v2-build all
cabal v2-exec -- bash  # Replace 'bash' with your preferred shell.

This will configure the backend with profiling enabled, build the backend tools, and drop you into a shell where PATH points to those tools. At this point, you can change directories and run any commands as you normally would. The settings will persist until you exit the shell, at which time you will be returned to your original shell. If you need to make changes to the backend code, run the "build" and "exec" commands again.

Use the GHCRTS environment variable to set flags for the GHC runtime system, for example,

# Run krun with detailed profiling and dump eventlog
env GHCRTS='-p -l-au' krun ...

The above command will produce in the current directory a report of the completed execution with the extension .eventlog. In order to view this report on speedscope, it needs to be converted to a supported format. To do this, make sure that hs-speedscope is installed (installable via cabal update && cabal install hs-speedscope) and run

hs-speedscope kore-exec.eventlog

where kore-exec.eventlog is the generated report. This will produce a new file with the extension .eventlog.json that can be directly inspected in the browser when pasted into speedscope.

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.

Besides the .eventlog report, the command also produces a profile in the form of a file kore-exec.prof; the report and profile 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 profile before it exits:

timeout -s INT 10m env GHCRTS='-p -l-au' krun ...

The .prof profile can be investigated using the following tools:

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