ostd::mm::frame

Struct FrameRef

pub struct FrameRef<'a, M: AnyFrameMeta> {
    pub inner: ManuallyDrop<Frame<M>>,
    pub _marker: PhantomData<&'a Frame<M>>,
}

Expand description

A struct that can work as &'a Frame<M>.

Fields§

§inner: ManuallyDrop<Frame<M>>§_marker: PhantomData<&'a Frame<M>>

Implementations§

Source §

impl<'a, C: PageTableConfig> FrameRef<'a, PageTablePageMeta<C>>

Source

pub open spec fn locks_preserved_except<'rcu>( addr: usize, guards0: Guards<'rcu, C>, guards1: Guards<'rcu, C>, ) -> bool

{
    &&& OwnerSubtree::implies(
        CursorOwner::node_unlocked(guards0),
        CursorOwner::node_unlocked_except(guards1, addr),
    )
    &&& forall |i: usize| guards0.lock_held(i) ==> guards1.lock_held(i)
    &&& forall |i: usize| guards0.unlocked(i) && i != addr ==> guards1.unlocked(i)

}

Source

pub exec fn lock<'rcu, A: InAtomicMode>( self, _guard: &'rcu A, ) -> res : PPtr<PageTableGuard<'rcu, C>>
where 'a: 'rcu,

with

Tracked(owner): Tracked<&NodeOwner<C>>,
Tracked(guards): Tracked<&mut Guards<'rcu, C>>,
->
guard_perm: Tracked<GuardPerm<'rcu, C>>,

requires

self.inner@.invariants(*owner),

old(guards).unlocked(owner.meta_perm.addr()),

ensures

guards.lock_held(owner.meta_perm.addr()),

Self::locks_preserved_except(owner.meta_perm.addr(), *old(guards), *guards),

res.addr() == guard_perm@.addr(),

owner.relate_guard_perm(guard_perm@),

Locks the page table node.

An atomic mode guard is required to

prevent deadlocks;
provide a lifetime ('rcu) that the nodes are guaranteed to outlive.

§Verification Design

As of when we verified this library, we didn’t have a spin lock implementation, so we axiomatize what happens when it’s successful.

Source

pub exec fn make_guard_unchecked<'rcu, A: InAtomicMode>( self, _guard: &'rcu A, ) -> res : PPtr<PageTableGuard<'rcu, C>>
where 'a: 'rcu,

with

Tracked(owner): Tracked<&NodeOwner<C>>,
Tracked(guards): Tracked<&mut Guards<'rcu, C>>,
->
guard_perm: Tracked<GuardPerm<'rcu, C>>,

requires

self.inner@.invariants(*owner),

old(guards).unlocked(owner.meta_perm.addr()),

ensures

guards.lock_held(owner.meta_perm.addr()),

Self::locks_preserved_except(owner.meta_perm.addr(), *old(guards), *guards),

res.addr() == guard_perm@.addr(),

owner.relate_guard_perm(guard_perm@),

Creates a new PageTableGuard without checking if the page table lock is held.

§Safety

This function must be called if this task logically holds the lock.

Calling this function when a guard is already created is undefined behavior unless that guard was already forgotten.

Methods from Deref<Target = Frame<M>>§

Source

pub exec fn meta(&self) -> &'a M

with

Tracked(perm): Tracked<&'a PointsTo<MetaSlot, Metadata<M>>>,

requires

self.ptr.addr() == perm.addr(),

self.ptr == perm.points_to.pptr(),

perm.is_init(),

perm.wf(&perm.inner_perms),

returns

perm.value().metadata,

Gets the metadata of this page.

§Verified Properties

§Preconditions

The caller must have a valid permission for the frame.

§Postconditions

The function returns the metadata of the frame.

§Safety

By requiring the caller to provide a typed permission, we ensure that the metadata is of type M. While a non-verified caller cannot be trusted to obey this interface, all functions that return a Frame<M> also return an appropriate permission.

Source

pub exec fn start_paddr(&self) -> Paddr

with

Tracked(perm): Tracked<&vstd::simple_pptr::PointsTo<MetaSlot>>,

requires

perm.addr() == self.ptr.addr(),

perm.is_init(),

FRAME_METADATA_RANGE.start <= perm.addr() < FRAME_METADATA_RANGE.end,

perm.addr() % META_SLOT_SIZE == 0,

returns

meta_to_frame(self.ptr.addr()),

Gets the physical address of the start of the frame.

Source

pub exec fn map_level(&self) -> PagingLevel

Gets the map level of this page.

This is the level of the page table entry that maps the frame, which determines the size of the frame.

Currently, the level is always 1, which means the frame is a regular page frame.

Source

pub exec fn size(&self) -> usize

Gets the size of this page in bytes.

Source

pub exec fn reference_count(&self) -> u64

with

Tracked(slot_own): Tracked<&mut MetaSlotOwner>,
Tracked(perm): Tracked<&PointsTo<MetaSlot, Metadata<M>>>,

requires

perm.addr() == self.ptr.addr(),

perm.points_to.pptr() == self.ptr,

perm.is_init(),

perm.wf(&perm.inner_perms),

perm.inner_perms.ref_count.id() == perm.points_to.value().ref_count.id(),

returns

perm.value().ref_count,

Gets the reference count of the frame.

It returns the number of all references to the frame, including all the existing frame handles (Frame, Frame<dyn AnyFrameMeta>), and all the mappings in the page table that points to the frame.

§Verified Properties

§Preconditions

Safety Invariant: Metaslot region invariants must hold.
Bookkeeping: The caller must have a valid and well-typed permission for the frame.

§Postconditions

Correctness: The function returns the reference count of the frame.

§Safety

The function is safe to call, but using it requires extra care. The reference count can be changed by other threads at any time including potentially between calling this method and acting on the result.

Source

pub exec fn borrow(&self) -> res : FrameRef<'a, M>

with

Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(perm): Tracked<&MetaPerm<M>>,

requires

old(regions).inv(),

old(regions).slot_owners[self.index()].raw_count <= 1,

old(regions).slot_owners[self.index()].self_addr == self.ptr.addr(),

perm.points_to.pptr() == self.ptr,

perm.points_to.value().wf(old(regions).slot_owners[self.index()]),

perm.is_init(),

self.inv(),

ensures

regions.inv(),

res.inner@.ptr.addr() == self.ptr.addr(),

regions.slot_owners[self.index()].raw_count == 1,

regions.slot_owners[self.index()].inner_perms
    == old(regions).slot_owners[self.index()].inner_perms,

regions.slot_owners[self.index()].self_addr
    == old(regions).slot_owners[self.index()].self_addr,

regions.slot_owners[self.index()].usage == old(regions).slot_owners[self.index()].usage,

regions.slot_owners[self.index()].path_if_in_pt
    == old(regions).slot_owners[self.index()].path_if_in_pt,

forall |i: usize| {
    i != self.index() ==> regions.slot_owners[i] == old(regions).slot_owners[i]
},

regions.slot_owners.dom() =~= old(regions).slot_owners.dom(),

Borrows a reference from the given frame.

§Verified Properties

§Preconditions

Safety Invariant: Metaslot region invariants must hold.
Bookkeeping: The caller must have a valid and well-typed permission for the frame.

§Postconditions

Safety Invariant: Metaslot region invariants hold after the call.
Correctness: The function returns a reference to the frame.
Correctness: The system context is unchanged.

Source

pub exec fn slot(&self) -> slot : &'a MetaSlot

with

Tracked(slot_perm): Tracked<&'a vstd::simple_pptr::PointsTo<MetaSlot>>,

requires

slot_perm.pptr() == self.ptr,

slot_perm.is_init(),

returns

slot_perm.value(),

Gets the metadata slot of the frame.

§Verified Properties

§Preconditions

Safety: The caller must have a valid permission for the frame.

§Postconditions

Correctness: The function returns a reference to the metadata slot of the frame.

§Safety

There is no way to mutably borrow the metadata slot, so taking an immutable reference is safe. (The fields of the slot can be mutably borrowed, but not the slot itself.)