Report CBMC verification time #1247

zhassan-aws · 2022-06-01T23:08:56Z

Description of changes:

Currently, there is no easy way to determine the time spent in the verification step (CBMC). What I typically do is to run kani or cargo kani with /usr/bin/time -p, but the reported time includes the time spent in compilation, codegen, verification, and processing of CBMC output. This PR adds reporting of the elapsed time for the verification step, which is needed when doing performance comparisons. The output looks like this:

SUMMARY: 
 ** 0 of 811 failed (20 unreachable)

VERIFICATION:- SUCCESSFUL


Verification Time: 3.579173s

Resolved issues:

Call-outs:

Testing:

How is this change tested? Added one test
Is this a refactor change? No

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

adpaco-aws · 2022-06-02T18:46:13Z

CBMC reports runtimes for different processes (SSA conversion, solver, etc.), including decision procedure. Is that not good for some reason?

jaisnan · 2022-06-02T18:46:38Z

kani-driver/src/call_cbmc.rs

            let _cbmc_result = self.run_redirect(cmd, &output_filename)?;
+            let elapsed = now.elapsed().as_secs_f32();


Are there any possible scenarios where there might be no time captured in the variable elapsed?

Can't think of a scenario.

kani-driver/src/call_cbmc.rs

jaisnan · 2022-06-02T18:47:12Z

kani-driver/src/call_cbmc.rs

@@ -51,6 +54,7 @@ impl KaniSession {
                // the best possible fix is port to rust instead of using python, or getting more
                // feedback than just exit status (or using a particular magic exit code?)
            }
+            println!("Verification Time: {}s", elapsed);


In case of non-termination, this would line would never be reached right?

Yes, and also in case CBMC exited with an error.

jaisnan · 2022-06-02T18:47:12Z

kani-driver/src/call_cbmc.rs

@@ -51,6 +54,7 @@ impl KaniSession {
                // the best possible fix is port to rust instead of using python, or getting more
                // feedback than just exit status (or using a particular magic exit code?)
            }
+            println!("Verification Time: {}s", elapsed);


In case of non-termination, this would line would never be reached right?

danielsn · 2022-06-02T18:50:22Z

kani-driver/src/call_cbmc.rs

            let _cbmc_result = self.run_redirect(cmd, &output_filename)?;
+            let elapsed = now.elapsed().as_secs_f32();


What's the alternative you have in mind? Is it f64? If so, we probably don't need that much precision, but probably won't hurt much either.

danielsn · 2022-06-02T18:51:00Z

tests/expected/report/verification-time/main.rs

+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that the time spent in CBMC is reported as "Verification time: <>s"


The actual check is just that there is a line that says Verification Time:, correct?

Yes. I'll clarify the comment a bit.

zhassan-aws · 2022-06-02T21:20:13Z

CBMC reports runtimes for different processes (SSA conversion, solver, etc.), including decision procedure. Is that not good for some reason?

Yes, there is no report of the overall CBMC runtime (which is necessary for performance comparisons). If I add up all the runtimes reported by CBMC on one example:

$ grep Runtime cbmc.log 
Runtime Symex: 0.289264s
Runtime Postprocess Equation: 0.00119202s
Runtime Convert SSA: 0.0894082s
Runtime Post-process: 0.00223362s
Runtime Solver: 0.0984715s
Runtime decision procedure: 0.188598s

they add up to less than 1 second, whereas the total CBMC runtime reported by the new line I added is more than 3 seconds:

Verification Time: 3.548905s

tedinski · 2022-06-02T21:32:26Z

they add up to less than 1 second, whereas the total CBMC runtime

Heh. I wonder if we can get CBMC to add a feature that reports start/end timestamps instead of time.

It'd be nice to create the kind of trace diagrams that cargo build --timings gives.

zhassan-aws · 2022-06-06T22:39:40Z

Heh. I wonder if we can get CBMC to add a feature that reports start/end timestamps instead of time.

It'd be nice to create the kind of trace diagrams that cargo build --timings gives.

That would be neat. I didn't know about --timings, but it would be a useful addition.

Report CBMC verification time

84bdba1

zhassan-aws requested a review from a team as a code owner June 1, 2022 23:08

jaisnan reviewed Jun 2, 2022

View reviewed changes

kani-driver/src/call_cbmc.rs Show resolved Hide resolved

jaisnan reviewed Jun 2, 2022

View reviewed changes

danielsn reviewed Jun 2, 2022

View reviewed changes

zhassan-aws added 2 commits June 2, 2022 14:28

Clarify comment in test

0ab5127

Merge branch 'main' into measure-cbmc-time

cdff7e5

adpaco-aws approved these changes Jun 8, 2022

View reviewed changes

danielsn approved these changes Jun 8, 2022

View reviewed changes

zhassan-aws and others added 2 commits June 8, 2022 11:29

Merge branch 'main' into measure-cbmc-time

8982a6d

Merge branch 'main' into measure-cbmc-time

d0408a6

zhassan-aws merged commit adebe36 into model-checking:main Jun 8, 2022

zhassan-aws deleted the measure-cbmc-time branch June 8, 2022 19:23

zhassan-aws mentioned this pull request Sep 13, 2022

Report memory usage for verification step #1675

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Report CBMC verification time #1247

Report CBMC verification time #1247

zhassan-aws commented Jun 1, 2022

adpaco-aws commented Jun 2, 2022

jaisnan Jun 2, 2022

zhassan-aws Jun 2, 2022

jaisnan Jun 2, 2022

zhassan-aws Jun 2, 2022

jaisnan Jun 2, 2022

danielsn Jun 2, 2022

zhassan-aws Jun 2, 2022

danielsn Jun 2, 2022

zhassan-aws Jun 2, 2022

zhassan-aws commented Jun 2, 2022

tedinski commented Jun 2, 2022

zhassan-aws commented Jun 6, 2022

		let _cbmc_result = self.run_redirect(cmd, &output_filename)?;
		let elapsed = now.elapsed().as_secs_f32();

Report CBMC verification time #1247

Report CBMC verification time #1247

Conversation

zhassan-aws commented Jun 1, 2022

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

adpaco-aws commented Jun 2, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

zhassan-aws commented Jun 2, 2022

tedinski commented Jun 2, 2022

zhassan-aws commented Jun 6, 2022