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.

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

Fix issues and Update toolchain 10-26 #2843

Merged
merged 5 commits into from
Oct 31, 2023

Conversation

jaisnan
Copy link
Contributor

@jaisnan jaisnan commented Oct 27, 2023

Resolves issues caused by

  1. rename Generator to Coroutine rust-lang/rust#116958
  2. Rollup of 6 pull requests rust-lang/rust#117103

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

@jaisnan jaisnan requested a review from a team as a code owner October 27, 2023 19:06
@jaisnan jaisnan added the Z-BenchCI Tag a PR to run benchmark CI label Oct 27, 2023
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

Looks good! Thanks Jai

@adpaco-aws
Copy link
Contributor

Despite this looking like a simple renaming, there is a performance regression in the hashset/check_insert_two_concrete benchmark. Comparing runs with the latest run in main:

This PR Latest in main Difference
number_program_steps 33199 28927 +4272
number_vccs 3310 2859 +451
solver_runtime 48.81328 12.15361 +301.636%
symex_runtime 31.2295 28.7472 +8.635%
verification_time 88.96327 48.72418 +82.585%

@zhassan-aws @tautschnig have you seen this benchmark fail lately? Do you have any suggestions?

@jaisnan
Copy link
Contributor Author

jaisnan commented Oct 30, 2023

@adpaco-aws, the second issue rust-lang/rust#117103 required very minor refactoring, which is contained in this commit dce6524. It's possible that this could be causing the performance regression.

@celinval
Copy link
Contributor

Hi @jaisnan, can you compare the MIR emitted before and after the toolchain upgrade (Instruction here)?

My guess is that the performance impact doesn't have anything to do with the conflict resolutions but more with an underlying change to the compiler.

@jaisnan
Copy link
Contributor Author

jaisnan commented Oct 31, 2023

I ran kani on the check_insert_two_concrete example with the command RUSTFLAGS="--emit mir" /home/ubuntu/kani/scripts/kani src/lib.rs --harness check_insert_two_concrete before and after the toolchain update.

My findings were:

  1. There is no difference in the MIRs generated by Kani in the two cases. I used diff to compare the two files and found no difference in the two MIRs.
  2. However, the symtabs for the two cases have a pretty big difference. The symtab for the case after the update is larger.
  3. Even locally, the performance seems to have regressed.

Before:

---snip---
Check 2220: std::ptr::swap_nonoverlapping_simple_untyped::<u8>.unwind.0
	 - Status: SUCCESS
	 - Description: "unwinding assertion loop 0"
	 - Location: ../../../../.rustup/toolchains/nightly-2023-10-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:977:5 in function std::ptr::swap_nonoverlapping_simple_untyped::<u8>

SUMMARY:
 ** 0 of 2221 failed (73 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 39.018295s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.

After:

---snip---
Check 2315: std::ptr::swap_nonoverlapping_simple_untyped::<u8>.unwind.0
	 - Status: SUCCESS
	 - Description: "unwinding assertion loop 0"
	 - Location: ../../../../.rustup/toolchains/nightly-2023-10-26-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:977:5 in function std::ptr::swap_nonoverlapping_simple_untyped::<u8>

SUMMARY:
 ** 0 of 2316 failed (76 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 53.54866s

@adpaco-aws
Copy link
Contributor

We agreed to merge the PR and continue the investigation in a separate issue. @jaisnan do you mind opening that?

@adpaco-aws adpaco-aws merged commit d230735 into model-checking:main Oct 31, 2023
19 of 20 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants