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

Allow specifying the scheduling strategy in #[kani_proof] for async functions #1661

Merged
merged 8 commits into from
Jul 27, 2023

Conversation

fzaiser
Copy link
Contributor

@fzaiser fzaiser commented Sep 9, 2022

Description of changes:

Instead of having to manually wrap the code in kani::spawnable_block_on as in #1659, this PR allows #[kani::proof] to be applied to harnesses that use spawn as well. For this to happen, the user has to specify a scheduling strategy.

Resolved issues:

Resolves #ISSUE-NUMBER

Call-outs:

Testing:

  • How is this change tested? Additional regression test.

  • Is this a refactor change? No

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

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

@fzaiser fzaiser requested a review from a team as a code owner September 9, 2022 04:43
@fzaiser fzaiser changed the title BLOCKED: Allow specifying the scheduling strategy in #[kani_proof] BLOCKED: Allow specifying the scheduling strategy in #[kani_proof] for async functions Sep 9, 2022
@fzaiser fzaiser changed the title BLOCKED: Allow specifying the scheduling strategy in #[kani_proof] for async functions Allow specifying the scheduling strategy in #[kani_proof] for async functions Jul 10, 2023
@fzaiser fzaiser force-pushed the spawn-macro branch 3 times, most recently from fb768a4 to 00386e8 Compare July 10, 2023 11:40
@fzaiser
Copy link
Contributor Author

fzaiser commented Jul 10, 2023

With #1659 merged, this is no longer blocked! I've rebased and updated this PR, but there seem to be issues with concrete playback that I don't understand (the script-based-pre exec tests are failing). Before I try to figure that out, I wanted to check that the changes of this PR are still desired. What do you think, @celinval @adpaco-aws?

@fzaiser
Copy link
Contributor Author

fzaiser commented Jul 10, 2023

Huh, seems that the tests pass in CI (not sure why they failed locally). In that case, this PR is ready for review.

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 @fzaiser.

Does verifying an async harnesses require the unstable flag to be passed? Is there any documentation to how an async harness is verified? What happens if no argument is passed?

library/kani_macros/src/lib.rs Outdated Show resolved Hide resolved
library/kani_macros/src/lib.rs Outdated Show resolved Hide resolved
@fzaiser
Copy link
Contributor Author

fzaiser commented Jul 14, 2023

Does verifying an async harnesses require the unstable flag to be passed?

Yes, it requires -Z async-lib.

Is there any documentation to how an async harness is verified?

There is some documentation here: https://model-checking.github.io/kani/crates/doc/kani/attr.proof.html. I just added additional information regarding spawn to the documentation of the proof macro in this PR.

What happens if no argument is passed?

If no argument is passed, it uses block_on (instead of block_on_with_spawn). If the harness code tries to call kani::spawn, it will hit this panic here. I changed this from an .expect() call to an explicit panic!() because Kani provides better location information that way. So verification will fail with the following output:

Check 53: kani::spawn::<[async block@tests/kani/AsyncAwait/spawn.rs:20:30: 22:6]>.assertion.1
         - Status: FAILURE
         - Description: "This is a placeholder message; Kani doesn't support message formatted at runtime"
         - Location: library/kani/src/futures.rs:189:13 in function kani::spawn::<[async block@tests/kani/AsyncAwait/spawn.rs:20:30: 22:6]>

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.

Can you please add the following ui tests please?

  • Wrong attribute argument
  • No unstable flag provided

Thanks!

@fzaiser
Copy link
Contributor Author

fzaiser commented Jul 21, 2023

@celinval I added the requested tests. This should be ready to merge.

@celinval celinval enabled auto-merge (squash) July 27, 2023 02:41
@celinval celinval merged commit a2a1e85 into model-checking:main Jul 27, 2023
12 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants