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

Benno Lossin
2025-05-26T08:56:32Z

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

> }
> }