LinkedList

ostd::mm::frame::linked_list

Struct LinkedList 

Source 
pub struct LinkedList<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
    pub front: Option<ReprPtr<MetaSlot, MetadataAsLink<M>>>,
    pub back: Option<ReprPtr<MetaSlot, MetadataAsLink<M>>>,
    pub size: usize,
    pub list_id: u64,
}
Expand description

A linked list of frames.

Two key features that LinkedList is different from alloc::collections::LinkedList is that:

  1. It is intrusive, meaning that the links are part of the frame metadata. This allows the linked list to be used without heap allocation. But it disallows a frame to be in multiple linked lists at the same time.
  2. The linked list exclusively own the frames, meaning that it takes unique pointers UniqueFrame. And other bodies cannot [from_in_use] a frame that is inside a linked list.
  3. We also allow creating cursors at a specific frame, allowing $O(1)$ removal without iterating through the list at a cost of some checks.

§Verified Properties

§Verification Design

The linked list is abstractly represented by a LinkedListOwner:

tracked struct LinkedListOwner<M: AnyFrameMeta + Repr<MetaSlotStorage>> {
    pub list: Seq<LinkOwner>,
    pub perms: Map<int, vstd_extra::cast_ptr::PointsTo<MetaSlot, Metadata<Link<M>>>>,
    pub list_id: u64,
}

§Invariant

The linked list uniquely owns the raw frames that it contains, so they cannot be used by other data structures. The frame metadata field in_list is equal to list_id for all links in the list.

   pub open spec fn inv_at(self, i: int) -> bool {
       &&& self.perms.contains_key(i)
       &&& self.perms[i].addr() == self.list[i].paddr
       &&& self.perms[i].is_init()
       &&& self.perms[i].value().wf(self.list[i])
       &&& i == 0 <==> self.perms[i].mem_contents().value().prev is None
       &&& i == self.list.len() - 1 <==> self.perms[i].value().next is None
       &&& 0 < i ==> self.perms[i].value().prev is Some && self.perms[i].value().prev.unwrap()
           == self.perms[i - 1].pptr()
       &&& i < self.list.len() - 1 ==> self.perms[i].value().next is Some
           && self.perms[i].value().next.unwrap() == self.perms[i + 1].pptr()
       &&& self.list[i].inv()
       &&& self.list[i].in_list == self.list_id
   }

   pub open spec fn inv(self) -> bool {
       forall|i: int| 0 <= i < self.list.len() ==> self.inv_at(i)
   }

§Safety

A given linked list can only have one cursor at a time, so there are no data races. The prev and next fields of the metadata for each link always points to valid links in the list, so the structure is memory safe (will not read or write invalid memory).

Fields§

§front: Option<ReprPtr<MetaSlot, MetadataAsLink<M>>>§back: Option<ReprPtr<MetaSlot, MetadataAsLink<M>>>§size: usize

The number of frames in the list.

§list_id: u64

A lazily initialized ID, used to check whether a frame is in the list. 0 means uninitialized.

Implementations§

Source§

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedList<M>

Source

pub const exec fn new() -> Self

Creates a new linked list.

Source§

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedList<M>

Source

pub exec fn size(&self) -> s : usize

with
Tracked(owner): Tracked<LinkedListOwner<M>>,
requires
self.wf(owner),
owner.inv(),
ensures
s == self.model(owner).list.len(),

Gets the number of frames in the linked list.

Source

pub exec fn is_empty(&self) -> b : bool

with
Tracked(owner): Tracked<LinkedListOwner<M>>,
requires
self.wf(owner),
owner.inv(),
ensures
b ==> self.size == 0 && self.front is None && self.back is None,
!b ==> self.size > 0 && self.front is Some && self.back is Some,

Tells if the linked list is empty.

Source

pub exec fn push_front(ptr: PPtr<Self>, frame: UniqueFrame<Link<M>>)

with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>,
requires
perm.pptr() == ptr,
perm.is_init(),
perm.mem_contents().value().wf(*old(owner)),
old(owner).inv(),
old(owner).list_id != 0,
old(frame_own).inv(),
old(frame_own).global_inv(*old(regions)),
frame.wf(*old(frame_own)),
old(frame_own).frame_link_inv(),
old(owner).list.len() < usize::MAX,
old(regions).inv(),
old(regions).slots.contains_key(old(frame_own).slot_index),
old(regions)
    .slot_owners[old(frame_own).slot_index]
    .inner_perms
    .in_list
    .is_for(old(regions).slots[old(frame_own).slot_index].value().in_list),
ensures
owner.inv(),
owner.list == old(owner).list.insert(0, frame_own.meta_own),
owner.list_id == old(owner).list_id,
frame_own.meta_own.paddr == old(frame_own).meta_own.paddr,
frame_own.meta_own.in_list == old(owner).list_id,

Pushes a frame to the front of the linked list.

§Verified Properties
§Preconditions

The list must be well-formed, with the pointers to its links’ metadata slots matching the tracked permission objects. The new frame must be active, so that it is valid to call into_raw on it inside of insert_before.

§Postconditions

The new frame is inserted at the front of the list, and the cursor is moved to the new frame. The list invariants are preserved.

§Safety

See [insert_before] for the safety guarantees.

Source

pub exec fn pop_front( ptr: PPtr<Self>, ) -> r : Option<(UniqueFrame<Link<M>>, Tracked<UniqueFrameOwner<Link<M>>>)>

with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
Tracked(owner): Tracked<LinkedListOwner<M>>,
Tracked(frame_own): Tracked<UniqueFrameOwner<Link<M>>>,
requires
old(regions).inv(),
perm.pptr() == ptr,
perm.is_init(),
perm.value().wf(owner),
owner.inv(),
old(regions).slots.contains_key(frame_to_index(owner.list[0].paddr)),
ensures
owner.list.len() == 0 ==> r.is_none(),
r.is_some() ==> r.unwrap().0.model(r.unwrap().1@).meta == owner.list[0]@,
r.is_some() ==> r.unwrap().1@.frame_link_inv(),

Pops a frame from the front of the linked list.

§Verified Properties
§Preconditions

The list must be well-formed, with the pointers to its links’ metadata slots matching the tracked permission objects. The list must be non-empty, so that the current frame is valid.

§Postconditions

The front frame is removed from the list, and the cursor is moved to the next frame. The list invariants are preserved.

§Safety

See [take_current] for the safety guarantees.

Source

pub exec fn push_back(ptr: PPtr<Self>, frame: UniqueFrame<Link<M>>)

with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>,
requires
perm.pptr() == ptr,
perm.is_init(),
perm.mem_contents().value().wf(*old(owner)),
old(owner).inv(),
old(owner).list_id != 0,
old(frame_own).inv(),
old(frame_own).global_inv(*old(regions)),
frame.wf(*old(frame_own)),
old(frame_own).frame_link_inv(),
old(owner).list.len() < usize::MAX,
old(regions).inv(),
old(regions).slots.contains_key(old(frame_own).slot_index),
old(regions)
    .slot_owners[old(frame_own).slot_index]
    .inner_perms
    .in_list
    .is_for(old(regions).slots[old(frame_own).slot_index].value().in_list),
ensures
owner.inv(),
old(owner).list.len() > 0
    ==> owner.list
        == old(owner).list.insert(old(owner).list.len() as int - 1, frame_own.meta_own),
old(owner).list.len() == 0
    ==> owner.list == old(owner).list.insert(0, frame_own.meta_own),
owner.list_id == old(owner).list_id,
frame_own.meta_own.paddr == old(frame_own).meta_own.paddr,
frame_own.meta_own.in_list == old(owner).list_id,

Pushes a frame to the back of the linked list.

§Verified Properties
§Preconditions

The list must be well-formed, with the pointers to its links’ metadata slots matching the tracked permission objects. The new frame must be active, so that it is valid to call into_raw on it inside of insert_before.

§Postconditions
  • The new frame is inserted at the back of the list, and the cursor is moved to the new frame.
  • The list invariants are preserved.
§Safety

See [insert_before] for the safety guarantees.

Source

pub exec fn pop_back( ptr: PPtr<Self>, ) -> r : Option<(UniqueFrame<Link<M>>, Tracked<UniqueFrameOwner<Link<M>>>)>

with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
Tracked(owner): Tracked<LinkedListOwner<M>>,
Tracked(frame_own): Tracked<UniqueFrameOwner<Link<M>>>,
requires
old(regions).inv(),
perm.pptr() == ptr,
perm.is_init(),
perm.mem_contents().value().wf(owner),
owner.inv(),
old(regions).slots.contains_key(frame_to_index(owner.list[owner.list.len() - 1].paddr)),
ensures
owner.list.len() == 0 ==> r.is_none(),
r.is_some()
    ==> r.unwrap().0.model(r.unwrap().1@).meta == owner.list[owner.list.len() - 1]@,
r.is_some() ==> r.unwrap().1@.frame_link_inv(),

Pops a frame from the back of the linked list.

§Verified Properties
§Preconditions
  • The list must be well-formed, with the pointers to its links’ metadata slots matching the tracked permission objects.
  • The list must be non-empty, so that the current frame is valid.
§Postconditions
  • The back frame is removed from the list, and the cursor is moved to the “ghost” non-element.
  • The list invariants are preserved.
§Safety

See [take_current] for the safety guarantees.

Source

pub exec fn contains(ptr: PPtr<Self>, frame: Paddr) -> r : bool

with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(slot_own): Tracked<&MetaSlotOwner>,
Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
requires
slot_own.inv(),
old(regions).inv(),
old(regions).slots.contains_key(frame_to_index(frame)),
old(regions).slots[frame_to_index(frame)].is_init(),
old(regions).slot_owners.contains_key(frame_to_index(frame)),
old(regions)
    .slot_owners[frame_to_index(frame)]
    .inner_perms
    .in_list
    .is_for(old(regions).slots[frame_to_index(frame)].mem_contents().value().in_list),
ensures
old(owner).list_id != 0 ==> *owner == *old(owner),

Tells if a frame is in the list.

§Verified Properties
§Preconditions
  • The list must be well-formed, with the pointers to its links’ metadata slots matching the tracked permission objects.
  • The frame must be a valid, active frame.
§Postconditions

The function returns true if the frame is in the list, false otherwise.

§Safety
  • lazy_get_id uses atomic memory accesses, so there are no data races.
  • We assume that the ID allocator has an available ID if the list previously didn’t have one, but the consequence if that is not the case is a failsafe panic.
  • Everything else conforms to the safe interface.
Source

pub exec fn cursor_mut_at(ptr: PPtr<Self>, frame: Paddr) -> r : Option<CursorMut<M>>

with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(owner): Tracked<LinkedListOwner<M>>,
Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
->
cursor_owner: Tracked<Option<CursorOwner<M>>>,
requires
old(regions).inv(),
ensures
!has_safe_slot(frame) ==> r is None,

Gets a cursor at the specified frame if the frame is in the list.

This method fails if the frame is not in the list.

§Verified Properties
§Preconditions
  • The list must be well-formed, with the pointers to its links’ metadata slots matching the tracked permission objects.
  • The frame should be raw (because it is owned by the list)
§Postconditions
  • This functions post-conditions are incomplete due to refactoring of the permission model. When complete, it will guarantee that the cursor is well-formed and points to the matching element in the list.
§Safety
  • lazy_get_id uses atomic memory accesses, so there are no data races.
  • We assume that the ID allocator has an available ID if the list previously didn’t have one, but the consequence if that is not the case is a failsafe panic.
  • Everything else conforms to the safe interface.
Source

pub exec fn cursor_front_mut(ptr: PPtr<Self>) -> r : CursorMut<M>

with
Tracked(owner): Tracked<LinkedListOwner<M>>,
Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
->
r_perm: Tracked<CursorOwner<M>>,
requires
perm.pptr() == ptr,
perm.is_init(),
perm.mem_contents().value().wf(owner),
owner.inv(),
ensures
r.wf(r_perm@),
r_perm@.inv(),
r_perm@ == CursorOwner::front_owner_spec(owner, perm),

Gets a cursor at the front that can mutate the linked list links.

If the list is empty, the cursor points to the “ghost” non-element.

§Verified Properties
§Preconditions
  • The list must be well-formed, with the pointers to its links’ metadata slots matching the tracked permission objects.
§Postconditions
  • The cursor is well-formed, with the pointers to its links’ metadata slots matching the tracked permission objects. The list invariants are preserved.
  • See CursorOwner::front_owner_spec for the precise specification.
§Safety
  • This function only uses the list permission, so there are no illegal memory accesses.
  • No data races are possible.
Source

pub exec fn cursor_back_mut( ptr: PPtr<Self>, ) -> res : (CursorMut<M>, Tracked<CursorOwner<M>>)

with
Tracked(owner): Tracked<LinkedListOwner<M>>,
Tracked(perm): Tracked<vstd::simple_pptr::PointsTo<LinkedList<M>>>,
requires
perm.pptr() == ptr,
perm.is_init(),
perm.mem_contents().value().wf(owner),
owner.inv(),
ensures
res.0.wf(res.1@),
res.1@.inv(),
res.1@ == CursorOwner::back_owner_spec(owner, perm),

Gets a cursor at the back that can mutate the linked list links.

If the list is empty, the cursor points to the “ghost” non-element.

§Verified Properties
§Preconditions
  • The list must be well-formed, with the pointers to its links’ metadata slots matching the tracked permission objects.
§Postconditions
  • The cursor is well-formed, with the pointers to its links’ metadata slots matching the tracked permission objects. The list invariants are preserved. See CursorOwner::back_owner_spec for the precise specification.
§Safety
  • This function only uses the list permission, so there are no illegal memory accesses.
  • No data races are possible.

Trait Implementations§

Source§

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Default for LinkedList<M>

Source§

exec fn default() -> Self

Source§

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> ModelOf for LinkedList<M>

§

fn model(self, owner: Self::Owner) -> <Self::Owner as View>::V

Source§

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> OwnerOf for LinkedList<M>

Source§

open spec fn wf(self, owner: Self::Owner) -> bool

{
    &&& self.front is None <==> owner.list.len() == 0
    &&& self.back is None <==> owner.list.len() == 0
    &&& owner.list.len() > 0
        ==> self.front is Some && self.front.unwrap().addr() == owner.list[0].paddr
            && owner.perms[0].pptr().addr() == self.front.unwrap().addr()
            && self.front.unwrap().ptr == owner.perms[0].points_to.pptr()
            && self.back is Some
            && self.back.unwrap().addr() == owner.list[owner.list.len() - 1].paddr
            && owner.perms[owner.list.len() - 1].pptr().addr()
                == self.back.unwrap().addr()
            && self.back.unwrap().ptr
                == owner.perms[owner.list.len() - 1].points_to.pptr()
    &&& self.size == owner.list.len()
    &&& self.list_id == owner.list_id

}
Source§

type Owner = LinkedListOwner<M>

The owner of the concrete type. The Owner must implement Inv, indicating that it must has a consistent state.

Auto Trait Implementations§

§

impl<M> Freeze for LinkedList<M>

§

impl<M> !RefUnwindSafe for LinkedList<M>

§

impl<M> Send for LinkedList<M>
where M: Send,

§

impl<M> Sync for LinkedList<M>
where M: Sync,

§

impl<M> Unpin for LinkedList<M>
where M: Unpin,

§

impl<M> UnwindSafe for LinkedList<M>
where M: UnwindSafe,

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> VERUS_SPEC__A

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

§

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> T

§

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

§

fn obeys_try_from_spec() -> bool

§

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

§

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>