Received-SPF: pass (google.com: domain of linux-kernel+bounces-134989-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:45e3:2400::1 as permitted sender) client-ip=2604:1380:45e3:2400::1;
Precedence: bulk
MIME-Version: 1.0
References: <20240402-linked-list-v1-0-b1c59ba7ae3b@google.com>
 <20240402-linked-list-v1-5-b1c59ba7ae3b@google.com> <d896a813-3081-40b4-985b-ef257d55cec2@proton.me>
 <CAH5fLgiN3jcd_HMgmP7H-026daMw0xkMk=CGaGc9AM7uHkFXFA@mail.gmail.com> <3f3cf5ae-30df-4032-b752-77126035784c@proton.me>
In-Reply-To: <3f3cf5ae-30df-4032-b752-77126035784c@proton.me>
From: Alice Ryhl <aliceryhl@google.com>
Date: Mon, 8 Apr 2024 10:04:17 +0200
Message-ID: <CAH5fLggF=dBYzySEt-TgNT+Tr-SNYvQxp3A26NktXNb2SNhDDg@mail.gmail.com>
Subject: Re: [PATCH 5/9] rust: list: add List
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>, 
	=?UTF-8?Q?Bj=C3=B6rn_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
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

On Thu, Apr 4, 2024 at 4:51=E2=80=AFPM Benno Lossin <benno.lossin@proton.me=
> wrote:
>
> On 04.04.24 16:12, Alice Ryhl wrote:
> > On Thu, Apr 4, 2024 at 4:03=E2=80=AFPM Benno Lossin <benno.lossin@proto=
n.me> wrote:
> >> On 02.04.24 14:17, Alice Ryhl wrote:
> >>> +        // never null for items in a list.
> >>> +        //
> >>> +        // INVARIANT: There are three cases:
> >>> +        //  * If the list has at least three items, then after remov=
ing the item, `prev` and `next`
> >>> +        //    will be next to each other.
> >>> +        //  * If the list has two items, then the remaining item wil=
l point at itself.
> >>> +        //  * If the list has one item, then `next =3D=3D prev =3D=
=3D item`, so these writes have no effect
> >>> +        //    due to the writes to `item` below.
> >>
> >> I think the writes do not have an effect. (no need to reference the
> >> writes to `item` below)
> >
> > ?
>
> The first write is
>
>      (*next).prev =3D prev;
>
> Using the fact that `next =3D=3D prev =3D=3D item` we have
>
>      (*item).prev =3D prev;
>
> But that is already true, since the function requirement is that
> `(*item).prev =3D=3D prev`. So the write has no effect.
> The same should hold for `(*prev).next =3D next`.

Oh, you are arguing that we aren't changing the value? I hadn't
actually realized that this was the case. But the reason that they end
up with the correct values according to the invariants is the writes
below that set them to null - not the fact that we don't change them
here. After all, setting them to a non-null value is wrong according
to the invariants.

Alice

> >>> +        unsafe {
> >>> +            (*next).prev =3D prev;
> >>> +            (*prev).next =3D next;
> >>> +        }
> >>> +        // SAFETY: We have exclusive access to items in the list.
> >>> +        // INVARIANT: The item is no longer in a list, so the pointe=
rs should be null.
> >>> +        unsafe {
> >>> +            (*item).prev =3D ptr::null_mut();
> >>> +            (*item).next =3D ptr::null_mut();
> >>> +        }