ostd::mm::frame::linked_list

Struct LinkedList

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

§Example

To create metadata types that allows linked list links, wrap the metadata type in Link:

use ostd::{
    mm::{frame::{linked_list::{Link, LinkedList}, Frame}, FrameAllocOptions},
    impl_untyped_frame_meta_for,
};

#[derive(Debug)]
struct MyMeta { mark: usize }

type MyFrame = Frame<Link<MyMeta>>;

impl_untyped_frame_meta_for!(MyMeta);

let alloc_options = FrameAllocOptions::new();
let frame1 = alloc_options.alloc_frame_with(Link::new(MyMeta { mark: 1 })).unwrap();
let frame2 = alloc_options.alloc_frame_with(Link::new(MyMeta { mark: 2 })).unwrap();

let mut list = LinkedList::new();
list.push_front(frame1.try_into().unwrap());
list.push_front(frame2.try_into().unwrap());

let mut cursor = list.cursor_front_mut();
assert_eq!(cursor.current_meta().unwrap().mark, 2);
cursor.move_next();
assert_eq!(cursor.current_meta().unwrap().mark, 1);

§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 list_id: u64,
}

The raw slot and storage permissions for each link are parked in the global MetaRegionOwners, while LinkedListOwner owns the corresponding type-specific Link<M>::ReprPerm. Cursor accessors borrow these independent components together when projecting a Link<M>.

§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. The per-link well-formedness against the region (pointer/permission wiring, next/prev pointer chain) is captured by LinkedListOwner::relate_region (opaque, with per-position LinkedListOwner::relate_region_at). The cursor exposes this via CursorOwner::wf_with_region and CursorMut::wf_region.

§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<MetaSlotStorage, Link<M>>>§back: Option<ReprPtr<MetaSlotStorage, 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<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 == 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(&mut self, frame: UniqueFrame<Link<M>>)

with

Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>,

requires

old(self).wf_region(*old(owner), *old(regions)),

old(owner).relate_region(*old(regions)),

frame.inv(),

old(frame_own).inv(),

frame.wf_with_region(*old(frame_own), *old(regions)),

frame.frame_link_inv(*old(frame_own), *old(regions)),

old(regions).inv(),

ensures

final(self).wf_region(*final(owner), *final(regions)),

final(owner).inv(),

final(owner).relate_region(*final(regions)),

final(regions).inv(),

final(owner).list == old(owner).list.insert(0, final(frame_own).meta_own),

old(owner).list_id != 0 ==> final(owner).list_id == old(owner).list_id,

final(owner).list_id != 0,

final(frame_own).meta_own.slot_vaddr == old(frame_own).meta_own.slot_vaddr,

final(frame_own).meta_own.in_list == final(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. The list invariants are preserved.

§Safety

See [insert_before] for the safety guarantees.

Source

pub exec fn pop_front(&mut self) -> r : Option<UniqueFrame<Link<M>>>

with

Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
->
frame_owner: Tracked<Option<UniqueFrameOwner<Link<M>>>>,

requires

old(regions).inv(),

old(self).wf_region(*old(owner), *old(regions)),

old(owner).relate_region(*old(regions)),

ensures

final(regions).inv(),

final(owner).inv(),

final(owner).relate_region(*final(regions)),

final(self).wf_region(*final(owner), *final(regions)),

final(owner).list_id == old(owner).list_id,

r is Some == (old(owner).list.len() > 0),

r is Some == frame_owner@ is Some,

r matches Some(
    frame,
) ==> (frame_owner@ matches Some(
    fo,
) ==> {
    &&& final(owner).list == old(owner).list.remove(0)
    &&& fo.meta_own@ == old(owner).list[0]@
    &&& frame.inv()
    &&& fo.inv()
    &&& frame.wf(fo)
    &&& frame.wf_with_region(fo, *final(regions))
    &&& frame.frame_link_inv(fo, *final(regions))

}),

r is None
    ==> *final(owner) == *old(owner) && *final(self) == *old(self)
        && *final(regions) == *old(regions),

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.

§Postconditions

The list invariants are preserved.
Returns the front frame and its owner, or None if the list is empty.

§Safety

See [take_current] for the safety guarantees.

Source

pub exec fn push_back(&mut self, frame: UniqueFrame<Link<M>>)

with

Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>,

requires

old(self).wf_region(*old(owner), *old(regions)),

old(owner).relate_region(*old(regions)),

frame.inv(),

old(frame_own).inv(),

frame.wf_with_region(*old(frame_own), *old(regions)),

frame.frame_link_inv(*old(frame_own), *old(regions)),

old(regions).inv(),

ensures

final(self).wf_region(*final(owner), *final(regions)),

final(owner).inv(),

final(owner).relate_region(*final(regions)),

final(regions).inv(),

final(owner).list
    == old(owner).list.insert(old(owner).list.len() as int, final(frame_own).meta_own),

old(owner).list_id != 0 ==> final(owner).list_id == old(owner).list_id,

final(owner).list_id != 0,

final(frame_own).meta_own.slot_vaddr == old(frame_own).meta_own.slot_vaddr,

final(frame_own).meta_own.in_list == final(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.
The list invariants are preserved.

§Safety

See [insert_before] for the safety guarantees.

Source

pub exec fn pop_back(&mut self) -> r : Option<UniqueFrame<Link<M>>>

with

Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
->
frame_owner: Tracked<Option<UniqueFrameOwner<Link<M>>>>,

requires

old(regions).inv(),

old(self).wf_region(*old(owner), *old(regions)),

old(owner).relate_region(*old(regions)),

ensures

final(regions).inv(),

final(owner).inv(),

final(owner).relate_region(*final(regions)),

final(self).wf_region(*final(owner), *final(regions)),

final(owner).list_id == old(owner).list_id,

(r is Some) == (old(owner).list.len() > 0),

(r is Some) == (frame_owner@ is Some),

r matches Some(
    frame,
) ==> (frame_owner@ matches Some(
    fo,
) ==> {
    &&& final(owner).list == old(owner).list.remove(old(owner).list.len() - 1)
    &&& fo.meta_own@ == old(owner).list[old(owner).list.len() - 1]@
    &&& frame.inv()
    &&& fo.inv()
    &&& frame.wf(fo)
    &&& frame.wf_with_region(fo, *final(regions))
    &&& frame.frame_link_inv(fo, *final(regions))

}),

r is None
    ==> *final(owner) == *old(owner) && *final(self) == *old(self)
        && *final(regions) == *old(regions),

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.

§Postconditions

Returns the back frame and its owner, or None if the list is empty.
The list invariants are preserved.

§Safety

See [take_current] for the safety guarantees.

Source

pub exec fn contains(&mut self, frame: Paddr) -> r : bool

with

Tracked(regions): Tracked<&MetaRegionOwners>,
Tracked(owner): Tracked<&LinkedListOwner<M>>,

requires

regions.inv(),

old(self).wf(*owner),

owner.relate_region(*regions),

ensures

(valid_frame_paddr(frame)
    && exists |i: int| {
        0 <= i < owner.list.len()
            && #[trigger] meta_to_index(owner.list[i].slot_vaddr)
                == frame_to_index(frame)
    }) ==> r,

returns

valid_frame_paddr(frame)
    && regions.slot_owners[frame_to_index(frame)].in_list_perm.value()
        == final(self).list_id,

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 list owner must relate its links to the region permissions.

§Postconditions

The result is true exactly when the frame address is valid and its region-owned in_list tag equals the list’s ID after lazy initialization.
A valid frame in the owner’s list always returns true.

§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(&mut self, frame: Paddr) -> r : Option<CursorMut<'_, M>>

with

Tracked(regions): Tracked<&MetaRegionOwners>,
Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
->
cursor_owner: Tracked<Option<CursorOwner<M>>>,

requires

regions.inv(),

old(self).wf_region(*old(owner), *regions),

old(owner).relate_region(*regions),

list_registry_ok(*regions, *old(owner)),

old(owner).list_id != 0,

ensures

!valid_frame_paddr(frame) ==> r is None,

r is Some == cursor_owner@ is Some,

(r is Some)
    == (valid_frame_paddr(frame)
        && exists |i: int| {
            0 <= i < old(owner).list.len()
                && #[trigger] meta_to_index(old(owner).list[i].slot_vaddr)
                    == frame_to_index(frame)
        }),

r is None
    ==> {
        &&& *final(owner) == *old(owner)
        &&& *final(self) == *old(self)
        &&& final(self).wf_region(*final(owner), *regions)
        &&& final(owner).inv()

    },

r matches Some(
    cursor,
) ==> (cursor_owner@ matches Some(
    co,
) ==> {
    &&& co.list_own == *old(owner)
    &&& 0 <= co.index < co.list_own.list.len()
    &&& meta_to_index(co.list_own.list[co.index].slot_vaddr) == frame_to_index(frame)
    &&& cursor.wf_region(co, *regions)
    &&& co.wf_with_region(*regions)
    &&& cursor.wf(co)
    &&& co.inv()
    &&& *cursor.list == *old(self)
    &&& *final(self) == *final(cursor.list)

}),

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 list owner must match the list and region permissions, and its membership registry must be consistent with the region’s in_list tags.
The list must already have a non-zero ID: lazy_get_id does not yet model freshness against the region’s in_list tags for a fresh list.

§Postconditions

A cursor is returned exactly when the valid frame belongs to the list. Its owner has an in-range index matching the frame, and the cursor is well-formed with the region permissions.
The returned cursor and its tracked owner are either both present or both absent.

§Safety

lazy_get_id uses atomic memory accesses, so there are no data races.

Source

pub exec fn cursor_front_mut(&mut self) -> r : CursorMut<'_, M>

ensures

r.current == old(self).front,

*r.list == *old(self),

*final(self) == *final(r.list),

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

§Safety

This function is written in safe Rust and there is no undefined behavior.

Source

pub exec fn cursor_back_mut(&mut self) -> r : CursorMut<'_, M>

ensures

r.current == old(self).back,

*r.list == *old(self),

*final(self) == *final(r.list),

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

§Safety

This function is written in safe Rust and there is no undefined behavior.

Source §

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

Source

pub exec fn drop( self, Tracked(owner): Tracked<&mut LinkedListOwner<M>>, Tracked(regions): Tracked<&mut MetaRegionOwners>, )

requires

self.wf(*old(owner)),

old(owner).inv(),

old(regions).inv(),

forall |i: int| {
    0 <= i < old(owner).list.len()
        ==> {
            let idx = meta_to_index(old(owner).list[i].slot_vaddr);
            &&& old(regions).contains(idx)
            &&& old(regions).ref_count(idx) == REF_COUNT_UNIQUE
            &&& old(regions).slot_owners[idx].paths_in_pt.is_empty()

        }
},

forall |i: int, j: int| {
    0 <= i < j < old(owner).list.len()
        ==> meta_to_index(old(owner).list[i].slot_vaddr)
            != meta_to_index(old(owner).list[j].slot_vaddr)
},

old(owner).relate_region(*old(regions)),

ensures

final(owner).list.len() == 0,

forall |idx: int| {
    (forall |i: int| {
        0 <= i < old(owner).list.len()
            ==> idx != meta_to_index(old(owner).list[i].slot_vaddr)
    })
        ==> {
            &&& final(regions).slot_owners[idx].usage
                == old(regions).slot_owners[idx].usage
            &&& final(regions).slot_owners[idx].slot_vaddr
                == old(regions).slot_owners[idx].slot_vaddr
            &&& final(regions).slot_owners[idx].paths_in_pt
                == old(regions).slot_owners[idx].paths_in_pt

        }
},

final(regions).slots.dom() =~= old(regions).slots.dom(),

final(regions).inv(),

Releases every frame owned by the list.

§Verified Properties

Requires matching list ownership and region permissions, with every list frame uniquely owned and absent from page tables. Empties the list owner, preserves the region invariant, and leaves unrelated frames’ usage, metadata addresses, and page-table ownership unchanged.

Source §

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

Source

pub open spec fn wf_region( self, owner: LinkedListOwner<M>, regions: MetaRegionOwners, ) -> 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->0.addr() == owner.list[0].slot_vaddr
            && owner.meta_pptr_at(regions, 0).addr() == self.front->0.addr()
            && self.back is Some
            && self.back->0.addr() == owner.list[owner.list.len() - 1].slot_vaddr
            && owner.meta_pptr_at(regions, owner.list.len() - 1).addr()
                == self.back->0.addr()
    &&& self.size == owner.list.len()
    &&& self.list_id == owner.list_id

}

Region-based analog of LinkedList::wf: the front/back pointer facts are stated directly over the region-owned slot pointers.

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->0.addr() == owner.list[0].slot_vaddr
            && self.back is Some
            && self.back->0.addr() == owner.list[owner.list.len() - 1].slot_vaddr
    &&& self.size == owner.list.len()
    &&& self.list_id == owner.list_id

}

Structural well-formedness of the LinkedList against its owner: size, list_id, and front/back addresses match. The per-link pointer-permission facts (pptr/ptr equality against the front/back) live in wf_region, which sources them from MetaRegionOwners.

Source §