Messages in this thread | | | Date | Mon, 08 Apr 2024 08:51:04 +0000 | From | Benno Lossin <> | 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@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.
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(); >>>>> + }
| |