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 Rust toolchain to nightly-2024-03-01 #3052

Merged

Conversation

adpaco-aws
Copy link
Contributor

Upgrades the Rust toolchain to nightly-2024-03-01. The Rust compiler PRs that triggered changes in this upgrades are:

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 adpaco-aws requested a review from a team as a code owner March 1, 2024 17:17
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Mar 1, 2024
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.

Thanks Adrian!

@celinval celinval changed the title Upgrade Rust toolchain to nightly-2024-01-03 Upgrade Rust toolchain to nightly-2024-03-01 Mar 1, 2024
@celinval
Copy link
Contributor

celinval commented Mar 1, 2024

Please just make sure there's no significant performance degradation before merging.

@adpaco-aws
Copy link
Contributor Author

Unfortunately I'm getting consistent >400% regressions in solver_runtime for s2n-quic/quic/s2n-quic-core/recovery::rtt_estimator::test::weighted_average_test (see this CI run for example). Other values like program steps, VCCs, etc. haven't really changed.

@celinval
Copy link
Contributor

celinval commented Mar 1, 2024

can you manually run before and after the PR to see if that's the case?

@zhassan-aws
Copy link
Contributor

This test is known to have high variance in performance, e.g. see https://github.com/model-checking/kani/actions/runs/7453782015

The numbers in this PR are on par with the numbers in previous PRs, so I would consider this to be noise. You can confirm by running the test locally a number of times with and without the changes.

@adpaco-aws adpaco-aws force-pushed the toolchain-upgrade-2024-01-03 branch from 24419a0 to ca58557 Compare March 4, 2024 18:45
@adpaco-aws
Copy link
Contributor Author

Thanks all for your feedback. I've run each version 10 times and the results are:

iter. before after
1 150.85266 200.95573
2 150.59746 200.90263
3 150.4481 202.78355
4 150.52237 201.8042
5 150.50912 200.75551
6 150.19904 200.7821
7 151.47997 200.9002
8 150.85907 200.75055
9 150.36966 204.47491
10 150.9473 201.89137

So it looks like there's a performance regression of about +50s/+33% for this test.

@adpaco-aws
Copy link
Contributor Author

adpaco-aws commented Mar 4, 2024

After some discussion, we consider that the regression is due to SAT variability.

No data suggests that the problem is more difficult per se after the toolchain upgrade. For example, runtime symex remains constant in all cases (~0.8s), as does program size (16292 steps) and VCCs (615/231).

The table below shows SAT-solving time for the UNSATISFIABLE instance in each of the iterations.

iter. before after
1 146.51s 196.37s
2 146.25s 196.281s
3 146.032s 198.212s
4 146.176s 197.226s
5 146.168s 196.173s
6 145.878s 196.158s
7 147.131s 196.314s
8 146.485s 196.165s
9 146.028s 199.885s
10 146.612s 197.307s

If we compare this with the table posted in my previous comment, we can conclude that the total time increase is due to the increase in SAT-solving time for the UNSATISFIABLE instance. Therefore, there is no reason to block this toolchain upgrade.

@zhassan-aws pointed out that there's almost no difference before/after this toolchain upgrade if we use CaDiCaL instead (the current solver is Kissat). So we'll propose switching the solver to CaDiCaL for this test.

@adpaco-aws adpaco-aws merged commit 12768f2 into model-checking:main Mar 4, 2024
19 of 20 checks passed
zhassan-aws added a commit that referenced this pull request Mar 13, 2024
These are the original release notes for the reference:

## What's Changed
* Automatic cargo update to 2024-02-26 by @github-actions in
#3043
* Upgrade rust toolchain to 2024-02-17 by @celinval in
#3040
* Upgrade `windows-targets` crate to version 0.52.4 by @adpaco-aws in
#3049
* Fix `codegen_atomic_binop` for `atomic_ptr` by @qinheping in
#3047
* Upgrade Rust toolchain to `nightly-2024-02-25` by @adpaco-aws in
#3048
* Update s2n-quic submodule by @zhassan-aws in
#3050
* Update s2n-quic submodule weekly through dependabot by @zhassan-aws in
#3053
* Retrieve info for recursion tracker reliably by @feliperodri in
#3045
* Automatic cargo update to 2024-03-04 by @github-actions in
#3055
* Upgrade Rust toolchain to `nightly-2024-03-01` by @adpaco-aws in
#3052
* Add `--use-local-toolchain` to Kani setup by @jaisnan in
#3056
* Replace internal reverse_postorder by a stable one by @celinval in
#3064
* Add option to override `--crate-name` from `kani` by @adpaco-aws in
#3054
* cargo update and fix macos CI by @zhassan-aws in
#3067
* Bump tests/perf/s2n-quic from `d103836` to `1a7faa8` by @dependabot in
#3066
* Upgrade toolchain to 2024-03-11 by @zhassan-aws in
#3071
* Emit `dead` goto-instructions on MIR StatementDead by @karkhaz in
#3063


**Full Changelog**:
kani-0.47.0...kani-0.48.0
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.

4 participants