Entry

ostd::mm::page_table

Struct Entry 

Source 
pub struct Entry<'rcu, C: PageTableConfig> {
    pub pte: C::E,
    pub idx: usize,
    pub node: PPtr<PageTableGuard<'rcu, C>>,
}

Fields§

§pte: C::E

The page table entry.

We store the page table entry here to optimize the number of reads from the node. We cannot hold a &mut E reference to the entry because that other CPUs may modify the memory location for accessed/dirty bits. Such accesses will violate the aliasing rules of Rust and cause undefined behaviors.

§idx: usize

The index of the entry in the node.

§node: PPtr<PageTableGuard<'rcu, C>>

The node that contains the entry.

Implementations§

Source§

impl<'rcu, C: PageTableConfig> Entry<'rcu, C>

Source

pub open spec fn new_spec( pte: C::E, idx: usize, node: PPtr<PageTableGuard<'rcu, C>>, ) -> Self

{ Self { pte, idx, node } }
Source

pub exec fn new(pte: C::E, idx: usize, node: PPtr<PageTableGuard<'rcu, C>>) -> Self

Source§

impl<'a, 'rcu, C: PageTableConfig> Entry<'rcu, C>

Source

pub exec fn is_none(&self) -> bool

Returns if the entry does not map to anything.

Source

pub exec fn is_node(&self) -> bool

with
Tracked(owner): Tracked <EntryOwner <C>>,
Tracked(parent_owner): Tracked <& NodeOwner <C>>,
Tracked(guard_perm): Tracked <& GuardPerm <'rcu,C>>,
requires
owner.inv(),
self.wf(owner),
guard_perm.addr() == self.node.addr(),
parent_owner.relate_guard_perm(*guard_perm),
parent_owner.inv(),

Returns if the entry maps to a page table node.

Source

pub exec fn to_ref(&self) -> res : ChildRef<'rcu, C>

with
Tracked(owner): Tracked <& EntryOwner <C>>,
Tracked(parent_owner): Tracked <& NodeOwner <C>>,
Tracked(regions): Tracked <& mut MetaRegionOwners>,
Tracked(guard_perm): Tracked <& GuardPerm <'rcu,C>>,
requires
self.wf(*owner),
owner.inv(),
old(regions).inv(),
parent_owner.level == owner.parent_level,
guard_perm.addr() == self.node.addr(),
guard_perm.is_init(),
guard_perm.value().inner.inner@.ptr.addr() == parent_owner.meta_perm.addr(),
guard_perm.value().inner.inner@.ptr.addr() == parent_owner.meta_perm.points_to.addr(),
guard_perm.value().inner.inner@.wf(*parent_owner),
parent_owner.meta_perm.is_init(),
parent_owner.meta_perm.wf(),
parent_owner.inv(),
owner.is_node() ==> owner.node.unwrap().relate_region(*old(regions)),
ensures
regions.inv(),
res.wf(*owner),
owner.is_node() ==> owner.node.unwrap().relate_region(*regions),

Gets a reference to the child.

Source

pub exec fn protect(&mut self, op: impl FnOnce(PageProperty) -> PageProperty)

with
Tracked(owner): Tracked <& mut EntryOwner <C>>,
Tracked(parent_owner): Tracked <& mut NodeOwner <C>>,
Tracked(guard_perm): Tracked <& mut GuardPerm <'rcu,C>>,
requires
old(owner).inv(),
old(self).wf(*old(owner)),
old(parent_owner).inv(),
old(self).node.addr() == old(guard_perm).addr(),
old(parent_owner).relate_guard_perm(*old(guard_perm)),
op.requires((old(self).pte.prop(),)),
old(owner).is_frame(),
ensures
owner.inv(),
self.wf(*owner),
parent_owner.inv(),
parent_owner.relate_guard_perm(*guard_perm),
guard_perm.addr() == old(guard_perm).addr(),
owner.is_frame(),

Operates on the mapping properties of the entry.

It only modifies the properties if the entry is present.

Source

pub exec fn replace(&mut self, new_child: Child<C>) -> res : Child<C>

with
Tracked(regions): Tracked <& mut MetaRegionOwners>,
Tracked(owner): Tracked <& EntryOwner <C>>,
Tracked(new_owner): Tracked <& EntryOwner <C>>,
Tracked(parent_owner): Tracked <& mut NodeOwner <C>>,
Tracked(guard_perm): Tracked <& mut GuardPerm <'rcu,C>>,
requires
old(self).wf(*owner),
owner.inv(),
new_child.wf(*new_owner),
new_owner.inv(),
old(parent_owner).inv(),
old(regions).inv(),
owner.is_node() ==> owner.node.unwrap().relate_region(*old(regions)),
old(guard_perm).addr() == old(self).node.addr(),
old(parent_owner).relate_guard_perm(*old(guard_perm)),
ensures
parent_owner.inv(),
parent_owner.relate_guard_perm(*guard_perm),
guard_perm.pptr() == old(guard_perm).pptr(),
guard_perm.value().inner.inner@.ptr.addr()
    == old(guard_perm).value().inner.inner@.ptr.addr(),
regions.inv(),
self.wf(*new_owner),
new_owner.inv(),
res.wf(*owner),
owner.is_node() ==> owner.node.unwrap().relate_region(*regions),

Replaces the entry with a new child.

The old child is returned.

§Panics

The method panics if the level of the new child does not match the current node.

Source

pub exec fn alloc_if_none<A: InAtomicMode>( &mut self, guard: &'rcu A, ) -> res : Option<PPtr<PageTableGuard<'rcu, C>>>

with
Tracked(owner): Tracked <& mut OwnerSubtree <C>>,
Tracked(regions): Tracked <& mut MetaRegionOwners>,
Tracked(guards): Tracked <& mut Guards <'rcu,C>>,
Tracked(parent_guard_perm): Tracked <& mut GuardPerm <'rcu,C>>,
->
guard_perm: Tracked <Option <GuardPerm <'rcu,C>>>,
requires
old(owner).inv(),
old(self).wf(old(owner).value),
old(regions).inv(),
ensures
old(owner).value.is_absent()
    ==> {
        &&& res is Some
        &&& owner.value.is_node()
        &&& guard_perm@ is Some
        &&& guard_perm@.unwrap().addr() == res.unwrap().addr()
        &&& owner.level == old(owner).level
        &&& owner.value.parent_level == old(owner).value.parent_level
        &&& owner.value.node.unwrap().relate_guard_perm(guard_perm@.unwrap())

    },
!old(owner).value.is_absent()
    ==> {
        &&& res is None
        &&& *owner == *old(owner)

    },
forall |i: usize| old(guards).lock_held(i) ==> guards.lock_held(i),
parent_guard_perm.addr() == old(parent_guard_perm).addr(),
parent_guard_perm.is_init(),
parent_guard_perm.value().inner.inner@.ptr.addr()
    == old(parent_guard_perm).value().inner.inner@.ptr.addr(),
owner.inv(),
regions.inv(),

Allocates a new child page table node and replaces the entry with it.

If the old entry is not none, the operation will fail and return None. Otherwise, the lock guard of the new child page table node is returned.

Source

pub exec fn split_if_mapped_huge<A: InAtomicMode>( &mut self, guard: &'rcu A, ) -> res : Option<PPtr<PageTableGuard<'rcu, C>>>

with
Tracked(owner): Tracked <& mut OwnerSubtree <C>>,
Tracked(parent_owner): Tracked <& mut NodeOwner <C>>,
Tracked(regions): Tracked <& mut MetaRegionOwners>,
Tracked(guards): Tracked <& mut Guards <'rcu,C>>,
Tracked(guard_perm): Tracked <& mut GuardPerm <'rcu,C>>,
requires
old(regions).inv(),
old(owner).inv(),
old(self).wf(old(owner).value),
old(self).node.addr() == old(guard_perm).addr(),
old(guard_perm).is_init(),
old(parent_owner).relate_guard_perm(*old(guard_perm)),
old(parent_owner).inv(),
ensures
old(owner).value.is_frame()
    ==> {
        &&& res is Some
        &&& owner.value.is_node()
        &&& owner.level == old(owner).level
        &&& parent_owner.relate_guard_perm(*guard_perm)
        &&& guards.guards.contains_key(res.unwrap().addr())
        &&& guards.guards[res.unwrap().addr()] is Some
        &&& guards.guards[res.unwrap().addr()].unwrap().pptr() == res.unwrap()
        &&& owner
            .value
            .node
            .unwrap()
            .relate_guard_perm(guards.guards[res.unwrap().addr()].unwrap())
        &&& owner.value.node.unwrap().meta_perm.addr() == res.unwrap().addr()

    },
!old(owner).value.is_frame()
    ==> {
        &&& res is None
        &&& *owner == *old(owner)

    },
owner.inv(),
regions.inv(),
parent_owner.inv(),
guard_perm.pptr() == old(guard_perm).pptr(),
guard_perm.value().inner.inner@.ptr.addr()
    == old(guard_perm).value().inner.inner@.ptr.addr(),

Splits the entry to smaller pages if it maps to a huge page.

If the entry does map to a huge page, it is split into smaller pages mapped by a child page table node. The new child page table node is returned.

If the entry does not map to a untracked huge page, the method returns None.

Source

pub exec fn new_at(guard: PPtr<PageTableGuard<'rcu, C>>, idx: usize) -> res : Self

with
Tracked(owner): Tracked <& EntryOwner <C>>,
Tracked(parent_owner): Tracked <& NodeOwner <C>>,
Tracked(guard_perm): Tracked <& GuardPerm <'rcu,C>>,
requires
owner.inv(),
parent_owner.inv(),
guard_perm.addr() == guard.addr(),
parent_owner.relate_guard_perm(*guard_perm),
idx < NR_ENTRIES(),
owner.match_pte(parent_owner.children_perm.value()[idx as int], owner.parent_level),
ensures
res.wf(*owner),
res.node.addr() == guard_perm.addr(),

Create a new entry at the node with guard.

§Safety

The caller must ensure that the index is within the bounds of the node.

Trait Implementations§

Source§

impl<'rcu, C: PageTableConfig> OwnerOf for Entry<'rcu, C>

Source§

open spec fn wf(self, owner: Self::Owner) -> bool

{
    &&& self.idx < NR_ENTRIES()
    &&& owner.match_pte(self.pte, owner.parent_level)
    &&& self.pte.paddr() % PAGE_SIZE() == 0
    &&& self.pte.paddr() < MAX_PADDR()

}
Source§

type Owner = EntryOwner<C>

The owner of the concrete type. The Owner must implement Inv, indicating that it must has a consistent state.

Auto Trait Implementations§

§

impl<'rcu, C> Freeze for Entry<'rcu, C>
where <C as PageTableConfig>::E: Freeze,

§

impl<'rcu, C> !RefUnwindSafe for Entry<'rcu, C>

§

impl<'rcu, C> Send for Entry<'rcu, C>

§

impl<'rcu, C> Sync for Entry<'rcu, C>

§

impl<'rcu, C> Unpin for Entry<'rcu, C>
where <C as PageTableConfig>::E: Unpin, C: Unpin,

§

impl<'rcu, C> !UnwindSafe for Entry<'rcu, C>

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> VERUS_SPEC__A

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

§

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> T

§

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

§

fn obeys_try_from_spec() -> bool

§

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

§

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>