Struct FrameRef 

pub struct FrameRef<'a, M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage>> {
    pub inner: ManuallyDrop<Frame<M>>,
    pub _marker: PhantomData<&'a Frame<M>>,
}

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

Fields

inner: ManuallyDrop<Frame<M>>

_marker: PhantomData<&'a Frame<M>>

Implementations

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

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

{
    &&& OwnerSubtree::implies(
        CursorOwner::<'rcu, C>::node_unlocked(guards0),
        CursorOwner::<'rcu, C>::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)

}

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

where 'a: 'rcu,

with

Tracked(owner): Tracked<&NodeOwner<C>>,
Tracked(guards): Tracked<&mut Guards>,

requires

self.inner@.invariants(*owner),

self.inner@.external_meta_wf(owner.frame_permission.resource(), ()),

old(guards).unlocked(owner.slot_vaddr()),

ensures

final(guards).lock_held(owner.slot_vaddr()),

Self::locks_preserved_except(owner.slot_vaddr(), *old(guards), *final(guards)),

owner.relate_guard(res),

Locks the page table node.

An atomic mode guard is required to

1. prevent deadlocks;
2. 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.

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

where 'a: 'rcu,

with

Tracked(owner): Tracked<&NodeOwner<C>>,
Tracked(guards): Tracked<&mut Guards>,

requires

self.inner@.invariants(*owner),

self.inner@.external_meta_wf(owner.frame_permission.resource(), ()),

old(guards).unlocked(owner.slot_vaddr()),

ensures

final(guards).lock_held(owner.slot_vaddr()),

Self::locks_preserved_except(owner.slot_vaddr(), *old(guards), *final(guards)),

owner.relate_guard(res),

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

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

with

Tracked(metadata_perm): Tracked<Option<&'a MetadataPerm>>,
Tracked(repr_perm): Tracked<&'a M::ReprPerm>,

requires

self.ptr_inv(),

{
    self.inv() && metadata_perm is None
        && typed_meta_wf::<M>(self.slot_perm(), self.metadata_perm(), *repr_perm)
        || metadata_perm is Some && self.external_meta_wf(*metadata_perm->0, *repr_perm)
},

ensures

{
    let metadata_perm = if metadata_perm is Some {
        *metadata_perm->0
    } else {
        self.metadata_perm()
    };
    ret == typed_meta_value::<M>(metadata_perm, *repr_perm)
},

Gets the metadata of this page.

Verified Properties

Preconditions

• The caller must have a valid permission for the frame.

Postconditions

• The function returns the borrowed 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.

pub exec fn start_paddr(&self) -> Paddr

requires

self.ptr_inv(),

returns

self.start_paddr_spec(),

Gets the physical address of the start of the frame.

Verified Properties

Preconditions

• Bookkeeping: takes the permission for the frame’s metadata slot.

Postconditions

• Correctness: returns the physical address of the frame.

Safety

The caller cannot obtain a frame that doesn’t have a valid permission, and this function does not mutate any state, so it is always sound to call.

pub exec fn map_level(&self) -> PagingLevel

returns

1u8,

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.

pub exec fn size(&self) -> usize

returns

PAGE_SIZE,

Gets the size of this page in bytes.

pub exec fn reference_count(&self) -> u64

with

Tracked(slot_own): Tracked<&MetaSlotOwner>,

requires

self.ptr_inv(),

self.tracked_slot_perm@.value().wf(*slot_own),

returns

slot_own.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.

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.

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.

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

requires

self.inv(),

ensures

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

Borrows a reference from the given frame.

Verified Properties

Preconditions

• Safety Invariant: Metaslot region invariants must hold.

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.

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

requires

self.ptr_inv(),

returns

self.tracked_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.)

Trait Implementations

impl<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage>> Deref for FrameRef<'_, M>

exec fn deref(&self) -> r : &Self::Target

ensures

*r == self.inner@,

type Target = Frame<M>

The resulting type after dereferencing.