New challenges for Rc, Arc, and related Weak implementations #367
Conversation
doc/src/challenges/XXXX-rc.md
Outdated
| - **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!
doc/src/challenges/XXXX-rc.md
Outdated
|
|
||
| - **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.
doc/src/challenges/XXXX-rc.md
Outdated
|
|
||
| ## 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.
doc/src/challenges/XXXX-rc.md
Outdated
|
|
||
| ## 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.
doc/src/challenges/XXXX-rc.md
Outdated
|
|
||
| | 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?
doc/src/challenges/XXXY-arc.md
Outdated
|
|
||
| * 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.
doc/src/challenges/XXXY-arc.md
Outdated
| @@ -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)?
|
Thanks for the review @tautschnig! I've added a new commit that should address your comments |
There was a problem hiding this comment.
Thanks! My comments for the Rc challenge also apply to the Arc one.
Also, you'll need to update SUMMARY.md for your challenges to render in our book. When I do that locally, I get warnings like these:
warning: Potential incomplete link
┌─ challenges/0026-rc.md:44:7
│
44 │ | Rc<[mem::MaybeUninit<T>],A>::assume_init | alloc::rc |
│ ^^^^^^^^^^^^^^^^^^^^^ Did you forget to define a URL for `mem::MaybeUninit<T>`?
│
= hint: declare the link's URL. For example: `[mem::MaybeUninit<T>]: http://example.com/`
warning: Potential incomplete link
┌─ challenges/0026-rc.md:77:7
│
77 │ | Rc<[T]>::new_uninit_slice | alloc::rc |
│ ^^^ Did you forget to define a URL for `T`?
│
= hint: declare the link's URL. For example: `[T]: http://example.com/`
Could you fix these? I think you should just be able to wrap the path in a code block like challenge 1 does. You can check the rendering locally by running mdbook serve --open in the doc/ directory.
|
|
||
| ## Goal | ||
|
|
||
| The goal of this challenge is to verify [Rc](https://github.com/rust-lang/rust/blob/master/library/alloc/src/rc.rs) (meaning "Reference counted") and its related [Weak](https://github.com/rust-lang/rust/blob/master/library/alloc/src/rc.rs) 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.
| The goal of this challenge is to verify [Rc](https://github.com/rust-lang/rust/blob/master/library/alloc/src/rc.rs) (meaning "Reference counted") and its related [Weak](https://github.com/rust-lang/rust/blob/master/library/alloc/src/rc.rs) 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. | |
| The goal of this challenge is to verify [Rc](https://doc.rust-lang.org/std/rc/struct.Rc.html) (meaning "Reference counted") and its related [Weak](https://doc.rust-lang.org/std/rc/struct.Weak.html) 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. |
|
|
||
| * It may be possible to use a new construct analogous to the [can_dereference API](https://model-checking.github.io/kani/crates/doc/kani/mem/fn.can_dereference.html). Our new construct would track that a pointer indeed originates from `into_raw`. | ||
|
|
||
| * It is unclear how to show the reference count is greater than 0 when it is being decremented; the proposed `linked_list` [challenge](0005-linked-list.md) solution does not appear to check list length before performing operations either. |
There was a problem hiding this comment.
| * It is unclear how to show the reference count is greater than 0 when it is being decremented; the proposed `linked_list` [challenge](0005-linked-list.md) solution does not appear to check list length before performing operations either. | |
| * You are not required to check that the reference count is greater than 0 when it is being decremented |
The reference to the linked list solution will become outdated if/when the solution moves from proposed to accepted, and I don't think it's necessary to make your point.
|
|
||
| Some properties needed for safety are beyond the ability of the Rust type system to express. This is true for all challenges, but we point out some of the properties that are relevant for this challenge. | ||
|
|
||
| * It may be possible to use a new construct analogous to the [can_dereference API](https://model-checking.github.io/kani/crates/doc/kani/mem/fn.can_dereference.html). Our new construct would track that a pointer indeed originates from `into_raw`. |
There was a problem hiding this comment.
So what is the assumption here? This seems more like an observation. Is it incumbent on the person solving the challenge to propose and use such an API in their verification? Or is your point that for into_raw functions in Rc and Weak, they don't need to verify that the pointer returned originates from the given Rc/Weak? I think the latter, but I'd prefer to rephrase this bullet in terms of the assumption being made.
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.