diff --git a/GSoC2025.md b/GSoC2025.md index 216091f..1e4ca0b 100644 --- a/GSoC2025.md +++ b/GSoC2025.md @@ -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) @@ -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) | |----------------|------------|---------:|---------:|----------------:|-------------:| @@ -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. +