You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Add the option to generate performance flamegraphs (#4138)
Adds the ability for `cargo kani` to optionally output the info needed
for generating flamegraphs of the compiler & driver's performance. When
enabled with the `FLAMEGRAPH` environment variable, it will generate an
output file for the driver and one for each crate in the workspace as
they are compiled. These output files can then be rendered as
flamegraphs to see where Kani is spending most of its execution time.
See [this draft docs
page](https://github.com/AlexanderPortland/kani/blob/flamegraph/docs/src/profiling.md)
for more detailed instructions on how it would be used.
This should help us pinpoint which pieces of the compilation process are
most to blame for our compilation times and focus future efforts to
improve them.
Resolves#4075
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---------
Co-authored-by: Carolyn Zech <carolynzech@gmail.com>
Co-authored-by: Carolyn Zech <cmzech@amazon.com>
To profile Kani's performance at a fine-grained level, we use a tool called [`samply`](https://github.com/mstange/samply) that allows the compiler & driver to periodically record the current stack trace, allowing us to construct flamegraphs of where they are spending most of their time.
4
+
5
+
## Install samply
6
+
First, install `samply` using [the instructions](https://github.com/mstange/samply?tab=readme-ov-file#installation) from their repo. The easier methods include installing a prebuilt binary or installing from crates.io.
7
+
8
+
9
+
## Running Kani for profiling output
10
+
1. First, build Kani from source with `cargo build-dev --profile profiling` to ensure you are getting all release mode optimizations without stripping useful debug info.
11
+
2. Then, you can profile the Kani compiler on a crate of your choice by [exporting Kani to your local PATH](build-from-source.md#adding-kani-to-your-path) and running `FLAMEGRAPH=[OPTION] cargo kani` within the crate.
12
+
13
+
The `FLAMEGRAPH` environment variable can be set to `driver` (to profile the complete `kani-driver` execution) or `compiler` (to profile each time the `kani-compiler` is called).
14
+
15
+
We have to instrument the driver and compiler separately because samply's instrumentation usually cannot handle detecting the subprocess the driver uses to call the compiler.
16
+
17
+
Our default sampling rate is *8000 Hz*, but you can change it yourself in [`session.rs`](../../kani-driver/src/session.rs) for the compiler or the [cargo-kani](../../scripts/cargo-kani) script for the driver.
18
+
19
+
> Note: Specifically when profiling the compiler, ensure you are running `cargo clean` immediately before `cargo kani`, or parts of the workspace may not be recompiled by the Kani compiler.
20
+
21
+
22
+
## Displaying profiling output
23
+
This will create a new `flamegraphs` directory in the crate which will contain a single `driver.json.gz` output file and one `compiler-{crate_name}.json.gz` file for each crate in the workspace. Run `samply load flamegraphs/XXX.json.gz` on any of these to open a local server that will display the file's flamegraph.
24
+
25
+
Once the server has opened, you'll see a display with the list of threads in rows at the top, and a flamegraph for the currently selected thread at the bottom. There is typically only one process when profiling the driver. When profiling the compiler, the process that runs the `kani-compiler` and handles all codegen is usually at the very bottom of the thread window.
26
+
27
+
In the flamegraph view, I've found it very useful to right click on a function of interest and select "focus on subtree only" so that it zooms in and you can more clearly see the callees it uses. This can then be undone with the breadcrumb trail at the top of the flamegraph.
0 commit comments