Skip to content

Add kani in ci + kani proof for conformance to 2.7.7.2 section #338

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

Merged
merged 2 commits into from
Jul 24, 2025

Conversation

priyasiddharth
Copy link

@priyasiddharth priyasiddharth commented Jun 3, 2025

Enable Kani in the CI and add the verify_spec_2_7_7_2() proof to verify that the implementation of queue satisfies 2.7.7.2 requirement. The proof relies on whether the EVENT_IDX feature has been negotiated. Conversely with test_needs_notification() test, this proof tests for all possible values of the queue structure.

Summary of the PR

This is review-ready version of #324 and #339.
First, we add Kani to the CI pipeline with a timeout of 20 minutes. The timeout is essential because Kani converts a rust program to a SAT problem which is NP-complete and may not return in a reasonable time.

Second, we add a kani proof to meet the requirements outlined in 2.7.7.2 of the virtio specification regarding the notification suppression mechanism. We have sketched this proof from the same proof defined for the queue implemented in firecraker. This commit adds the verify_spec_2_7_7_2() proof to verify that the implementation of queue meets 2.7.7.2 requirement. The proof relies on whether the EVENT_IDX feature has been negotiated. Conversely with test_needs_notification() test, this proof tests for all possible values of queue. To run the proof, you can run:

cargo kani

The proof currently passes with kani v0.62.0:

SUMMARY:
 ** 0 of 4880 failed (379 unreachable)

 ** 1 of 1 cover properties satisfied


VERIFICATION:- SUCCESSFUL
Verification Time: 82.47572s

Manual Harness Summary:
Complete - 1 successfully verified harnesses, 0 failures, 1 total.

Requirements

Before submitting your PR, please make sure you addressed the following
requirements:

  • All commits in this PR have Signed-Off-By trailers (with
    git commit -s), and the commit message has max 60 characters for the
    summary and max 75 characters for each description line.
  • All added/changed functionality has a corresponding unit/integration
    test.
  • All added/changed public-facing functionality has entries in the "Upcoming
    Release" section of CHANGELOG.md (if no such section exists, please create one).
  • Any newly added unsafe code is properly documented.

@stefano-garzarella
Copy link
Member

@priyasiddharth thanks for this PR. IIUC you are re-working a patch initially developed from @MatiasVara, so I think you should add also your S-o-b in the patch.

@priyasiddharth
Copy link
Author

Thank you @stefano-garzarella for the taking on the review. I have added a sign-off tag.

@priyasiddharth priyasiddharth force-pushed the main branch 2 times, most recently from f915258 to 6ac82d5 Compare June 10, 2025 14:33
@priyasiddharth
Copy link
Author

@stefano-garzarella PTAL

@stefano-garzarella
Copy link
Member

@priyasiddharth please mention big changes (e.g. you included patch from #339) and the reason after a push. I think that should also be mentioned in the PR description/title.

Also we usually squash new changes in commit, so all the "fix(comment)..." commit, should be squashed in the first commit (you can remove my Co-authored-by, it was just a suggestion while reviewing. As a general rule, a commit in a PR should not change/fix code added in the same PR.

Maybe we can also change the order of the patches, first enable the CI, then add the first test.

@stefano-garzarella
Copy link
Member

@alexandruag @andreeaflorescu @jiangliu @slp @stsquad @epilys any thought on this?

@priyasiddharth
Copy link
Author

@andreeaflorescu @epilys PTAL

@priyasiddharth
Copy link
Author

@andreeaflorescu @epilys PTAL

Copy link
Member

@epilys epilys left a comment

Choose a reason for hiding this comment

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

LGTM, left one comment about missing license header

Run kani as a part of the CI pipeline. In particular, run the proofs for
virtio-queue. In some cases, kani may not finish so set a twenty minutes
timeout.

Signed-off-by: Matias Ezequiel Vara Larsen <[email protected]>
Signed-off-by: Siddharth Priya <[email protected]>
Add the verify_spec_2_7_7_2() proof to verify that the implementation of
queue satisfies 2.7.7.2 requirement. The proof relies on whether the
EVENT_IDX feature has been negotiated. Conversely with
`test_needs_notification()` test, this proof `tests` for all possible
values of the queue structure.

Signed-off-by: Matias Ezequiel Vara Larsen <[email protected]>
Signed-off-by: Siddharth Priya <[email protected]>
@stefano-garzarella stefano-garzarella enabled auto-merge (rebase) July 24, 2025 13:57
@stefano-garzarella
Copy link
Member

@priyasiddharth @MatiasVara as next step (in another PR), maybe we can add something in README.md like we do for ## Fuzzing to explain a bit what we do for proof of conformance and how to run kani. WDYT?

@stefano-garzarella stefano-garzarella merged commit 9d26f93 into rust-vmm:main Jul 24, 2025
2 checks passed
@MatiasVara
Copy link
Contributor

@priyasiddharth @MatiasVara as next step (in another PR), maybe we can add something in README.md like we do for ## Fuzzing to explain a bit what we do for proof of conformance and how to run kani. WDYT?

It is a great idea!

@stefano-garzarella
Copy link
Member

@priyasiddharth @MatiasVara as next step (in another PR), maybe we can add something in README.md like we do for ## Fuzzing to explain a bit what we do for proof of conformance and how to run kani. WDYT?

It is a great idea!

Just added an issue to track it #353

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.

6 participants