Skip to content

Enable GitHub Linux/Arm runners in CI #3841

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 12 commits into from
Jul 15, 2025
Merged

Enable GitHub Linux/Arm runners in CI #3841

merged 12 commits into from
Jul 15, 2025

Conversation

tautschnig
Copy link
Member

GitHub made Linux Arm 64-bit runners available:
https://github.blog/changelog/2025-01-16-linux-arm64-hosted-runners-now-available-for-free-in-public-repositories-public-preview/. Run regression tests on those and build release packages.

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

@tautschnig
Copy link
Member Author

Waiting for GitHub to fix permissions - see https://github.com/orgs/community/discussions/148648#discussioncomment-11858717.

@tautschnig
Copy link
Member Author

Turns out we need a CBMC fix as well (which has previously already been built for CBMC's Debian package, but not been upstreamed): diffblue/cbmc#8572.

@tautschnig tautschnig self-assigned this Jan 20, 2025
@tautschnig
Merge remote-tracking branch 'origin/main' into arm-ci
c985ac8
@tautschnig
Update CBMC dependency to 6.7.0
757c788 
Kani now uses CBMC's latest release. Notably, this includes necessary
fixes to improve Kani's quantifier support as well as full aarch64/Linux
support, and better constant propagation (which, in turn, required
adjusting the `unsupported_num_objects` test so that object creation
done in a loop does not get sliced from the formula).

Resolves: model-checking#4020
@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Jun 26, 2025
@tautschnig tautschnig marked this pull request as ready for review July 11, 2025 16:02
@tautschnig tautschnig requested a review from a team as a code owner July 11, 2025 16:02
@tautschnig tautschnig removed their assignment Jul 12, 2025
carolynzech
carolynzech approved these changes Jul 14, 2025
View reviewed changes
Copy link
Contributor

@carolynzech carolynzech left a comment

Choose a reason for hiding this comment

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

Thanks! I wonder if we should add x86 as a suffix to make the distinction clearer (e.g. BuildBundle-Linux-x86). I don't feel strongly, though.

@tautschnig
Copy link
Member Author

Thanks! I wonder if we should add x86 as a suffix to make the distinction clearer (e.g. BuildBundle-Linux-x86). I don't feel strongly, though.

Makes a lot of sense, now done!

@tautschnig tautschnig added this pull request to the merge queue Jul 15, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Jul 15, 2025
@tautschnig tautschnig self-assigned this Jul 15, 2025
@tautschnig tautschnig added this pull request to the merge queue Jul 15, 2025
@tautschnig tautschnig removed this pull request from the merge queue due to a manual request Jul 15, 2025
@tautschnig tautschnig added this pull request to the merge queue Jul 15, 2025
@tautschnig tautschnig removed this pull request from the merge queue due to a manual request Jul 15, 2025
@tautschnig tautschnig enabled auto-merge July 15, 2025 20:22
@tautschnig tautschnig added this pull request to the merge queue Jul 15, 2025
Merged via the queue into model-checking:main with commit d49a9ff Jul 15, 2025
15 of 17 checks passed
@tautschnig tautschnig deleted the arm-ci branch July 15, 2025 21:56
tautschnig added a commit to tautschnig/kani that referenced this pull request Aug 6, 2025
@tautschnig
Fix release job dependencies
27639da 
This is a fix-up to model-checking#3841 where the job names were not adjusted in one
place.
@tautschnig tautschnig mentioned this pull request Aug 6, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Aug 6, 2025
@tautschnig
Fix release job dependencies (#4273)
32e3d8f 
This is a fix-up to #3841 where the job names were not adjusted in one
place.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
@rajath-mk rajath-mk mentioned this pull request Aug 6, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Aug 7, 2025
@rajath-mk @zhassan-aws
bump kani vesion 0.65.0 (#4274)
677c791 
from the autogenerated : 

## What's Changed
* Ensure that contract closures are FnOnce by @vonaka in
#4151
* Adjust sized hierarchy for Kani's memory predicates by @tautschnig in
#4193
* Update to Rust edition 2024 by @tautschnig in
#4197
* `ptr_offset_from`: Replace arithmetic over pointers by offset
arithmetic by @tautschnig in
#4180
* Automatic cargo update to 2025-07-07 by @github-actions[bot] in
#4208
* Bump tests/perf/s2n-quic from `b8f8cca` to `8715fdf` by
@dependabot[bot] in #4209
* Upgrade Rust toolchain to 2025-07-04 by @tautschnig in
#4199
* Upgrade Rust toolchain to 2025-07-10 by @thanhnguyen-aws in
#4215
* Update CBMC dependency to 6.7.1 by @tautschnig in
#4178
* Split compiler flags to avoid dependency recompilation by
@AlexanderPortland in #4211
* Fix the bug that assign clause cannot be inferred for the inner loop
of nested loops by @thanhnguyen-aws in
#4179
* Upgrade Rust toolchain to 2025-07-11 by @thanhnguyen-aws in
#4219
* Automatic toolchain upgrade to nightly-2025-07-12 by
@github-actions[bot] in #4222
* Fix bug: `goto-cc` crash when there are two quantifers in one proof by
@thanhnguyen-aws in #4221
* Automatic toolchain upgrade to nightly-2025-07-13 by
@github-actions[bot] in #4223
* Automatic cargo update to 2025-07-14 by @github-actions[bot] in
#4224
* Cleanup links to issues that have been addressed by @tautschnig in
#4200
* Selectively enable and fix (slow) Tokio tests by @tautschnig in
#4203
* Bump tests/perf/s2n-quic from `32ba87d` to `1cbd879` by
@dependabot[bot] in #4227
* Implement support for Cargo.toml's default-members by @tautschnig in
#4201
* Do not invoke memset with count of zero by @tautschnig in
#4205
* Support bitwuzla, cvc5, z3 as solver attribute values by @tautschnig
in #4218
* Use CBMC's shuffle_vector expression by @tautschnig in
#4204
* Move tests from slow/kani back to regular suite by @tautschnig in
#4202
* Automatic toolchain upgrade to nightly-2025-07-14 by
@github-actions[bot] in #4225
* Enable GitHub Linux/Arm runners in CI by @tautschnig in
#3841
* Automatic cargo update to 2025-07-21 by @github-actions[bot] in
#4231
* Skip codegen for unneeded harnesses by @AlexanderPortland in
#4213
* Strongly type differing compiler args for clarity by
@AlexanderPortland in #4220
* Remove StableMIR ICE workaround by @carolynzech in
#4235
* Fix bug: Kani unwinds loops with contract in generic function (with -Z
loop-contracts) by @thanhnguyen-aws in
#4232
* Automatic cargo update to 2025-07-28 by @github-actions[bot] in
#4238
* Bump tests/perf/s2n-quic from `1cbd879` to `4938450` by
@dependabot[bot] in #4242
* Upgrade Rust toolchain to 2025-07-21 by @tautschnig in
#4241
* Remove `pretty_ty` and use rustc_public's formatter instead by
@tautschnig in #4243
* Upgrade Rust toolchain to 2025-07-24 by @tautschnig in
#4244
* Documentation cleanup of UB detected by Kani by @tautschnig in
#4245
* Upgrade Rust toolchain to 2025-07-29 by @tautschnig in
#4247
* Automatic toolchain upgrade to nightly-2025-07-30 by
@github-actions[bot] in #4253
* Add unstable option prove-safety-only by @tautschnig in
#4239
* Set bits_per_byte in byte_extract expressions by @tautschnig in
#4255
* `KaniAttributes` Path Resolution Refactor by @carolynzech in
#4249
* Automatic toolchain upgrade to nightly-2025-07-31 by
@github-actions[bot] in #4256
* Support contracts & stubs in trait implementations (partial fix) by
@carolynzech in #4250
* [Breaking Changes] Remove unstable list feature and default memory
checks by @carolynzech in
#4258
* Upgrade Rust toolchain to 2025-08-01 by @tautschnig in
#4261
* Autoharness: add support for references by @tautschnig in
#4234
* Turn off debug assertions under `--prove-safety-only` by @tautschnig
in #4262
* Automatic toolchain upgrade to nightly-2025-08-02 by
@github-actions[bot] in #4264
* Automatic toolchain upgrade to nightly-2025-08-03 by
@github-actions[bot] in #4265
* Automatic cargo update to 2025-08-04 by @github-actions[bot] in
#4267
* Automatic toolchain upgrade to nightly-2025-08-04 by
@github-actions[bot] in #4266
* Introduce thread pool for writing goto binaries in parallel by
@AlexanderPortland in #4236
* Major-version update cargo dependencies by @tautschnig in
#4240
* Bump tests/perf/s2n-quic from `4938450` to `8f510f0` by
@dependabot[bot] in #4270
* Automatic toolchain upgrade to nightly-2025-08-05 by
@github-actions[bot] in #4271
* Automatic toolchain upgrade to nightly-2025-08-06 by
@github-actions[bot] in #4272
* Avoid updating irrelevant symbols when handling quantifiers by
@AlexanderPortland in #4268
* Lazily evaluate debug info by @AlexanderPortland in
#4269
* Clone a template `BodyTransformer` to avoid re-initialization by
@AlexanderPortland in #4259
* Ensuring that MIR constants are marked as static consts by @vonaka in
#4233
* Fix release job dependencies by @tautschnig in
#4273

## New Contributors
* @vonaka made their first contribution in
#4151

**Full Changelog**:
kani-0.64.0...kani-0.65.0

---------

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
1 more reviewer

@carolynzech carolynzech carolynzech approved these changes

Reviewers whose approvals may not affect merge requirements
Assignees

@tautschnig tautschnig

Labels
Z-EndToEndBenchCI Tag a PR to run benchmark CI
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@tautschnig @carolynzech