New challenges for Rc, Arc, and related Weak implementations #367
Conversation
| - **Tracking Issue:** *Link to issue* | ||
| - **Start date:** 2025/06/01 | ||
| - **End date:** 2025/12/31 | ||
| - **Reward:** *TBD*[^reward] |
There was a problem hiding this comment.
Actually, please do propose a reward - it will still be reviewed the by reward committee and they may propose changes, but they do want an initial proposal. Thank you!
|
|
||
| - **Status:** Open | ||
| - **Solution:** *Option field to point to the PR that solved this challenge.* | ||
| - **Tracking Issue:** *Link to issue* |
There was a problem hiding this comment.
We knowingly have a chicken&egg problem here; please create an issue now, put its link in here, and eventually update the issue once this PR is merged.
|
|
||
| ## Goal | ||
|
|
||
| The goal of this challenge is to verify Rc and its related Weak implementation. Rc is the library-provided building block that enables safe multiple ownership of data through reference counting for single-threaded cases, as opposed to the usual ownership types used by Rust. A related challenge verifies the Arc implementation, which is atomic multi-threaded. |
There was a problem hiding this comment.
Please include source-code pointers as Rc is not as easy to search for. I'd appreciate if the same could be done for Weakand Arc.
|
|
||
| ## Motivation | ||
|
|
||
| The Rc (for single-threaded code) and Arc (atomic multi-threaded) cell types are widely used in Rust programs to enable shared ownership of data through reference counting. Since shared ownership is generally not permitted by Rust's type system, these implementations use unsafe code to bypass Rust's usual compile-time checks. Verifying the Rust standard library thus fundamentally requires verification of these types. |
There was a problem hiding this comment.
In terms of reading it is a bit awkward that only the second paragraph explains what Rc and Arc stand for. Please make sure you include the explanation of the acronyms upon first use.
|
|
||
| | Function | Location | | ||
| |---------|---------| | ||
| | Rc<mem::MaybeUninit<T>,A>::assume_init | alloc::rc | |
There was a problem hiding this comment.
Can you please include guidance in the challenge on what level of completeness you expect with regard to generics?
|
|
||
| * Showing that something is initialized, as required by `assume_init`, appears to be beyond the current state of the art for type systems, so it may be impossible to express the full safety property required there. | ||
|
|
||
| * In general, Kani does not support verifying concurrent code, but it may still be possible to verify the memory-related safety properties here, assuming that the atomicity declarations are sufficient. |
There was a problem hiding this comment.
The challenges should not prescribe a particular verification tool, so I don't think you should consider Kani's limitations a constraint.
| @@ -0,0 +1,138 @@ | |||
| # Challenge XXXY[^challenge_id]: Verify atomically reference-counted Cell implementation | |||
There was a problem hiding this comment.
Do you forsee any overlap/interaction with Challenge 7 (Safety of Methods for Atomic Types and ReentrantLock)?
This PR proposes two new challenges, namely:
Any feedback is greatly appreciated!
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.