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

Upgrade to 2024-01-08 rust toolchain #2969

Merged
merged 2 commits into from
Jan 8, 2024

Conversation

zhassan-aws
Copy link
Contributor

@zhassan-aws zhassan-aws commented Jan 8, 2024

Relevant PRs:

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

@zhassan-aws zhassan-aws requested a review from a team as a code owner January 8, 2024 17:53
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Jan 8, 2024
@adpaco-aws
Copy link
Contributor

Thanks for doing this, @zhassan-aws ! Do you have any remarks on the regression we saw in #2962? It looks like the change in program steps and VCCs is still there but it doesn't affect solving time in the latest CI run.

@zhassan-aws
Copy link
Contributor Author

zhassan-aws commented Jan 8, 2024

The failure in the benchcomp run is due to an increase in the solver runtime for s2n-quic/quic/s2n-quic-core/sync::spsc::tests::alloc_test from 27 to 42 seconds (~55% increase). However, this increase only results in a 39% increase in the overall verification time (from 40 to 56 seconds), which is within our 50% threshold.

@zhassan-aws
Copy link
Contributor Author

Thanks for doing this, @zhassan-aws ! Do you have any remarks on the regression we saw in #2962? It looks like the change in program steps and VCCs is still there but it doesn't affect solving time in the latest CI run.

Interestingly, the failure we were seeing in recovery::rtt_estimator::test::weighted_average_test with the previous PR (#2962) is no longer occurring. In fact, verification time improved by ~5% for this test (down from 104 seconds to 98).

Copy link
Contributor

@adpaco-aws adpaco-aws left a comment

Choose a reason for hiding this comment

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

Interestingly, the failure we were seeing in recovery::rtt_estimator::test::weighted_average_test with the previous PR (#2962) is no longer occurring.

That's great! In that case, I'm fine with merging this update before it becomes more troublesome.

@zhassan-aws zhassan-aws merged commit 2d23f1a into model-checking:main Jan 8, 2024
19 of 20 checks passed
@zhassan-aws zhassan-aws deleted the toolchain-2024-01-08 branch January 8, 2024 21:16
zhassan-aws added a commit that referenced this pull request Jan 9, 2024
These are the auto-generated release notes for comparison purposes:

## What's Changed
* Automate cargo update without dependabot by @tautschnig in
#2942
* Update nightly toolchain to toolchain-2023-12-15 by @celinval in
#2948
* Automatic cargo update to 2023-12-18 by @github-actions in
#2951
* Migrate function, block and statement modules to StableMIR by
@celinval in #2947
* Update Rust toolchain to `nightly-2023-12-18` by @adpaco-aws in
#2953
* Update the rust toolchain to 2023-12-20 by @celinval in
#2961
* Migrate foreign function, compiler-interface and kani-middle modules
to use StableMIR by @celinval in
#2959
* Build CBMC with `cmake` in all "CBMC latest" jobs by @adpaco-aws in
#2965
* Automatic cargo update to 2024-01-01 by @github-actions in
#2964
* Automatic cargo update to 2024-01-08 by @github-actions in
#2968
* Upgrade to 2024-01-08 rust toolchain by @zhassan-aws in
#2969


**Full Changelog**:
kani-0.43.0...kani-0.44.0

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: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
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