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

["Benno Lossin" <lossin@kernel.org>]

On Tue May 27, 2025 at 3:02 AM CEST, Marcelo Moreira wrote:
> 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:
>> > +/// - `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.

We should change the invariant to only consider threads that can access
`data`. So 

    - `data` is valid for writes when `is_available` was atomically
      changed from `true` to `false` and no thread that has access to
      `data` is holding an RCU read-side lock that was acquired prior to
      the change in `is_available`.

>> >  #[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>.

We don't do SAFETY comments on "implicit" unsafe operations. A SAFETY
comment must always be directly above an `unsafe` block.

> 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.

I think it should be done in this patch series, as it makes the safety
comments significantly easier. In my mind the refactoring also shouldn't
be too expensive.

> 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.

Missing '`' around code. Also please use `Self` instead of Revocable<T>.

>> >              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.

Your email client seems to rewrap the lines, could you avoid that, as it
makes the text harder to read? Thanks!

I don't think it's a good idea to have information in parenthesis in
safety comments, they should be clear without the need for optional
information. Also this needs the invariant change that I mentioned
above. 

>> 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.

Yes, but please include them in the next version of your patch series :)
They make the safety comments a lot simpler.

---
Cheers,
Benno