Skip to content

gsoc2025: add Acknowledgement #146

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

Merged
zjp-CN merged 1 commit into from
Nov 6, 2025
Merged

gsoc2025: add Acknowledgement #146

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 16 additions & 6 deletions GSoC2025.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,8 @@ results in details and in a statistical chart. The data derive from `results.jso

![](https://github.com/user-attachments/assets/d49e4bce-9ba8-4df0-8d9b-f85690ac0d8b)

![](https://github.com/user-attachments/assets/26b59698-0387-4edf-92d7-bb8cde701b5e)

![](https://github.com/user-attachments/assets/e923bcda-9c9f-4c55-b915-0ee41bd9e870)

</details>
Expand All @@ -51,7 +53,8 @@ The usage and explanations have been documented in the [README][dv] of the repo.

## Comparision

Here's a rough comparision on verification process and duration without cache.
The table below compares verification process and duration with distributed-verification
enabled (columns 3-4) and disabled (columns 5-6).

| Duration (min) | Parameters | dv (amd) | dv (arm) | v-r-s (no auto) | v-r-s (auto) |
|----------------|------------|---------:|---------:|----------------:|-------------:|
Expand Down Expand Up @@ -98,16 +101,23 @@ fresh verifications will be performed in this case.

## What's left to do

Unfortunately, the incremental machanism is not fully applicapable to the verify-rust-std
project until the following problems are solved:
At present, the incremental verification workflow is quite incomplete for several reasons.
The incremental machanism is not fully applicapable to the verify-rust-std project until
the following problems are solved:
* [Partitioned proof runners regularly receive shutdown or communication lost][#143]
* This indicates that some runners are impossible to finish jobs on their own.
* [Untrustworthy outputs of multi-threaded verifications][#4438]
* This indicates that `results.json` files are unreliable to merge, especially when a
failure happens.
* At present, the incremental verification workflow is quite incomplete for several
other reasons.
* ESBMC or other verification tools are not supported.

ESBMC or other verification tools are not supported yet.

[#143]: https://github.com/os-checker/distributed-verification/issues/143
[#4438]: https://github.com/model-checking/kani/issues/4438

## Acknowledgement

Thanks to Michael for mentoring the task. And I'd like to extend sincere gratitude to
Jakub for his dedicated coordination efforts. The dev-desktop also helps me with the
project throughout the entire development.