Re: [PATCH 5/9] rust: list: add List

[Alice Ryhl <aliceryhl@google.com>]

On Thu, Apr 4, 2024 at 4:51 PM Benno Lossin <benno.lossin@proton.me> wrote:
>
> On 04.04.24 16:12, Alice Ryhl wrote:
> > On Thu, Apr 4, 2024 at 4:03 PM Benno Lossin <benno.lossin@proton.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.

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