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-01-23 #2983

Merged
merged 17 commits into from
Feb 8, 2024

Conversation

celinval
Copy link
Contributor

@celinval celinval commented Jan 24, 2024

Try upgrading Rust toolchain to 2024-01-22, however, regression isn't working yet due to an issue with our assertion override hack. Related PRs so far:

Resolves #ISSUE-NUMBER

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

  - This is due to the safety fix to the internal function, which was
    done here: rust-lang/rust#120128
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Jan 24, 2024
@celinval celinval changed the title Toolchain 2024 01 22 Upgrade Rust toolchain to nightly-2024-01-23 Jan 24, 2024
celinval and others added 8 commits January 23, 2024 16:25
Dependency upgrade resulting from `cargo update`.

Co-authored-by: tautschnig <tautschnig@users.noreply.github.com>
These are the auto-generated release notes for comparison purposes:

## What's Changed
* Rethink `should_panic` and `fail_uncoverable` options as global
conditions by @adpaco-aws in
model-checking#2967
* Upgrade toolchain to nightly-2024-01-17 by @celinval in
model-checking#2976
* Benchcomp visualize: fix missing import by @tautschnig in
model-checking#2977
* Cargo update 2024-01-18 by @remi-delmas-3000 in
model-checking#2978

**Full Changelog**:
model-checking/kani@kani-0.44.0...kani-0.45.0

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Make __kani__workaround_core_assert public in lib.rs
@celinval celinval marked this pull request as ready for review January 26, 2024 22:45
@celinval celinval requested a review from a team as a code owner January 26, 2024 22:45
@qinheping
Copy link
Contributor

Some perf benchmarks regress from success to failure. We should not merge this PR until we fix them.
An example: https://github.com/model-checking/kani/actions/runs/7674225174/job/20918412309?pr=2983#step:13:237

@celinval
Copy link
Contributor Author

I did a quick research, the loop unwind assertion fails in function: ... My hypothesis is that the change in behavior we are seeing is due to rust-lang/rust#111803 where the threshold for calling nonoverlapping swap changed. Increasing the unwind limit seems to suffice to fix most harnesses. Unfortunately, check_insert_two_concrete harness runs out of memory.

@tautschnig tautschnig self-assigned this Feb 1, 2024
celinval added a commit to celinval/kani-dev that referenced this pull request Feb 3, 2024
I tried applying model-checking#2983 fix,
however, this would require user to import
`__kani_workaround_core_assert`. To fix that, I moved the definition to
be under `kani` crate.
tautschnig pushed a commit that referenced this pull request Feb 5, 2024
I tried applying #2983 fix,
however, this would require user to import
`__kani_workaround_core_assert`. To fix that, I moved the definition to
be under `kani` crate.

I replaced the existing fixme test. Initially I didn't check we had one,
and I created a second one which is simpler (no cargo needed) but that
also includes other cases.

Resolves #2187
@tautschnig tautschnig removed their assignment Feb 6, 2024
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Some change has dramatically increase the memory usage for this harness.
For now, we should include this harness in the list of slow tests until
we are able to identify the cause.
We also fix the unwind in the remaning harnesses.

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri feliperodri enabled auto-merge (squash) February 8, 2024 02:36
@feliperodri feliperodri merged commit f8fabc4 into model-checking:main Feb 8, 2024
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.

5 participants