diff --git a/GSoC2025.md b/GSoC2025.md new file mode 100644 index 0000000..436a453 --- /dev/null +++ b/GSoC2025.md @@ -0,0 +1,113 @@ +# Google Summer of Code 2025 Final Report + +## Goal + +The main goal it to implement [distributed and resource-efficient verification][proposal] +for verify-rust-std project. That is to implement + +> A system that can reliably run all verification tasks within a time limit (where that +> time limit needs to be determined empirically), and for changes that do not impact any +> contract no actual verification tool is invoked. + +[proposal]: https://github.com/rust-lang/google-summer-of-code/tree/45141d74c28d91e114cf621d2d56aea6c3f82547?tab=readme-ov-file#distributed-and-resource-efficient-verification + +## What I did + +I developed a set of tools to achieve the goal with 600+ commits, 70 issues, and 57 PRs +from April to October. + +The first is `distributed-verification`, which analyzes all kani proofs in the standard +library. The tool traverses calls in each proof, and computes a direct hash value based on +the source code, then computes an aggregated hash value through all the functions reached. + +The second is `verify_rust_std`, which compares two versions of proofs by their hash +values, and emits the proofs whose hash has changed. Specifically, `kani-list.json` +generated by `kani` and JSONs generated by `distributed-verification` are merged into a +`hash.json` file as one version of proofs by `verify_rust_std merge` command. Then `kani` +filters the exact differentiated proof names and executes verification on them. + +The third is a static [webpage][home] deployed on Github Pages, showing verification +results in details and in a statistical chart. The data derive from `results.json` and +`core.sqlite3`, stored in another Github repo. + +
+ +WebUI + +![](https://github.com/user-attachments/assets/d49e4bce-9ba8-4df0-8d9b-f85690ac0d8b) + +![](https://github.com/user-attachments/assets/e923bcda-9c9f-4c55-b915-0ee41bd9e870) + +
+ +The CI workflow [verify-rust-std.yml] demonstrates that kani proofs are partitioned onto 8 +machines to be verified. + +The usage and explanations have been documented in the [README][dv] of the repo. + +[dv]: https://github.com/os-checker/distributed-verification +[home]: https://os-checker.github.io/distributed-verification/ +[verify-rust-std.yml]: https://github.com/os-checker/distributed-verification/blob/95a4bfe47a769be6bf5d897b729f918c0e18fcd3/.github/workflows/verify-rust-std.yml + +## Comparision + +Here's a rough comparision on verification process and duration without cache. + +| Duration (min) | Parameters | dv (amd) | dv (arm) | v-r-s (no auto) | v-r-s (auto) | +|----------------|------------|---------:|---------:|----------------:|-------------:| +| (installation) | kani | 5 | 12 | 5 | 5 | +| (installation) | dv | 0.5 | 0.5 | | | +| installation | = | 5.5 | 12.5 | 5 | 5 | +| gen proof info | | 2 | 2 | 6 | 4 | +| (verify) | partition | 8 | 8 | 4 | 1 | +| (verify) | kani -j | 3 | 3 | 4 | 3 | +| (verify) | runner | 10 | 8 | 15 | 50 | +| (verify) | total | 240 | 192 | 240 | 150 | +| **runner** | | 18 | 23 | 26 | 59 | + +* dv (amd) shows that generating annotated proofs with distributed-verification and +verifying them on 8 amd64 machines may take 18 minutes. There are two jobs: partition job +and verification job. The first is installing dv and generating proof info in 2.5 minutes, +while partitioning proofs and uploading proof info just happen in a second. The second is +installing dv and kani, and running verifications in 15.5 minutes. Since verification job +is done in parallel, it takes 18 minutes to see the complete CI finishes. +* dv (arm) shows that the same process on arm64 as that on amd64, whereas it takes a bit +longer time to install kani because solvers are installed from source code instead of +`apt install`. It's 2 minutes less in partition verifications than on amd64 machines. +* v-r-s (no auto) shows that kani is installed in 5 minutes, generates kani-list.json in 6 +minutes, and verifies partitioned proofs in 15 minutes, thus total 26 minutes for each +runner in the verify-rust-std repo. +* v-r-s (auto) shows a total 59 minutes in the whole process without proofs partitioned +onto other machines. It takes the longest runner time, while least total verification +time for no reason from my understanding: it does more verification work, because +autoharnesses are also verified. + +For partial or incremental verification, the minimal duration is 2.5 minutes on both amd64 +and arm64 when no code reached is modified, because only the first job needs doing. As +the code is increasingly modified with regard to some proofs, the duration in the second +job increases. As a result, distributed-verification saves 10 to 20 times as much time as +verify-rust-std CI currently takes. + +Note that a Rust toolchain bump always invalidates all the current proof hashes, thus +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 untile 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` are unsable to be trusted 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. + +[#143]: https://github.com/os-checker/distributed-verification/issues/143 +[#4438]: https://github.com/model-checking/kani/issues/4438