Challenge 27: Verify atomically reference-counted Cell implementation
- Status: Open
- Solution: Option field to point to the PR that solved this challenge.
- Tracking Issue: #383
- Start date: 2025/06/01
- End date: 2025/12/31
- Reward: 10,000 USD
Goal
The goal of this challenge is to verify Arc (meaning "Atomically reference counted") and its related Weak implementation. Arc is the library-provided building block that enables safe multiple ownership of data through reference counting for multi-threaded code, as opposed to the usual ownership types used by Rust. The Rc implementation is the subject of a related challenge.
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.
Description
This challenge verifies a number of Arc methods that encapsulate unsafety, as well as providing contracts for unsafe methods that impose safety conditions on their callers for correct use.
A key part of the Arc implementation is the Weak struct, which allows keeping a temporary reference to an Arc without creating circular references and without protecting the inner value from being dropped.
Assumptions
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.
-
You are not required to check that the reference count is greater than 0 when it is being decremented.
-
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.
Success Criteria
All the following pub unsafe functions must be annotated with safety contracts and the contracts have been verified:
| Function | Location |
|---|---|
Arc<mem::MaybeUninit<T>,A>::assume_init | alloc::sync |
Arc<[mem::MaybeUninit<T>],A>::assume_init | alloc::sync |
Arc<T:?Sized>::from_raw | alloc::sync |
Arc<T:?Sized>::increment_strong_count | alloc::sync |
Arc<T:?Sized>::decrement_strong_count | alloc::sync |
Arc<T:?Sized,A:Allocator>::from_raw_in | alloc::sync |
Arc<T:?Sized,A:Allocator>::increment_strong_cobunt_in | alloc::sync |
Arc<T:?Sized,A:Allocator>::decrement_strong_count_in | alloc::sync |
Arc<T:?Sized,A:Allocator>::get_mut_unchecked | alloc::sync |
Arc<dyn Any+Send+Sync,A:Allocator>::downcast_unchecked | alloc::sync |
Weak<T:?Sized>::from_raw | alloc::sync |
Weak<T:?Sized,A:Allocator>::from_raw_in | alloc::sync |
These (not necessarily public) functions contain unsafe code in their bodies but are not themselves marked unsafe. At least 75% of these should be proven unconditionally safe, or safety contracts should be added.
| Function | Location |
|---|---|
| `Arc<T:?Sized, A:Allocator>::into_inner_with_allocator | alloc::sync |
Arc<T>::new | alloc::sync |
Arc<T>::new_uninit | alloc::sync |
Arc<T>::new_zeroed | alloc::sync |
Arc<T>::pin | alloc::sync |
Arc<T>::try_pin | alloc::sync |
Arc<T>::try_new | alloc::sync |
Arc<T>::try_new_uninit | alloc::sync |
Arc<T>::try_new_zeroed | alloc::sync |
Arc<T,A:Allocator>::new_in | alloc::sync |
Arc<T,A:Allocator>::new_uninit_in | alloc::sync |
Arc<T,A:Allocator>::new_zeroed_in | alloc::sync |
Arc<T,A:Allocator>::new_cyclic_in | alloc::sync |
Arc<T,A:Allocator>::pin_in | alloc::sync |
Arc<T,A:Allocator>::try_pin_in | alloc::sync |
Arc<T,A:Allocator>::try_new_in | alloc::sync |
Arc<T,A:Allocator>::try_new_uninit_in | alloc::sync |
Arc<T,A:Allocator>::try_new_zeroed_in | alloc::sync |
Arc<T,A:Allocator>::try_unwrap] | alloc::sync |
Arc<T,A:Allocator>::into_inner | alloc::sync |
Arc<[T]>::new_uninit_slice | alloc::sync |
Arc<[T]>::new_zeroed_slice | alloc::sync |
Arc<[T]>::into_array | alloc::sync |
Arc<[T],A:Allocator>::new_uninit_slice_in | alloc::sync |
Arc<[T],A:Allocator>::new_zeroed_slice_in | alloc::sync |
Arc<T:?Sized,A:Allocator>::into_raw_with_allocator | alloc::sync |
Arc<T:?Sized,A:Allocator>::as_ptr | alloc::sync |
Arc<T:?Sized,A:Allocator>::inner | alloc::sync |
Arc<T:?Sized,A:Allocator>::from_box_in | alloc::sync |
ArcFromSlice<T: Clone>::from_slice | alloc::sync |
ArcFromSlice<T: Copy>::from_slice | alloc::sync |
Clone<T: ?Sized, A:Allocator>::clone for Arc | alloc::sync |
Arc<T:?Sized+CloneToUninit, A:Allocator+Clone>::make_mut | alloc::sync |
Arc<T:?Sized, A:Allocator>::get_mut | alloc::sync |
Drop<T: ?Sized, A:Allocator>::drop for Arc | alloc::sync |
Arc<dyn Any+Send+Sync,A:Allocator>::downcast | alloc::sync |
Weak<T:?Sized,A:Allocator>::as_ptr | alloc::sync |
Weak<T:?Sized,A:Allocator>::into_raw_with_allocator | alloc::sync |
Weak<T:?Sized,A:Allocator>::upgrade | alloc::sync |
Weak<T:?Sized,A:Allocator>::inner | alloc::sync |
Drop<T:?Sized, A:Allocator>::drop for Weak | alloc::sync |
Default<T:Default>::default | alloc::sync |
Default<str>::default | alloc::sync |
Default<core::ffi::CStr>::default | alloc::sync |
Default<[T]>::default | alloc::sync |
From<&Str>::from | alloc::sync |
From<Vec<T,A:Allocator+Clone>>::from | alloc::sync |
From<Arc<str>>::from | alloc::sync |
TryFrom<Arc[T],A:Allocator>::try_from | alloc::sync |
ToArcSlice<T, I>::to_arc_slice | alloc::sync |
UniqueArcUninit<T:?Sized, A:Allocator>::new] | alloc::sync |
UniqueArcUninit<T:?Sized, A:Allocator>::data_ptr | alloc::sync |
Drop<T:?Sized, A:Allocator>::drop for UniqueArcUninit | alloc::sync |
UniqueArc<T:?Sized,A:Allocator>::into_arc | alloc::sync |
UniqueArc<T:?Sized,A:Allocator+Clone>::downgrade | alloc::sync |
Deref<T:?Sized,A:Allocator>::deref | alloc::sync |
DerefMut<T:?Sized,A:Allocator>::deref_mut | alloc::sync |
Drop<T:?Sized, A:Allocator>::drop for UniqueArc | alloc::sync |
This list excludes non-public unsafe functions; relevant ones should be called from public unsafe functions.
For functions taking inputs of generic type 'T', the proofs can be limited to primitive types o nly. Moreover, for functions taking allocators as input, the proofs can be limited to only the allocators implemented in the standard library (Global/System).
Note that solving this challenge will in part require proving an absence of data races from methods using atomic types (in this case Arc). This is also one of the main difficulties of Challenge 7. It's likely that a technique to do this for one challenge could be used for the other, with some adaptation.
List of UBs
In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following undefined behaviors:
- Data races.
- Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
- Invoking undefined behavior via compiler intrinsics.
- Mutating immutable bytes.
- Producing an invalid value.
Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.