ostd::mm::frame

Struct Frame

#[repr(transparent)]
pub struct Frame<M: AnyFrameMeta> {
    pub ptr: PPtr<MetaSlot>,
    pub _marker: PhantomData<M>,
}

Expand description

A smart pointer to a frame.

A frame is a contiguous range of bytes in physical memory. The Frame type is a smart pointer to a frame that is reference-counted.

Frames are associated with metadata. The type of the metadata M is determines the kind of the frame. If M implements [AnyUFrameMeta], the frame is a untyped frame. Otherwise, it is a typed frame.

§Verification Design

Fields§

§ptr: PPtr<MetaSlot>§_marker: PhantomData<M>

Implementations§

Source §

impl<M: AnyFrameMeta> Frame<M>

Source

pub open spec fn paddr(self) -> usize

{ meta_to_frame(self.ptr.addr()) }

Source

pub open spec fn index(self) -> usize

{ frame_to_index(self.paddr()) }

Source §

impl<'a, M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Frame<M>

Source

pub exec fn from_unused(paddr: Paddr, metadata: M) -> r : Result<Self, GetFrameError>

with

Tracked(regions): Tracked<&mut MetaRegionOwners>,
->
perm: Tracked<Option<PointsTo<MetaSlot, Metadata<M>>>>,

requires

old(regions).inv(),

old(regions).slots.contains_key(frame_to_index(paddr)),

ensures

regions.inv(),

r matches Ok(
    res,
) ==> perm@ is Some
    && MetaSlot::get_from_unused_perm_spec(
        paddr,
        metadata,
        false,
        res.ptr,
        perm@.unwrap(),
    ),

r is Ok ==> MetaSlot::get_from_unused_spec(paddr, false, *old(regions), *regions),

!has_safe_slot(paddr) ==> r is Err,

Gets a Frame with a specific usage from a raw, unused page.

The caller should provide the initial metadata of the page.

If the provided frame is not truly unused at the moment, it will return an error. If wanting to acquire a frame that is already in use, use Frame::from_in_use instead.

§Verified Properties

§Preconditions

Safety Invariant: Metaslot region invariants must hold.
Bookkeeping: The slot must be available in order to get the permission. This is stronger than it needs to be; absent permissions correspond to error cases.

§Postconditions

Safety Invariant: Metaslot region invariants hold after the call.
Correctness: If successful, the function returns a pointer to the metadata slot and a permission to the slot.
Correctness: If successful, the slot is initialized with the given metadata.

§Safety

This function returns an error if paddr does not correspond to a valid slot or the slot is in use.

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

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 §

impl<M: AnyFrameMeta> Frame<M>

Source

pub exec fn from_in_use(paddr: Paddr) -> res : Result<Self, GetFrameError>

with

Tracked(regions): Tracked<&mut MetaRegionOwners>,

requires

old(regions).inv(),

old(regions).slots.contains_key(frame_to_index(paddr)),

!MetaSlot::get_from_in_use_panic_cond(paddr, *old(regions)),

ensures

regions.inv(),

res is Ok
    ==> regions.slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
        == old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
            + 1,

res matches Ok(res) ==> res.ptr == old(regions).slots[frame_to_index(paddr)].pptr(),

!has_safe_slot(paddr) ==> res is Err,

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

Gets a dynamically typed Frame from a raw, in-use page.

If the provided frame is not in use at the moment, it will return an error.

The returned frame will have an extra reference count to the frame.

§Verified Properties

§Preconditions

Safety Invariant: Metaslot region invariants must hold.
Liveness: The slot must have fewer than REF_COUNT_MAX - 1 references or the function will panic.

§Postconditions

Safety Invariant: Metaslot region invariants hold after the call.
Correctness: If successful, the function returns the frame at paddr.
Correctness: If successful, the frame has an extra reference count to the frame.
Safety: Frames other than the one at paddr are not affected by the call.

§Safety

If paddr is a valid frame address, it is safe to take a reference to the frame.
If paddr is not a valid frame address, the function will return an error.

Source §

impl<'a, M: AnyFrameMeta> Frame<M>

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,

Gets the physical address of the start of the frame.

Source

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

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.slots =~= old(regions).slots,

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

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

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

Source §

impl<C: PageTableConfig> Frame<PageTablePageMeta<C>>

Source

pub exec fn alloc<'rcu>(level: PagingLevel) -> res : Self

with

Tracked(parent_owner): Tracked<&mut NodeOwner<C>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(guards): Tracked<&Guards<'rcu, C>>,
Ghost(idx): Ghost<usize>,
->
owner: Tracked<OwnerSubtree<C>>,

requires

1 <= level < NR_LEVELS,

idx < NR_ENTRIES,

old(regions).inv(),

old(parent_owner).inv(),

ensures

regions.inv(),

parent_owner.inv(),

allocated_empty_node_owner(owner@, level),

res.ptr.addr() == owner@.value.node.unwrap().meta_perm.addr(),

guards.unlocked(owner@.value.node.unwrap().meta_perm.addr()),

MetaSlot::get_from_unused_spec(
    meta_to_frame(owner@.value.node.unwrap().meta_perm.addr()),
    false,
    *old(regions),
    *regions,
),

owner@.value.relate_region(*regions),

owner@.value.in_scope,

owner@
    .value
    .match_pte(
        C::E::new_pt_spec(meta_to_frame(owner@.value.node.unwrap().meta_perm.addr())),
        level as PagingLevel,
    ),

*parent_owner
    == old(parent_owner)
        .set_children_perm(
            idx,
            C::E::new_pt_spec(meta_to_frame(owner@.value.node.unwrap().meta_perm.addr())),
        ),

Allocates a new empty page table node.

Source §

impl<'a, M: AnyFrameMeta> Frame<M>

Source

pub proof fn lemma_from_raw_manuallydrop_inverse( raw: Paddr, frame: Self, regions0: MetaRegionOwners, regions1: MetaRegionOwners, )

requires

Self::from_raw_requires(regions0, raw),

Self::from_raw_ensures(regions0, regions1, raw, frame),

<Self as TrackDrop>::constructor_requires(frame, regions1),

ensures

forall |regions2: MetaRegionOwners| {
    <Self as TrackDrop>::constructor_ensures(frame, regions1, regions2)
        ==> regions2 == regions0
},

Source §

impl<'a, M: AnyFrameMeta> Frame<M>

Source

pub open spec fn from_raw_requires(regions: MetaRegionOwners, paddr: Paddr) -> bool

{
    &&& regions.slot_owners.contains_key(frame_to_index(paddr))
    &&& regions.slot_owners[frame_to_index(paddr)].raw_count == 1
    &&& regions.slot_owners[frame_to_index(paddr)].self_addr == frame_to_meta(paddr)
    &&& has_safe_slot(paddr)
    &&& regions.inv()

}

§Internal Safety Spec

This is a condition that supports unsafe Rust encapsulation. It should never be exposed to the API client.

Source

pub open spec fn from_raw_ensures( old_regions: MetaRegionOwners, new_regions: MetaRegionOwners, paddr: Paddr, r: Self, ) -> bool

{
    &&& new_regions.inv()
    &&& new_regions.slots.contains_key(frame_to_index(paddr))
    &&& new_regions.slot_owners[frame_to_index(paddr)].raw_count == 0
    &&& new_regions.slot_owners[frame_to_index(paddr)].inner_perms
        == old_regions.slot_owners[frame_to_index(paddr)].inner_perms
    &&& new_regions.slot_owners[frame_to_index(paddr)].usage
        == old_regions.slot_owners[frame_to_index(paddr)].usage
    &&& new_regions.slot_owners[frame_to_index(paddr)].path_if_in_pt
        == old_regions.slot_owners[frame_to_index(paddr)].path_if_in_pt
    &&& new_regions.slot_owners[frame_to_index(paddr)].self_addr == r.ptr.addr()
    &&& forall |i: usize| {
        i != frame_to_index(paddr)
            ==> new_regions.slot_owners[i] == old_regions.slot_owners[i]
    }
    &&& forall |i: usize| {
        i != frame_to_index(paddr)
            ==> new_regions.slots.contains_key(i) == old_regions.slots.contains_key(i)
    }
    &&& r.ptr.addr() == frame_to_meta(paddr)
    &&& r.paddr() == paddr

}

Source

pub open spec fn into_raw_pre_frame_inv(self) -> bool

{ self.inv() }

Safety Invariant: The frame’s structural invariant must hold.

Source

pub open spec fn into_raw_pre_not_unused(self, regions: MetaRegionOwners) -> bool

{ regions.slot_owners[self.index()].inner_perms.ref_count.value() != REF_COUNT_UNUSED }

Bookkeeping: The frame must be in use (not unused).

Source

pub open spec fn into_raw_post_raw_count_incremented( self, old_regions: MetaRegionOwners, new_regions: MetaRegionOwners, ) -> bool

{
    &&& new_regions.slot_owners.contains_key(self.index())
    &&& new_regions.slot_owners[self.index()].raw_count
        == (old_regions.slot_owners[self.index()].raw_count + 1) as usize

}

Correctness: The frame’s raw count is incremented.

Source

pub open spec fn into_raw_post_noninterference( self, old_regions: MetaRegionOwners, new_regions: MetaRegionOwners, ) -> bool

{
    &&& forall |i: usize| {
        i != self.index() && old_regions.slots.contains_key(i)
            ==> new_regions.slots.contains_key(i)
                && new_regions.slots[i] == old_regions.slots[i]
    }
    &&& forall |i: usize| {
        i != self.index() ==> new_regions.slot_owners[i] == old_regions.slot_owners[i]
    }
    &&& new_regions.slot_owners.dom() =~= old_regions.slot_owners.dom()

}

Safety: Frames other than this one are not affected by the call.

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Frame<M>

Source

pub open spec fn from_raw_spec(paddr: Paddr) -> Self

{
    Frame::<M> {
        ptr: PPtr::<MetaSlot>(frame_to_meta(paddr), PhantomData),
        _marker: PhantomData,
    }
}

Source §

impl<C: PageTableConfig> Frame<PageTablePageMeta<C>>

Source

pub open spec fn invariants(self, owner: NodeOwner<C>) -> bool

{
    &&& owner.inv()
    &&& self.wf(owner)

}

Trait Implementations§

Source §

impl<M: AnyFrameMeta> Clone for Frame<M>

Source §

exec fn clone(&self) -> Self

1.0.0 · Source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more

Source §

impl<M: AnyFrameMeta> Inv for Frame<M>

Source §

open spec fn inv(self) -> bool

{
    &&& self.ptr.addr() % META_SLOT_SIZE == 0
    &&& FRAME_METADATA_RANGE.start <= self.ptr.addr()
        < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
    &&& self.ptr.addr() < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR

}

Source §

impl<M: AnyFrameMeta> TrackDrop for Frame<M>

We need to keep track of when frames are forgotten with ManuallyDrop. We maintain a counter for each frame of how many times it has been forgotten (raw_count). Calling ManuallyDrop::new increments the counter. It is technically safe to forget a frame multiple times, and this will happen with read-only FrameRefs. All such references need to be dropped by the time from_raw is called. So, ManuallyDrop::drop decrements the counter when the reference is dropped, and from_raw may only be called when the counter is 1.

Source §

open spec fn constructor_requires(self, s: Self::State) -> bool

{
    &&& s.slot_owners.contains_key(frame_to_index(meta_to_frame(self.ptr.addr())))
    &&& s.inv()

}

Source §

open spec fn constructor_ensures(self, s0: Self::State, s1: Self::State) -> bool

{
    let slot_own = s0.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))];
    &&& s1.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))]
        == MetaSlotOwner {
            raw_count: (slot_own.raw_count + 1) as usize,
            ..slot_own
        }
    &&& forall |i: usize| {
        i != frame_to_index(meta_to_frame(self.ptr.addr()))
            ==> s1.slot_owners[i] == s0.slot_owners[i]
    }
    &&& s1.slots =~= s0.slots
    &&& s1.slot_owners.dom() =~= s0.slot_owners.dom()

}

Source §

proof fn constructor_spec(self, tracked s: &mut Self::State)

Source §

open spec fn drop_requires(self, s: Self::State) -> bool

{
    &&& s.slot_owners.contains_key(frame_to_index(meta_to_frame(self.ptr.addr())))
    &&& s.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count > 0

}

Source §

open spec fn drop_ensures(self, s0: Self::State, s1: Self::State) -> bool

{
    let slot_own = s0.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))];
    &&& s1.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count
        == (slot_own.raw_count - 1) as usize
    &&& forall |i: usize| {
        i != frame_to_index(meta_to_frame(self.ptr.addr()))
            ==> s1.slot_owners[i] == s0.slot_owners[i]
    }
    &&& s1.slots =~= s0.slots
    &&& s1.slot_owners.dom() =~= s0.slot_owners.dom()

}

Source §