| lists.openwall.net | lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC | |
|
Open Source and information security mailing list archives
| ||
|
Date: Thu, 04 Apr 2024 14:51:16 +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 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:
>>> +
>>> + if self.first.is_null() {
>>> + self.first = item;
>>> + // SAFETY: The caller just gave us ownership of these fields.
>>> + // INVARIANT: A linked list with one item should be cyclic.
>>> + unsafe {
>>> + (*item).next = item;
>>> + (*item).prev = item;
>>> + }
>>> + } else {
>>> + let next = self.first;
>>> + // SAFETY: We just checked that `next` is non-null.
>>
>> Missing mention of the type invariant.
>
> SAFETY: By the type invariant, this pointer is valid or null. We just
> checked that it's not null, so it must be valid.
Sounds good.
[...]
>>> + /// Removes the first item from this list.
>>> + pub fn pop_front(&mut self) -> Option<ListArc<T, ID>> {
>>> + if self.first.is_null() {
>>> + return None;
>>> + }
>>> +
>>> + // SAFETY: The first item of this list is in this list.
>>> + Some(unsafe { self.remove_internal(self.first) })
>>> + }
>>> +
>>> + /// Removes the provided item from this list and returns it.
>>> + ///
>>> + /// This returns `None` if the item is not in the list.
>>
>> I think this should say "Returns `None` if the item is not in a list.".
>> (Technically it should be "is not in a `List<T, ID>`", since it *can* be
>> in another list with a different ID.)
>
> I'm not really convinced. The phrases "the list" and "a list" are
> equivalent given the safety requirement for this method, but "the
> list" seems more natural to me. The `remove` method of any other
> collection would say "the list" too.
They are equivalent, but saying "the list" has the potential for this
confusion: "If the function returns `None` if the item is not in the
list, then why do I need to ensure that it is not in a different list?".
>
>>> + ///
>>> + /// # Safety
>>> + ///
>>> + /// The provided item must not be in a different linked list.
>>> + pub unsafe fn remove(&mut self, item: &T) -> Option<ListArc<T, ID>> {
>>> + let mut item = unsafe { ListLinks::fields(T::view_links(item)) };
>>> + // SAFETY: The user provided a reference, and reference are never dangling.
>>> + //
>>> + // As for why this is not a data race, there are two cases:
>>> + //
>>> + // * If `item` is not in any list, then these fields are read-only and null.
>>> + // * If `item` is in this list, then we have exclusive access to these fields since we
>>> + // have a mutable reference to the list.
>>> + //
>>> + // In either case, there's no race.
>>> + let ListLinksFields { next, prev } = unsafe { *item };
>>> +
>>> + debug_assert_eq!(next.is_null(), prev.is_null());
>>> + if !next.is_null() {
>>> + // This is really a no-op, but this ensures that `item` is a raw pointer that was
>>> + // obtained without going through a pointer->reference->pointer conversion rountrip.
>>> + // This ensures that the list is valid under the more restrictive strict provenance
>>> + // ruleset.
>>> + //
>>> + // SAFETY: We just checked that `next` is not null, and it's not dangling by the
>>> + // list invariants.
>>> + unsafe {
>>> + debug_assert_eq!(item, (*next).prev);
>>> + item = (*next).prev;
>>> + }
>>> +
>>> + // SAFETY: We just checked that `item` is in a list, so the caller guarantees that it
>>> + // is in this list. The pointers are in the right order.
>>> + Some(unsafe { self.remove_internal_inner(item, next, prev) })
>>> + } else {
>>> + None
>>> + }
>>> + }
>>> +
>>> + /// Removes the provided item from the list.
>>> + ///
>>> + /// # Safety
>>> + ///
>>> + /// The pointer must point at an item in this list.
>>> + unsafe fn remove_internal(&mut self, item: *mut ListLinksFields) -> ListArc<T, ID> {
>>> + // SAFETY: The caller promises that this pointer is not dangling, and there's no data race
>>> + // since we have a mutable reference to the list containing `item`.
>>> + let ListLinksFields { next, prev } = unsafe { *item };
>>> + // SAFETY: The pointers are ok and in the right order.
>>> + unsafe { self.remove_internal_inner(item, next, prev) }
>>> + }
>>> +
>>> + /// Removes the provided item from the list.
>>> + ///
>>> + /// # Safety
>>> + ///
>>> + /// The `item` pointer must point at an item in this list, and we must have `(*item).next ==
>>> + /// next` and `(*item).prev == prev`.
>>> + unsafe fn remove_internal_inner(
>>> + &mut self,
>>> + item: *mut ListLinksFields,
>>> + next: *mut ListLinksFields,
>>> + prev: *mut ListLinksFields,
>>> + ) -> ListArc<T, ID> {
>>> + // SAFETY: We have exclusive access to items in the list, and prev/next pointers are
>>
>> I think you mean that you have exclusive access to the prev/next fields
>> of the `ListLinks` associated with `ID`... But that is rather long.
>> Does anyone have any idea to shorten this?
>
> SAFETY: We have exclusive access to the pointers of items in the list,
> and the prev/next pointers are never null for items in a list.
I would say that they are valid instead of never null, since you
dereference them below. Otherwise sounds good.
>
>>> + // 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`.
>
>>> + 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();
>>> + }
>>> + // INVARIANT: There are three cases:
>>> + // * If `item` was not the first item, then `self.first` should remain unchanged.
>>> + // * If `item` was the first item and there is another item, then we just updated
>>> + // `prev->next` to `next`, which is the new first item, and setting `item->next` to null
>>> + // did not modify `prev->next`.
>>> + // * If `item` was the only item in the list, then `prev == item`, and we just set
>>> + // `item->next` to null, so this correctly sets `first` to null now that the list is
>>> + // empty.
>>> + if self.first == item {
>>> + // SAFETY: The `prev` field of an item in a list is never dangling.
>>
>> I don't think this SAFETY comment makes sense.
>>
>>> + self.first = unsafe { (*prev).next };
>
> SAFETY: `prev` is the `prev` pointer from a `ListLinks` in a `List`,
> so the pointer is valid. There's no race, since we have exclusive
> access to the list.
Sounds good.
--
Cheers,
Benno
Powered by blists - more mailing lists