[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <f51231b2-46a4-4fea-af9d-d16b0ea59bf5@proton.me>
Date: Mon, 08 Apr 2024 08:51:04 +0000
From: Benno Lossin <benno.lossin@...ton.me>
To: Alice Ryhl <aliceryhl@...gle.com>
Cc: Miguel Ojeda <ojeda@...nel.org>, Andrew Morton <akpm@...ux-foundation.org>, Alex Gaynor <alex.gaynor@...il.com>, Wedson Almeida Filho <wedsonaf@...il.com>, Boqun Feng <boqun.feng@...il.com>, Gary Guo <gary@...yguo.net>, Björn Roy Baron <bjorn3_gh@...tonmail.com>, Andreas Hindborg <a.hindborg@...sung.com>, Marco Elver <elver@...gle.com>, Kees Cook <keescook@...omium.org>, Coly Li <colyli@...e.de>, Paolo Abeni <pabeni@...hat.com>, Pierre Gondois <pierre.gondois@....com>, Ingo Molnar <mingo@...nel.org>, Jakub Kicinski <kuba@...nel.org>, Wei Yang <richard.weiyang@...il.com>, Matthew Wilcox <willy@...radead.org>, linux-kernel@...r.kernel.org, rust-for-linux@...r.kernel.org
Subject: Re: [PATCH 5/9] rust: list: add List
On 08.04.24 10:04, Alice Ryhl wrote:
> On Thu, Apr 4, 2024 at 4:51 PM Benno Lossin <benno.lossin@...ton.me> wrote:
>>
>> On 04.04.24 16:12, Alice Ryhl wrote:
>>> On Thu, Apr 4, 2024 at 4:03 PM Benno Lossin <benno.lossin@...ton.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 removing the item, `prev` and `next`
>>>>> + // will be next to each other.
>>>>> + // * If the list has two items, then the remaining item will point at itself.
>>>>> + // * If the list has one item, then `next == prev == 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 = prev;
>>
>> Using the fact that `next == prev == item` we have
>>
>> (*item).prev = prev;
>>
>> But that is already true, since the function requirement is that
>> `(*item).prev == prev`. So the write has no effect.
>> The same should hold for `(*prev).next = 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.
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 == prev == item`, so these
writes have no effect, since also `(*item).prev == prev` and
`(*item).next == 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?
--
Cheers,
Benno
>
> Alice
>
>>>>> + unsafe {
>>>>> + (*next).prev = prev;
>>>>> + (*prev).next = next;
>>>>> + }
>>>>> + // SAFETY: We have exclusive access to items in the list.
>>>>> + // INVARIANT: The item is no longer in a list, so the pointers should be null.
>>>>> + unsafe {
>>>>> + (*item).prev = ptr::null_mut();
>>>>> + (*item).next = ptr::null_mut();
>>>>> + }
Powered by blists - more mailing lists