diff --git a/Cargo.lock b/Cargo.lock index 7e8c27066f3b..095a517289a3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -39,6 +39,21 @@ dependencies = [ "memchr", ] +[[package]] +name = "android-tzdata" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e999941b234f3131b00bc13c22d06e8c5ff726d1b6318ac7eb276997bbb4fef0" + +[[package]] +name = "android_system_properties" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "819e7219dbd41043ac279b19830f2efc897156490d7fd6ea916720117ee66311" +dependencies = [ + "libc", +] + [[package]] name = "annotate-snippets" version = "0.11.5" @@ -190,6 +205,12 @@ dependencies = [ "which", ] +[[package]] +name = "bumpalo" +version = "3.18.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "793db76d6187cd04dff33004d8e6c9cc4e05cd330500379d2394209271b4aeee" + [[package]] name = "byteorder" version = "1.5.0" @@ -303,6 +324,18 @@ dependencies = [ "which", ] +[[package]] +name = "chrono" +version = "0.4.41" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c469d952047f47f91b68d1cba3f10d63c11d73e4636f24f08daf0278abf01c4d" +dependencies = [ + "android-tzdata", + "iana-time-zone", + "num-traits", + "windows-link", +] + [[package]] name = "clap" version = "4.5.39" @@ -408,6 +441,12 @@ dependencies = [ "unicode-segmentation", ] +[[package]] +name = "core-foundation-sys" +version = "0.8.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b" + [[package]] name = "cprover_bindings" version = "0.63.0" @@ -783,6 +822,30 @@ dependencies = [ "windows-sys 0.59.0", ] +[[package]] +name = "iana-time-zone" +version = "0.1.63" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b0c919e5debc312ad217002b8048a17b7d83f80703865bbfcfebb0458b0b27d8" +dependencies = [ + "android_system_properties", + "core-foundation-sys", + "iana-time-zone-haiku", + "js-sys", + "log", + "wasm-bindgen", + "windows-core", +] + +[[package]] +name = "iana-time-zone-haiku" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f31827a206f56af32e590ba56d5d2d085f558508192593743f16b2306495269f" +dependencies = [ + "cc", +] + [[package]] name = "icu_collections" version = "2.0.0" @@ -987,6 +1050,16 @@ version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "72167d68f5fce3b8655487b8038691a3c9984ee769590f93f2a631f4ad64e4f5" +[[package]] +name = "js-sys" +version = "0.3.77" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1cfaf33c695fc6e08064efbc1f72ec937429614f25eef83af942d0e227c3a28f" +dependencies = [ + "once_cell", + "wasm-bindgen", +] + [[package]] name = "kani" version = "0.63.0" @@ -1038,6 +1111,7 @@ version = "0.63.0" dependencies = [ "anyhow", "cargo_metadata", + "chrono", "clap", "comfy-table", "console", @@ -2390,6 +2464,64 @@ dependencies = [ "wit-bindgen-rt", ] +[[package]] +name = "wasm-bindgen" +version = "0.2.100" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1edc8929d7499fc4e8f0be2262a241556cfc54a0bea223790e71446f2aab1ef5" +dependencies = [ + "cfg-if", + "once_cell", + "rustversion", + "wasm-bindgen-macro", +] + +[[package]] +name = "wasm-bindgen-backend" +version = "0.2.100" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2f0a0651a5c2bc21487bde11ee802ccaf4c51935d0d3d42a6101f98161700bc6" +dependencies = [ + "bumpalo", + "log", + "proc-macro2", + "quote", + "syn", + "wasm-bindgen-shared", +] + +[[package]] +name = "wasm-bindgen-macro" +version = "0.2.100" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7fe63fc6d09ed3792bd0897b314f53de8e16568c2b3f7982f468c0bf9bd0b407" +dependencies = [ + "quote", + "wasm-bindgen-macro-support", +] + +[[package]] +name = "wasm-bindgen-macro-support" +version = "0.2.100" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8ae87ea40c9f689fc23f209965b6fb8a99ad69aeeb0231408be24920604395de" +dependencies = [ + "proc-macro2", + "quote", + "syn", + "wasm-bindgen-backend", + "wasm-bindgen-shared", +] + +[[package]] +name = "wasm-bindgen-shared" +version = "0.2.100" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1a05d73b933a847d6cccdda8f838a22ff101ad9bf93e33684f39c1f5f0eece3d" +dependencies = [ + "unicode-ident", +] + [[package]] name = "which" version = "7.0.3" @@ -2433,6 +2565,65 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" +[[package]] +name = "windows-core" +version = "0.61.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c0fdd3ddb90610c7638aa2b3a3ab2904fb9e5cdbecc643ddb3647212781c4ae3" +dependencies = [ + "windows-implement", + "windows-interface", + "windows-link", + "windows-result", + "windows-strings", +] + +[[package]] +name = "windows-implement" +version = "0.60.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a47fddd13af08290e67f4acabf4b459f647552718f683a7b415d290ac744a836" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "windows-interface" +version = "0.59.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bd9211b69f8dcdfa817bfd14bf1c97c9188afa36f4750130fcdf3f400eca9fa8" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "windows-link" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "76840935b766e1b0a05c0066835fb9ec80071d4c09a16f6bd5f7e655e3c14c38" + +[[package]] +name = "windows-result" +version = "0.3.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "56f42bd332cc6c8eac5af113fc0c1fd6a8fd2aa08a0119358686e5160d0586c6" +dependencies = [ + "windows-link", +] + +[[package]] +name = "windows-strings" +version = "0.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "56e6c93f3a0c3b36176cb1327a4958a0353d5d166c2a35cb268ace15e91d3b57" +dependencies = [ + "windows-link", +] + [[package]] name = "windows-sys" version = "0.52.0" diff --git a/Cargo.toml b/Cargo.toml index cfa94e5ce44e..62d572f35a3a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -32,6 +32,12 @@ path = "src/bin/cargo_kani.rs" [profile.release] strip = "debuginfo" +[profile.profiling] +inherits = "release" +debug = true +strip = "none" +lto = "off" + # Below is the workspace (vs above is "kani-verifier" crate) config: [workspace] diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index 7c37e0445314..8f72ffc5c718 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -42,6 +42,7 @@ - [`benchcomp` command line](./benchcomp-cli.md) - [`benchcomp` configuration file](./benchcomp-conf.md) - [Custom parsers](./benchcomp-parse.md) + - [Profiling Kani](./profiling.md) - [Limitations](./limitations.md) - [Undefined behaviour](./undefined-behaviour.md) diff --git a/docs/src/dev-documentation.md b/docs/src/dev-documentation.md index c3fe857cf0b6..39565d6895ba 100644 --- a/docs/src/dev-documentation.md +++ b/docs/src/dev-documentation.md @@ -15,6 +15,7 @@ developers (including external contributors): 4. [Development setup recommendations for working with `rustc`](./rustc-hacks.md). 5. [Guide for testing in Kani](./testing.md). 6. [Transition to StableMIR](./stable-mir.md). + 7. [Profiling Kani's performance](./profiling.md) > **NOTE**: The developer documentation is intended for Kani developers and not users. At present, the project is under heavy development and some items diff --git a/docs/src/profiling.md b/docs/src/profiling.md new file mode 100644 index 000000000000..4ce0f1f6ac1d --- /dev/null +++ b/docs/src/profiling.md @@ -0,0 +1,27 @@ +# Profiling Kani's Performance + +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. + +## Install samply +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. + + +## Running Kani for profiling output +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. +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. + +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). + +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. + +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. + +> 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. + + +## Displaying profiling output +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. + +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. + +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. \ No newline at end of file diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index e3f75f00e063..6ecc2d767739 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -35,6 +35,7 @@ tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt" which = "7" time = {version = "0.3.36", features = ["formatting"]} tokio = { version = "1.40.0", features = ["io-util", "process", "rt", "time"] } +chrono = { version = "0.4.41", default-features = false, features = [ "clock" ]} # A good set of suggested dependencies can be found in rustup: diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index b834dad3c657..9cba9c940979 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -6,6 +6,7 @@ use crate::call_single_file::{LibConfig, to_rustc_arg}; use crate::project::Artifact; use crate::session::{ KaniSession, get_cargo_path, lib_folder, lib_no_core_folder, setup_cargo_command, + setup_cargo_command_inner, }; use crate::util; use anyhow::{Context, Result, bail}; @@ -202,7 +203,8 @@ crate-type = ["lib"] let mut failed_targets = vec![]; for package in packages { for verification_target in package_targets(&self.args, package) { - let mut cmd = setup_cargo_command()?; + let mut cmd = + setup_cargo_command_inner(Some(verification_target.target().name.clone()))?; cmd.args(&cargo_args) .args(vec!["-p", &package.id.to_string()]) .args(verification_target.to_args()) diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 01c475309972..500679d0c733 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -25,6 +25,10 @@ pub const BUG_REPORT_URL: &str = /// the driver logs separately, by using the logger directives to select the kani-driver crate. /// `export KANI_LOG=kani_driver=debug`. const LOG_ENV_VAR: &str = "KANI_LOG"; +// Constants related to the option to create flamegraphs to debug compiler performance. See our mdbook's developer documentation for details. +const FLAMEGRAPH_ENV_VAR: &str = "FLAMEGRAPH"; +const FLAMEGRAPH_DIR: &str = "flamegraphs"; +const FLAMEGRAPH_SAMPLING_RATE: &str = "8000"; // in Hz /// Contains information about the execution environment and arguments that affect operations pub struct KaniSession { @@ -409,18 +413,51 @@ fn init_logger(args: &VerificationArgs) { tracing::subscriber::set_global_default(subscriber).unwrap(); } -// Setup the default version of cargo being run, based on the type/mode of installation for kani -// If kani is being run in developer mode, then we use the one provided by rustup as we can assume that the developer will have rustup installed +pub fn setup_cargo_command() -> Result { + setup_cargo_command_inner(None) +} + +// Setup the default version of cargo being run, based on the type/mode of installation for kani. +// Optionally takes a path to output compiler profiling info to. +// If kani is being run in developer mode, then we use the one provided by rustup as we can assume that the developer will have rustup installed. // For release versions of Kani, we use a version of cargo that's in the toolchain that's been symlinked during `cargo-kani` setup. This will allow // Kani to remove the runtime dependency on rustup later on. -pub fn setup_cargo_command() -> Result { +pub fn setup_cargo_command_inner(profiling_out_path: Option) -> Result { let install_type = InstallType::new()?; let cmd = match install_type { InstallType::DevRepo(_) => { - let mut cmd = Command::new("cargo"); - cmd.arg(self::toolchain_shorthand()); - cmd + // check if we should instrument the compiler for a flamegraph + let instrument_compiler = matches!( + std::env::var(FLAMEGRAPH_ENV_VAR), + Ok(ref s) if s == "compiler" + ); + + if let Some(profiler_out_path) = profiling_out_path + && instrument_compiler + { + // create temporary flamegraph directory + std::fs::create_dir_all(FLAMEGRAPH_DIR)?; + let time_postfix = chrono::Local::now().format("%Y-%m-%dT%H:%M:%S"); + + let mut cmd = Command::new("samply"); + cmd.arg("record"); + + // adjust the sampling rate (in Hz) + cmd.arg("-r").arg(FLAMEGRAPH_SAMPLING_RATE); + cmd.arg("-o").arg(format!( + "{FLAMEGRAPH_DIR}/compiler-{profiler_out_path}-{time_postfix}.json.gz", + )); + + // just save the output and don't open the interactive UI. + cmd.arg("--save-only"); + cmd.arg("cargo").arg(self::toolchain_shorthand()); + cmd + } else { + let mut cmd = Command::new("cargo"); + cmd.arg(self::toolchain_shorthand()); + cmd + } } InstallType::Release(kani_dir) => { let cargo_path = kani_dir.join("toolchain").join("bin").join("cargo"); diff --git a/scripts/cargo-kani b/scripts/cargo-kani index b3f85af666d1..b05d7791f02d 100755 --- a/scripts/cargo-kani +++ b/scripts/cargo-kani @@ -18,4 +18,18 @@ then exit 1 fi -exec -a cargo-kani "${KANI_DRIVER}" "$@" +FLAMEGRAPH_DIR="flamegraphs" +FLAMEGRAPH_SAMPLING_RATE=8000 # in Hz + +FLAMEGRAPH_DRIVER=0 +if [[ ( -n "${FLAMEGRAPH:-}" ) && ( "${FLAMEGRAPH}" == "driver" ) ]]; then + FLAMEGRAPH_DRIVER=1 +fi + +if (( FLAMEGRAPH_DRIVER == 0 )); then + exec -a cargo-kani "${KANI_DRIVER}" "$@" +else + mkdir -p "${FLAMEGRAPH_DIR}" + DATE_POSTFIX=$(date +"%Y-%m-%dT%H:%M:%S") + exec -a cargo-kani samply record -r $FLAMEGRAPH_SAMPLING_RATE -o "${FLAMEGRAPH_DIR}/driver-${DATE_POSTFIX}.json.gz" --save-only "${KANI_DRIVER}" "$@" +fi \ No newline at end of file