Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

When printing --time statistics, include all buckets in total times #1409

Merged
merged 2 commits into from
Feb 6, 2025
Merged

When printing --time statistics, include all buckets in total times #1409

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
25effdf
When printing --time statistics, include all buckets in total times
Chris-Hawblitzel Jan 26, 2025
a58f1b7
Merge branch 'main' into total-time
Chris-Hawblitzel Feb 6, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 18 additions & 10 deletions source/rust_verify/src/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -107,14 +107,21 @@ pub fn main() {
let total_time = total_time_1 - total_time_0;

let times_ms_json_data = if verifier.args.time {
fn compute_total(
verifier: &rust_verify::verifier::Verifier,
f: impl Fn(&rust_verify::verifier::BucketStats) -> std::time::Duration,
) -> u128 {
verifier.bucket_stats.iter().map(|(_, v)| f(v)).sum::<std::time::Duration>().as_millis()
}

let mut smt_init_times = verifier
.bucket_stats
.iter()
.filter(|(k, _)| k.function().is_none())
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this filtering that's causing the issue? I admittedly forget why this line is here.
@tjhance @achreto ?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this filtering that's causing the issue? I admittedly forget why this line is here.

It looks to me like the filtering is to split out spinoff_prover functions when reporting per-module statistics, so that they are reported separately from the modules that contain them. This sounds useful to me, since spinoff_prover functions are often expensive functions that you'd want to keep an eye on individually when profiling. I suspect, though, that it wasn't intended for these to be excluded from the total times.

.map(|(k, v)| (k.module(), v.time_smt_init.as_millis()))
.collect::<Vec<_>>();
smt_init_times.sort_by(|(_, a), (_, b)| b.cmp(a));
let total_smt_init: u128 = smt_init_times.iter().map(|(_, v)| v).sum();
let total_smt_init: u128 = compute_total(&verifier, |v| v.time_smt_init);

struct SmtStats {
time_millis: u128,
Expand All @@ -136,7 +143,7 @@ pub fn main() {
})
.collect::<Vec<_>>();
smt_run_stats.sort_by(|(_, a), (_, b)| b.time_millis.cmp(&a.time_millis));
let total_smt_run: u128 = smt_run_stats.iter().map(|(_, v)| v.time_millis).sum();
let total_smt_run: u128 = compute_total(&verifier, |v| v.time_smt_run);
let rlimit_counts: Option<Vec<u64>> =
smt_run_stats.iter().map(|(_, v)| v.rlimit_count).collect();
let total_rlimit_count: Option<u64> =
Expand Down Expand Up @@ -182,7 +189,8 @@ pub fn main() {
})
.collect::<Vec<_>>();
air_times.sort_by(|(_, a), (_, b)| b.cmp(a));
let total_air: u128 = air_times.iter().map(|(_, v)| v).sum();
let total_air: u128 =
compute_total(&verifier, |v| v.time_air - (v.time_smt_init + v.time_smt_run));

let mut verify_times = verifier
.bucket_stats
Expand All @@ -191,7 +199,7 @@ pub fn main() {
.map(|(k, v)| (k.module(), (v.time_verify).as_millis()))
.collect::<Vec<_>>();
verify_times.sort_by(|(_, a), (_, b)| b.cmp(a));
let total_verify: u128 = verify_times.iter().map(|(_, v)| v).sum();
let total_verify: u128 = compute_total(&verifier, |v| v.time_verify);

// Rust time:
let rust_init = stats.time_rustc;
Expand Down Expand Up @@ -342,7 +350,7 @@ pub fn main() {
}
}
println!(
" total air-time: {:>10} ms ({} threads)",
" total air-time: {:>10} ms ({} threads)",
total_air, verifier.num_threads
);
if verifier.args.time_expanded {
Expand All @@ -357,26 +365,26 @@ pub fn main() {
}
if !verifier.encountered_vir_error {
println!(
" total smt-time: {:>10} ms ({} threads)",
" total smt-time: {:>10} ms ({} threads)",
(total_smt_init + total_smt_run),
verifier.num_threads
);
println!(
" total smt-init: {:>10} ms ({} threads)",
" total smt-init: {:>10} ms ({} threads)",
total_smt_init, verifier.num_threads
);
if verifier.args.time_expanded {
for (i, (m, t)) in smt_init_times.iter().take(3).enumerate() {
println!(
" {}. {:<40} {:>10} ms",
" {}. {:<40} {:>10} ms",
i + 1,
rust_verify::verifier::module_name(m),
t
);
}
}
println!(
" total smt-run: {:>10} ms{} ({} threads)",
" total smt-run: {:>10} ms{} ({} threads)",
total_smt_run,
total_rlimit_count
.map(|rc| format!(", {:>8} rlimit", rc))
Expand All @@ -386,7 +394,7 @@ pub fn main() {
if verifier.args.time_expanded {
for (i, (m, t)) in smt_run_stats.iter().take(3).enumerate() {
println!(
" {}. {:<40} {:>10} ms{}",
" {}. {:<40} {:>10} ms{}",
i + 1,
rust_verify::verifier::module_name(m),
t.time_millis,
Expand Down