ostd::mm::frame::linked_list

Struct LinkedList

pub struct LinkedList<M: AnyFrameMeta + Repr<MetaSlot>> {
    pub front: Option<ReprPtr<MetaSlot, Link<M>>>,
    pub back: Option<ReprPtr<MetaSlot, Link<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:

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.
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.
We also allow creating cursors at a specific frame, allowing $O(1)$ removal without iterating through the list at a cost of some checks.

Fields§

§front: Option<ReprPtr<MetaSlot, Link<M>>>§back: Option<ReprPtr<MetaSlot, Link<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<MetaSlot>> LinkedList<M>

Source

pub const exec fn new() -> Self

Creates a new linked list.

Source §

impl<M: AnyFrameMeta + Repr<MetaSlot>> 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 <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(owner),

owner.inv(),

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(),

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]
    .in_list
    .is_for(old(regions).slots[old(frame_own).slot_index].value().in_list),

Pushes a frame to the front of the linked list.

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)),

Pops a frame from the front of the linked list.

Source

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

with

Tracked(regions): Tracked <& mut MetaRegionOwners>,
Tracked(owner): Tracked <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(owner),

owner.inv(),

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(),

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]
    .in_list
    .is_for(old(regions).slots[old(frame_own).slot_index].value().in_list),

Pushes a frame to the back of the linked list.

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)),

Pops a frame from the back of the linked list.

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(),

slot_own.self_addr == frame_to_meta(frame),

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)]
    .in_list
    .is_for(old(regions).slots[frame_to_index(frame)].mem_contents().value().in_list),

Tells if a frame is in the list.

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 <& mut LinkedListOwner <M>>,

requires

old(regions).inv(),

frame < MAX_PADDR(),

frame % PAGE_SIZE() == 0,

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)]
    .in_list
    .is_for(old(regions).slots[frame_to_index(frame)].mem_contents().value().in_list),

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

This method fail if Self::contains returns false.

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.

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.

Trait Implementations§

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() == self.front.unwrap() && self.back is Some
            && self.back.unwrap().addr() == owner.list[owner.list.len() - 1].paddr
            && owner.perms[owner.list.len() - 1].pptr() == self.back.unwrap()
    &&& self.size == owner.list.len()
    &&& self.list_id == owner.list_id

}