rust-for-linux.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
From: "Benno Lossin" <lossin@kernel.org>
To: "Marcelo Moreira" <marcelomoreira1905@gmail.com>,
	"Boqun Feng" <boqun.feng@gmail.com>
Cc: "Danilo Krummrich" <dakr@kernel.org>, <benno.lossin@proton.me>,
	<ojeda@kernel.org>, <rust-for-linux@vger.kernel.org>,
	<skhan@linuxfoundation.org>,
	<linux-kernel-mentees@lists.linuxfoundation.org>,
	<~lkcamp/patches@lists.sr.ht>
Subject: Re: [PATCH v2] rust: doc: Clarify safety invariants for Revocable type
Date: Fri, 23 May 2025 10:42:58 +0200	[thread overview]
Message-ID: <DA3ENUO97I6D.234AA7I97AV62@kernel.org> (raw)
In-Reply-To: <CAPZ3m_i8fwsBRJKay72LHT4pEW=eZ5LxCFD=8CYkuEksjjt3_Q@mail.gmail.com>

On Fri May 23, 2025 at 2:13 AM CEST, Marcelo Moreira wrote:
> Thanks a lot for the discussions. I was reading them one by one and
> trying to consolidate the ideas.
> I am preparing a new patch version focused on improving everything
> that was discussed.
>
> Before submitting the patch, I would like to understand if things are
> clear to me. Here is what I am preparing:
>
> 1. Refined `Revocable<T>` Invariants, suggested by Benno:
> Proposed Documentation:
> /// # 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`.
> /// - `data` is valid for writes when `is_available` was atomically
> changed from `true` to `false`.

A few comments:

* your email client seems to wrap this line :(
* the "two cases" should be indented, as they logically belong to the
  bullet point above.
* the information for writing `data` needs to be changed according to
  what I suggested in reply to Danilo

>  2. Updated try_access and try_access_with_guard Safety Comments:
> Proposed Documentation:
> // INVARIANT: `self.data` is valid for reads because
> `self.is_available` is true,
> // and the RCU read-side lock ensures this condition is maintained
> during access.

I'm missing the context *where* this invariant comment is placed. Maybe
send the patch with the modification or send a link to a branch where
you have the commit.

> These comments now directly reference the new Revocable<T> read invariants.
> This addresses the  point about justifying the access to data via the
> invariants,
> especially considering the RCU read-side lock.
>
>
> 3. Clarified revoke_internal for SYNC = false and swap correction
> Proposed Documentation:
>  if self.is_available.swap(false, Ordering::Relaxed) {
>  if SYNC {
>                 // SAFETY: Just an FFI call, there are no further requirements.
>                 unsafe { bindings::synchronize_rcu() };

@Boqun: is this true?

If the answer is yes, then we should add this as a safe function in the
rcu module.

>  }  else {
>        // This branch for `revoke_nosync` requires the caller to prove
> that `data`
>        // can be dropped immediately without waiting for any RCU grace period.

I'm not sure that having a single function that does the revocation, but
has this going on is a good idea. The safety requirements will be pretty
complex.

@Danilo what do you think of inlining this function?

> }
> // SAFETY: We know `self.data` is valid because only one CPU can succeed the
> // `swap` above that takes `is_available` from `true` to `false`.
>  unsafe { drop_in_place(self.data.get()) };
>    }
> }
>
> I've added a  comment for the SYNC = false branch (used by revoke_nosync).
> This explicit else block, even if semantically empty of executable code, is for
> documenting the unsafe contract for revoke_nosync(). It  states that the caller
> must prove data safety since no RCU grace period is awaited, aligning with
> Danilo's explanation of revoke_nosync's purpose. Additionally, I've corrected
> the comment from compare_exchange to swap to accurately reflect the
> atomic operation used.
>
>
> 4. Documented RevocableGuard<'_, T> Invariants and PhantomData Adjustment
> Proposed Documentation:
> /// # Invariants
> ///
> /// - The RCU read-side lock is held for the lifetime of this guard.
> /// - `data_ref` points to valid data for the lifetime of this guard.
> pub struct RevocableGuard<'a, T> {
>     data_ref: *const T,
>     _rcu_guard: rcu::Guard,
>     _p: PhantomData<&'a T>,
> }

I think we can change this type to:

    pub struct RevocableGuard<'a, T> {
        data: &'a T,
        _rcu_guard: rcu::Guard,
    }

And then we don't need any invariants :)

> This adds the # Invariants section for RevocableGuard, as we agreed it should
> state its guarantees, including the RCU read-side lock. The adjustment of
> _p: PhantomData<&'a ()> to _p: PhantomData<&'a T> is a minor improvement in
> type-level documentation, making the lifetime dependency more explicit to the
> Rust compiler and future readers.
>
>
> 5. Revised RevocableGuard Deref Safety Comment
> Proposed Documentation:
> fn deref(&self) -> &Self::Target {
>         // SAFETY: By the invariants of `RevocableGuard`, the RCU
> read-side lock is held,
>         // and `data_ref` points to valid data for the lifetime of this guard.
>         unsafe { &*self.data_ref }

With the above change, this body becomes `self.data` :)

>     }
>
> The // SAFETY: comment for Deref is updated to refer to the RevocableGuard's new
> invariants, providing a justification for the unsafe dereference.
>
>
> 6. PinnedDrop for Revocable<T> Safety Documentation & Readability
> Proposed Documentation:
> let p = unsafe { self.get_unchecked_mut() };
>         if *p.is_available.get_mut() {
>             // INVARIANT: `is_available` is true, so `data` is valid for reads.
>             // SAFETY: `self.data` is valid for writes because
> `is_available` was atomically changed from true to false

This is wrong? It still is `true`?

>             // in `PinnedDrop::drop`, and only one thread can do it
> now as we have `&mut self`.
>             // This ensures `data` is valid for writes in this
> context, allowing `drop_in_place`.
>             unsafe { drop_in_place(p.data.get()) };
>         }
>
> The // INVARIANT: and // SAFETY: comments within the PinnedDrop
> implementation are
> updated to reflect the new write invariant of Revocable<T>, justifying
> the drop_in_place call.
>
>
> Please let me know if something is wrong or unnecessary... I'll try to
> rephrase if appropriate. Tks :D

It already looks much better than what we have currently. It's fine to
send a patch that's still needing review (and it makes it easier to
review when I have the full context). So I'd just do that and we go from
there. We're only on v2 on this one and I have seen patches go into the
double digits, so don't worry about that.

---
Cheers,
Benno

  reply	other threads:[~2025-05-23  8:43 UTC|newest]

Thread overview: 19+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2025-05-03 14:53 [PATCH v2] rust: doc: Clarify safety invariants for Revocable type Marcelo Moreira
2025-05-09 10:10 ` Benno Lossin
2025-05-17  0:03   ` Marcelo Moreira
2025-05-17  8:19     ` Benno Lossin
2025-05-17  9:54   ` Danilo Krummrich
2025-05-17 19:09     ` Benno Lossin
2025-05-19  8:50       ` Danilo Krummrich
2025-05-19  9:18         ` Benno Lossin
2025-05-19  9:55           ` Danilo Krummrich
2025-05-19 11:10             ` Benno Lossin
2025-05-19 11:37               ` Danilo Krummrich
2025-05-19 12:26                 ` Benno Lossin
2025-05-23  0:13                   ` Marcelo Moreira
2025-05-23  8:42                     ` Benno Lossin [this message]
2025-05-23  8:55                       ` Danilo Krummrich
2025-05-23 11:53                         ` Benno Lossin
2025-05-26  2:10                           ` Marcelo Moreira
2025-05-23  7:19                   ` Danilo Krummrich
2025-05-23  8:31                     ` Benno Lossin

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=DA3ENUO97I6D.234AA7I97AV62@kernel.org \
    --to=lossin@kernel.org \
    --cc=benno.lossin@proton.me \
    --cc=boqun.feng@gmail.com \
    --cc=dakr@kernel.org \
    --cc=linux-kernel-mentees@lists.linuxfoundation.org \
    --cc=marcelomoreira1905@gmail.com \
    --cc=ojeda@kernel.org \
    --cc=rust-for-linux@vger.kernel.org \
    --cc=skhan@linuxfoundation.org \
    --cc=~lkcamp/patches@lists.sr.ht \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).