-
Notifications
You must be signed in to change notification settings - Fork 42
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
Kore profiling produces a report of time spent in Kore functions. It is often more useful for debugging performance, but it requires extra tools. There is also a performance penalty.
Build the backend with event logging enabled:
stack build --ghc-options "-eventlog -debug" --copy-bins
Again, the 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 event logging
env GHCRTS='-lu' krun ...
As above, use timeout -s INT
to set a time-out if desired.
ghc-events-analyze will be required to analyze the result:
git clone https://github.com/well-typed/ghc-events-analyze
cd ghc-events-analyze
# Requires the cabal-install tool and GHC 8.2.2
cabal v2-install ghc-events-analyze
Running ghc-events-analyze kore-exec.eventlog
produces
a textual summary of time spent in different Kore functions
and a graphical report (SVG) showing at any time which Kore functions were evaluating.