Received-SPF: pass (google.com: domain of linux-kernel+bounces-135083-linux.lists.archive=gmail.com@vger.kernel.org designates 147.75.48.161 as permitted sender) client-ip=147.75.48.161;
Date: Mon, 08 Apr 2024 08:51:04 +0000
To: Alice Ryhl <aliceryhl@google.com>
From: 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
Subject: Re: [PATCH 5/9] rust: list: add List
Message-ID: <f51231b2-46a4-4fea-af9d-d16b0ea59bf5@proton.me>
In-Reply-To: <CAH5fLggF=dBYzySEt-TgNT+Tr-SNYvQxp3A26NktXNb2SNhDDg@mail.gmail.com>
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> <CAH5fLggF=dBYzySEt-TgNT+Tr-SNYvQxp3A26NktXNb2SNhDDg@mail.gmail.com>
Feedback-ID: 71780778:user:proton
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable

On 08.04.24 10:04, Alice Ryhl wrote:
> 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`.
>=20
> 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.

I just was confused by the "due to the writes to `item` below".
In the single element case, I also think that the INVARIANT comment of
the next `unsafe` block (still visible in this mail) is a bit weird,
since the element still is in the list.
For a single item, removing it is setting the prev, next and first
pointers to null. So I think you might be able to use this for the last
bullet point:

     * If the list has one item, then `next =3D=3D prev =3D=3D item`, so th=
ese
       writes have no effect, since also `(*item).prev =3D=3D prev` and
       `(*item).next =3D=3D next` by function requirement.

For the INVARIANT comment below, I think you also need the case
distinction:

     * If the list had more than one item, `item` is no longer in the
       list, so the pointers should be null.
     * If the list had one item, then `item` points to itself, to remove
       it, we set `prev` and `next` to null and later also `self.first`.

What do you think?

--=20
Cheers,
Benno

>=20
> Alice
>=20
>>>>> +        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();
>>>>> +        }