rust-for-linux.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
* [PATCH v3] rust: revocable: Correct safety comments and add invariants
@ 2025-05-26  2:01 Marcelo Moreira
  2025-05-26  8:56 ` Benno Lossin
  0 siblings, 1 reply; 7+ messages in thread
From: Marcelo Moreira @ 2025-05-26  2:01 UTC (permalink / raw)
  To: lossin, dakr, ojeda, rust-for-linux, skhan, linux-kernel-mentees,
	~lkcamp/patches

Introducing a comprehensive `# Invariants` section for the `Revocable<T>`
type. This new documentation details the validity conditions of the `data`
field concerning `is_available` and RCU read-side locks.

The safety comments in `Revocable::try_access`,
`Revocable::try_access_with_guard`, and the `PinnedDrop` implementation
for `Revocable<T>` have been updated to explicitly reference these newly
defined invariants, ensuring that the justification for unsafe operations
is clear and directly tied to the type's guaranteed properties.

Reported-by: Benno Lossin <lossin@kernel.org>
Closes: https://github.com/Rust-for-Linux/linux/issues/1160
Suggested-by: Benno Lossin <lossin@kernel.org>
Suggested-by: Danilo Krummrich <dakr@kernel.org>
Signed-off-by: Marcelo Moreira <marcelomoreira1905@gmail.com>
---
Changes in v3:
- Refined the wording of the `Revocable<T>` invariants to be more precise
  about read and write validity conditions, specifically including RCU
  read-side lock acquisition timing for reads and RCU grace period for writes.
- Simplified the `try_access_with_guard` safety comment for better conciseness.
- Removed changes related to `RevocableGuard` invariants and its `Deref`
  implementation, as these are planned for a separate, future patch.
- Reverted `revoke_internal` changes (like `else` block for `revoke_nosync`
  and `swap` correction) to be part of a separate refactoring patch.
---
 rust/kernel/revocable.rs | 25 ++++++++++++++++++-------
 1 file changed, 18 insertions(+), 7 deletions(-)

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`.
+/// - `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`.
 #[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.
             Some(RevocableGuard::new(self.data.get(), guard))
         } else {
             None
@@ -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.
             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.
+            // 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`.
             unsafe { drop_in_place(p.data.get()) };
         }
     }
-- 
2.49.0


^ permalink raw reply related	[flat|nested] 7+ messages in thread

* Re: [PATCH v3] rust: revocable: Correct safety comments and add invariants
  2025-05-26  2:01 [PATCH v3] rust: revocable: Correct safety comments and add invariants Marcelo Moreira
@ 2025-05-26  8:56 ` Benno Lossin
  2025-05-27  1:02   ` Marcelo Moreira
  0 siblings, 1 reply; 7+ messages in thread
From: Benno Lossin @ 2025-05-26  8:56 UTC (permalink / raw)
  To: Marcelo Moreira, dakr, ojeda, rust-for-linux, skhan,
	linux-kernel-mentees, ~lkcamp/patches

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 :)

> +/// - `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).

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

>              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()) };

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?

---
Cheers,
Benno

>          }
>      }


^ permalink raw reply	[flat|nested] 7+ messages in thread

* Re: [PATCH v3] rust: revocable: Correct safety comments and add invariants
  2025-05-26  8:56 ` Benno Lossin
@ 2025-05-27  1:02   ` Marcelo Moreira
  2025-05-27 12:03     ` Benno Lossin
  0 siblings, 1 reply; 7+ messages in thread
From: Marcelo Moreira @ 2025-05-27  1:02 UTC (permalink / raw)
  To: Benno Lossin
  Cc: dakr, ojeda, rust-for-linux, skhan, linux-kernel-mentees,
	~lkcamp/patches

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

^ permalink raw reply	[flat|nested] 7+ messages in thread

* Re: [PATCH v3] rust: revocable: Correct safety comments and add invariants
  2025-05-27  1:02   ` Marcelo Moreira
@ 2025-05-27 12:03     ` Benno Lossin
  2025-06-02  1:17       ` Marcelo Moreira
  0 siblings, 1 reply; 7+ messages in thread
From: Benno Lossin @ 2025-05-27 12:03 UTC (permalink / raw)
  To: Marcelo Moreira
  Cc: dakr, ojeda, rust-for-linux, skhan, linux-kernel-mentees,
	~lkcamp/patches

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

^ permalink raw reply	[flat|nested] 7+ messages in thread

* Re: [PATCH v3] rust: revocable: Correct safety comments and add invariants
  2025-05-27 12:03     ` Benno Lossin
@ 2025-06-02  1:17       ` Marcelo Moreira
  2025-06-02  6:38         ` Miguel Ojeda
  0 siblings, 1 reply; 7+ messages in thread
From: Marcelo Moreira @ 2025-06-02  1:17 UTC (permalink / raw)
  To: Benno Lossin
  Cc: dakr, ojeda, rust-for-linux, skhan, linux-kernel-mentees,
	~lkcamp/patches

oh no, it looks like I submitted the patch without the explicit v4
version and without the 0/3 part :/...  Sorry for that, it's the first
time I've made a split patch like that.

Em ter., 27 de mai. de 2025 às 09:03, Benno Lossin <lossin@kernel.org> escreveu:
>
> 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

^ permalink raw reply	[flat|nested] 7+ messages in thread

* Re: [PATCH v3] rust: revocable: Correct safety comments and add invariants
  2025-06-02  1:17       ` Marcelo Moreira
@ 2025-06-02  6:38         ` Miguel Ojeda
  2025-06-02 10:28           ` Marcelo Moreira
  0 siblings, 1 reply; 7+ messages in thread
From: Miguel Ojeda @ 2025-06-02  6:38 UTC (permalink / raw)
  To: Marcelo Moreira
  Cc: Benno Lossin, dakr, ojeda, rust-for-linux, skhan,
	linux-kernel-mentees, ~lkcamp/patches

On Mon, Jun 2, 2025 at 3:18 AM Marcelo Moreira
<marcelomoreira1905@gmail.com> wrote:
>
> oh no, it looks like I submitted the patch without the explicit v4
> version and without the 0/3 part :/...  Sorry for that, it's the first
> time I've made a split patch like that.

No worries!

I saw the other message with the extra "manual" v4 cover letter, but
that may confuse tooling, since it is wrapped and the title does not
match etc., so it is best to resubmit it properly at this point.

The cover letter, and the right titles etc. should be generated by
`git format-patch` for you, so I would suggest using that and
reviewing the output (you will need to fill the cover letter in the
file it generates) before sending it.

Thanks!

Cheers,
Miguel

^ permalink raw reply	[flat|nested] 7+ messages in thread

* Re: [PATCH v3] rust: revocable: Correct safety comments and add invariants
  2025-06-02  6:38         ` Miguel Ojeda
@ 2025-06-02 10:28           ` Marcelo Moreira
  0 siblings, 0 replies; 7+ messages in thread
From: Marcelo Moreira @ 2025-06-02 10:28 UTC (permalink / raw)
  To: Miguel Ojeda
  Cc: Benno Lossin, dakr, ojeda, rust-for-linux, skhan,
	linux-kernel-mentees, ~lkcamp/patches

Em seg., 2 de jun. de 2025 às 03:38, Miguel Ojeda
<miguel.ojeda.sandonis@gmail.com> escreveu:
>
> On Mon, Jun 2, 2025 at 3:18 AM Marcelo Moreira
> <marcelomoreira1905@gmail.com> wrote:
> >
> > oh no, it looks like I submitted the patch without the explicit v4
> > version and without the 0/3 part :/...  Sorry for that, it's the first
> > time I've made a split patch like that.
>
> No worries!
>
> I saw the other message with the extra "manual" v4 cover letter, but
> that may confuse tooling, since it is wrapped and the title does not
> match etc., so it is best to resubmit it properly at this point.

Ok, I will resend, Thanks!

> The cover letter, and the right titles etc. should be generated by
> `git format-patch` for you, so I would suggest using that an
> reviewing the output (you will need to fill the cover letter in the
> file it generates) before sending it.

Ok.

Cheers,
Marcelo Moreira.

^ permalink raw reply	[flat|nested] 7+ messages in thread

end of thread, other threads:[~2025-06-02 10:28 UTC | newest]

Thread overview: 7+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2025-05-26  2:01 [PATCH v3] rust: revocable: Correct safety comments and add invariants Marcelo Moreira
2025-05-26  8:56 ` Benno Lossin
2025-05-27  1:02   ` Marcelo Moreira
2025-05-27 12:03     ` Benno Lossin
2025-06-02  1:17       ` Marcelo Moreira
2025-06-02  6:38         ` Miguel Ojeda
2025-06-02 10:28           ` Marcelo Moreira

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