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

[Benno Lossin]

On 08.04.24 10:04, Alice Ryhl wrote:
> On Thu, Apr 4, 2024 at 4:51 PM Benno Lossin <benno.lossin@xxxxxxxxx> wrote:
>>
>> On 04.04.24 16:12, Alice Ryhl wrote:
>>> On Thu, Apr 4, 2024 at 4:03 PM Benno Lossin <benno.lossin@xxxxxxxxx> 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();
>>>>> +        }