Re: [PATCH v3] rust: revocable: Correct safety comments and add invariants

Marcelo Moreira
2025-05-27T01:02:27Z

Em seg., 26 de mai. de 2025 às 05:56, Benno Lossin <lossin@kernel.org> wrote:
>
> On Mon May 26, 2025 at 4:01 AM CEST, Marcelo Moreira wrote:
> > diff --git a/rust/kernel/revocable.rs b/rust/kernel/revocable.rs
> > index 1e5a9d25c21b..fed860ad2e60 100644
> > --- a/rust/kernel/revocable.rs
> > +++ b/rust/kernel/revocable.rs
> > @@ -61,6 +61,14 @@
> > /// v.revoke();
> > /// assert_eq!(add_two(&v), None);
> > /// ```
> > +/// # Invariants
> > +///
> > +/// - `data` is valid for reads in two cases:
> > +/// - while `is_available` is true, or
> > +/// - while the RCU read-side lock is taken and it was acquired while `is_available` was `true`.
>
> This looks good now :)

Nice! sounds good =)

> > +/// - `data` is valid for writes when `is_available` was atomically changed from `true` to `false`
> > +/// and no thread is holding an RCU read-side lock that was acquired prior to the change in
> > +/// `is_available`.
>
> This doesn't cover the case needed in `drop`, since there might be a
> thread holding the RCU read-side lock when `drop` is run. But that
> doesn't matter, because that thread isn't going to access `data` (since
> it can't have a reference to the value anymore, after all we're dropping
> it).

My understanding: I understand that the write invariant primarily describes
how data becomes valid for writes after revocation (RCU grace period).
In the specific context of drop, the validity for writes (e.g., drop_in_place)
is predominantly guaranteed by the exclusive mutable access (&mut self) of the
PinnedDrop implementation, rather than the RCU-based write invariant.
The RCU readers would not be able to access the data being dropped anyway.

Plans for v4: I don't understand if we need to change something here or if this
will be reflected in the SAFETY comment for drop.

> > #[pin_data(PinnedDrop)]
> > pub struct Revocable<T> {
> > is_available: AtomicBool,
> > @@ -97,8 +105,9 @@ pub fn new(data: impl PinInit<T>) -> impl PinInit<Self> {
> > pub fn try_access(&self) -> Option<RevocableGuard<'_, T>> {
> > let guard = rcu::read_lock();
> > if self.is_available.load(Ordering::Relaxed) {
> > - // Since `self.is_available` is true, data is initialised and has to remain valid
> > - // because the RCU read side lock prevents it from being dropped.
> > + // INVARIANT: `self.data` is valid for reads because `self.is_available` is true,
> > + // and the RCU read-side lock held by `guard` ensures this condition is maintained
> > + // during access.
>
> Two things here:
> 1. This comment should refer to the type invariants of `Self` ie
> "`self.data` is valid for reads because of the type invariants of
> `Self` and because ...".
> 2. `INVARIANT` comments report on changes in the type invariants of a
> type. For example when constructing a type with type invariants, one
> has to document that the invariants are fulfilled. In this case, the
> invariants of `RevocableGuard` are:
>
> /// The RCU read-side lock is held while the guard is alive.
>
> Which already is fulfilled by us having the `rcu::Guard` type around.
> So we should also change the invariants of the `RevocableGuard`.
>
> I think I suggested on the previous version that we change `data_ref` to
> a shared reference and thus simplify the `RevocableGuard` type, because
> it won't need `unsafe` any more. Then we can also remove all invariants
> on it. (And we also won't need the `new` function any more, since we
> have direct access to the fields).
>
> (This change should be its own patch)
>
> Then we will gain a new `unsafe` block in the code here that we will
> justify with the type invariant of `Self`.
>
> On second thought, we can reuse the `try_access_with_guard` function and
> then we won't need an `unsafe` block here.
>
> > Some(RevocableGuard::new(self.data.get(), guard))
> > } else {
> > None

My understanding: The INVARIANT comment should be changed to SAFETY,
as we are justifying an unsafe operation (implicitly within RevocableGuard::new
due to self.data.get()), not establishing a new invariant for Revocable<T>.

The SAFETY comment should explicitly state that the validity of self.data for
reads is because of Revocable<T>'s type invariants, in addition to the
conditions
(is_available being true and RCU read-side lock).

The proposed RevocableGuard simplification (changing data_ref to &T and
making RevocableGuard internally safe) is a significant refactoring that
should be in a separate, future patch.

For this v4 patch, RevocableGuard::new will continue to take a raw
pointer. Therefore,
try_access will continue to call RevocableGuard::new(self.data.get(),
guard), and the SAFETY
comment will justify this existing (implicit) unsafe interaction,
rather than introducing a new
unsafe block by calling try_access_with_guard here, which would
prematurely depend on the
RevocableGuard refactoring.

Plans for v4: Change the comment from // INVARIANT: to // SAFETY.
- Reformulate the comment to: "SAFETY: self.data is valid for reads because
of Revocable<T>'s type invariants, as is_available is true and _guard holds
the RCU read-side lock."

- No changes to the underlying logic of try_access (it will still call
RevocableGuard::new with self.data.get()).

> > @@ -115,8 +124,8 @@ pub fn try_access(&self) -> Option<RevocableGuard<'_, T>> {
> > /// object.
> > pub fn try_access_with_guard<'a>(&'a self, _guard: &'a rcu::Guard) -> Option<&'a T> {
> > if self.is_available.load(Ordering::Relaxed) {
> > - // SAFETY: Since `self.is_available` is true, data is initialised and has to remain
> > - // valid because the RCU read side lock prevents it from being dropped.
> > + // SAFETY: `self.data` is valid for reads as `is_available` is true and `_guard`
> > + // holds the RCU read-side lock, adhering to `Revocable<T>`'s invariants.
>
> This is the wrong way around, the safety comment *relies* on the type
> invariants of `Self`. So it should be
>
> SAFETY: `self.data` is valid for reads because of the type
> invariants of `Self` and as `is_available` is true and `_guard`
> holds the RCU read-side lock.

My understanding: The SAFETY comment should clarify that the
operation's safety derives from or
relies on Revocable<T>'s type invariants, rather than merely "adhering to" them.

Plans for v4: Reformulate the SAFETY comment to:
SAFETY: self.data is valid for reads because of Revocable<T>'s type
invariants, as is_available is true and _guard holds the RCU read-side lock.

> > Some(unsafe { &*self.data.get() })
> > } else {
> > None
> > @@ -176,9 +185,11 @@ fn drop(self: Pin<&mut Self>) {
> > // SAFETY: We are not moving out of `p`, only dropping in place
> > let p = unsafe { self.get_unchecked_mut() };
> > if *p.is_available.get_mut() {
> > - // SAFETY: We know `self.data` is valid because no other CPU has changed
> > - // `is_available` to `false` yet, and no other CPU can do it anymore because this CPU
> > - // holds the only reference (mutable) to `self` now.
> > + // INVARIANT: `is_available` is true, so `data` is valid for reads.
>
> We're not only reading `data`, but also writing to it! (`drop_in_place`
> takes a mutable raw pointer and will call `Drop::drop` with a mutable
> reference)
>
> > + // SAFETY: `self.data` is valid for writes because `is_available` is true, and
> > + // this `PinnedDrop` context (having `&mut self`) guarantees exclusive access,
> > + // ensuring no other thread can concurrently access or revoke `data`.
> > + // This ensures `data` is valid for `drop_in_place`.
>
> We have to mention the type invariants of `Self` here too. And also we
> have to satisfy all the conditions on the second invariant:
>
> /// - `data` is valid for writes when `is_available` was atomically changed from `true` to `false`
> /// and no thread is holding an RCU read-side lock that was acquired prior to the change in
> /// `is_available`.
>
> This is the problem with that invariant that I outlined above. Nobody
> can access `data`, since we're getting dropped.
>
> > unsafe { drop_in_place(p.data.get()) };

My understanding: The operation in drop_in_place is a write
(destruction), so the prior INVARIANT
comment focusing on "reads" was a mistake.

The SAFETY comment needs to explicitly mention Revocable<T>'s type invariants.

For drop, the primary safety guarantee for writes is the exclusive
mutable access (&mut self)
provided by the PinnedDrop context, in addition to is_available being
true. The RCU-specific
conditions of the write invariant are less directly relevant here
because of this exclusive ownership
during drop.

Plans for v4: Remove the line: // INVARIANT: is_available is true, so
data is valid for reads.

Reformulate the // SAFETY: comment to: SAFETY: self.data is valid for
writes because of
Revocable<T>'s type invariants (specifically, that data is valid when
is_available is true),
and because this PinnedDrop context (having &mut self) guarantees
exclusive access,
ensuring no other thread can concurrently access or revoke data. This
ensures data is valid
for drop_in_place.

>
> A function that also needs to be adjusted is the `revoke_internal`
> function. That's where the second type invariant comes in. I suggested
> that we remove that and split the behavior into `revoke()` and
> `revoke_nosync()` and Danilo agreed, so could you add that in another
> patch?
>

My understanding: I fully understand and agree that the following are
significant refactorings
and should be handled in separate, dedicated patches, not in v4

- RevocableGuard Simplification: Changing data_ref from a raw pointer
(*const T) to a shared
reference (&T), removing its unsafe logic and internal invariants.

- revoke_internal Refactoring: Splitting revoke_internal into revoke()
and revoke_nosync() functions.

Thanks again for your invaluable guidance! =D

Cheers,
Marcelo Moreira