From: Alice Ryhl <aliceryhl@google.com>
To: Benno Lossin <benno.lossin@proton.me>
Cc: "Miguel Ojeda" <ojeda@kernel.org>,
	"Andrew Morton" <akpm@linux-foundation.org>,
	"Alex Gaynor" <alex.gaynor@gmail.com>,
	"Wedson Almeida Filho" <wedsonaf@gmail.com>,
	"Boqun Feng" <boqun.feng@gmail.com>,
	"Gary Guo" <gary@garyguo.net>,
	"Björn Roy Baron" <bjorn3_gh@protonmail.com>,
	"Andreas Hindborg" <a.hindborg@samsung.com>,
	"Marco Elver" <elver@google.com>,
	"Kees Cook" <keescook@chromium.org>, "Coly Li" <colyli@suse.de>,
	"Paolo Abeni" <pabeni@redhat.com>,
	"Pierre Gondois" <pierre.gondois@arm.com>,
	"Ingo Molnar" <mingo@kernel.org>,
	"Jakub Kicinski" <kuba@kernel.org>,
	"Wei Yang" <richard.weiyang@gmail.com>,
	"Matthew Wilcox" <willy@infradead.org>,
	linux-kernel@vger.kernel.org, rust-for-linux@vger.kernel.org
Subject: Re: [PATCH 7/9] rust: list: add cursor
Date: Wed, 3 Apr 2024 14:49:11 +0200	[thread overview]
Message-ID: <CAH5fLghEg37m_PhJxE8FVORHGROE9rd1CJttaWBGc7cXZCX+yQ@mail.gmail.com> (raw)
In-Reply-To: <4aaf7fd7-49ed-4b3e-b691-0d8d7d426d3a@proton.me>
On Wed, Apr 3, 2024 at 2:19 PM Benno Lossin <benno.lossin@proton.me> wrote:
>
> On 02.04.24 14:17, Alice Ryhl wrote:
> > diff --git a/rust/kernel/list.rs b/rust/kernel/list.rs
> > index 892705dd0571..47e52818c7bd 100644
> > --- a/rust/kernel/list.rs
> > +++ b/rust/kernel/list.rs
> > @@ -408,6 +408,20 @@ pub fn push_all_back(&mut self, other: &mut List<T, ID>) {
> >          other.first = ptr::null_mut();
> >      }
> >
> > +    /// Returns a cursor to the first element of the list.
> > +    ///
> > +    /// If the list is empty, this returns `None`.
> > +    pub fn cursor_front(&mut self) -> Option<Cursor<'_, T, ID>> {
> > +        if self.first.is_null() {
> > +            None
> > +        } else {
> > +            Some(Cursor {
>
> Missing INVARIANT comment.
>
> > +                current: self.first,
> > +                list: self,
> > +            })
> > +        }
> > +    }
> > +
> >      /// Creates an iterator over the list.
> >      pub fn iter(&self) -> Iter<'_, T, ID> {
> >          // INVARIANT: If the list is empty, both pointers are null. Otherwise, both pointers point
> > @@ -476,6 +490,69 @@ fn next(&mut self) -> Option<ArcBorrow<'a, T>> {
> >      }
> >  }
> >
> > +/// A cursor into a [`List`].
> > +///
> > +/// # Invariants
> > +///
> > +/// The `current` pointer points a value in `list`.
> > +pub struct Cursor<'a, T: ?Sized + ListItem<ID>, const ID: u64 = 0> {
> > +    current: *mut ListLinksFields,
> > +    list: &'a mut List<T, ID>,
> > +}
> > +
> > +impl<'a, T: ?Sized + ListItem<ID>, const ID: u64> Cursor<'a, T, ID> {
> > +    /// Access the current element of this cursor.
> > +    pub fn current(&self) -> ArcBorrow<'_, T> {
> > +        // SAFETY: The `current` pointer points a value in the list.
> > +        let me = unsafe { T::view_value(ListLinks::from_fields(self.current)) };
> > +        // SAFETY:
> > +        // * All values in a list are stored in an `Arc`.
> > +        // * The value cannot be removed from the list for the duration of the lifetime annotated
> > +        //   on the returned `ArcBorrow`, because removing it from the list would require mutable
> > +        //   access to the cursor or the list. However, the `ArcBorrow` holds an immutable borrow
> > +        //   on the cursor, which in turn holds an immutable borrow on the list, so any such
>
> The cursor has a mutable borrow on the list.
>
>
> > +        //   mutable access requires first releasing the immutable borrow on the cursor.
> > +        // * Values in a list never have a `UniqueArc` reference.
>
> Is there some type invariant guaranteeing this?
The List owns a ListArc reference to the value. It would be unsound
for there to also be a UniqueArc reference to it.
Alice
next prev parent reply	other threads:[~2024-04-03 12:49 UTC|newest]
Thread overview: 40+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2024-04-02 12:16 [PATCH 0/9] Add Rust linked list for reference counted values Alice Ryhl
2024-04-02 12:16 ` [PATCH 1/9] rust: list: add ListArc Alice Ryhl
2024-04-03 15:51   ` Benno Lossin
2024-04-04 14:00     ` Alice Ryhl
2024-05-03 14:36       ` Alice Ryhl
2024-05-04 15:50         ` Benno Lossin
2024-04-03 17:18   ` Kane York
2024-04-02 12:16 ` [PATCH 2/9] rust: list: add tracking for ListArc Alice Ryhl
2024-04-03 15:52   ` Benno Lossin
2024-04-04 14:14     ` Alice Ryhl
2024-04-04 14:41       ` Benno Lossin
2024-04-02 12:17 ` [PATCH 3/9] rust: list: add struct with prev/next pointers Alice Ryhl
2024-04-03 15:57   ` Benno Lossin
2024-04-04 14:03     ` Alice Ryhl
2024-04-04 14:05       ` Benno Lossin
2024-04-05  9:47   ` Benno Lossin
2024-04-08  7:57     ` Alice Ryhl
2024-04-02 12:17 ` [PATCH 4/9] rust: list: add macro for implementing ListItem Alice Ryhl
2024-04-03 10:42   ` Benno Lossin
2024-04-02 12:17 ` [PATCH 5/9] rust: list: add List Alice Ryhl
2024-04-04 14:03   ` Benno Lossin
2024-04-04 14:12     ` Alice Ryhl
2024-04-04 14:51       ` Benno Lossin
2024-04-08  8:04         ` Alice Ryhl
2024-04-08  8:51           ` Benno Lossin
2024-04-02 12:17 ` [PATCH 6/9] rust: list: add iterators Alice Ryhl
2024-04-04 14:36   ` Benno Lossin
2024-04-04 14:41     ` Alice Ryhl
2024-04-04 14:52       ` Benno Lossin
2024-04-08  8:00         ` Alice Ryhl
2024-04-02 12:17 ` [PATCH 7/9] rust: list: add cursor Alice Ryhl
2024-04-03 12:19   ` Benno Lossin
2024-04-03 12:49     ` Alice Ryhl [this message]
2024-04-04 13:28       ` Benno Lossin
2024-04-04 13:40         ` Alice Ryhl
2024-04-02 12:17 ` [PATCH 8/9] rust: list: support heterogeneous lists Alice Ryhl
2024-04-04 15:35   ` Benno Lossin
2024-04-08  7:59     ` Alice Ryhl
2024-04-02 12:17 ` [PATCH 9/9] rust: list: add ListArcField Alice Ryhl
2024-04-04 15:47   ` 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=CAH5fLghEg37m_PhJxE8FVORHGROE9rd1CJttaWBGc7cXZCX+yQ@mail.gmail.com \
    --to=aliceryhl@google.com \
    --cc=a.hindborg@samsung.com \
    --cc=akpm@linux-foundation.org \
    --cc=alex.gaynor@gmail.com \
    --cc=benno.lossin@proton.me \
    --cc=bjorn3_gh@protonmail.com \
    --cc=boqun.feng@gmail.com \
    --cc=colyli@suse.de \
    --cc=elver@google.com \
    --cc=gary@garyguo.net \
    --cc=keescook@chromium.org \
    --cc=kuba@kernel.org \
    --cc=linux-kernel@vger.kernel.org \
    --cc=mingo@kernel.org \
    --cc=ojeda@kernel.org \
    --cc=pabeni@redhat.com \
    --cc=pierre.gondois@arm.com \
    --cc=richard.weiyang@gmail.com \
    --cc=rust-for-linux@vger.kernel.org \
    --cc=wedsonaf@gmail.com \
    --cc=willy@infradead.org \
    /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).