Skip to main content

PageTable

ostd::mm::page_table

Struct PageTable 

Source 
pub struct PageTable<C: PageTableConfig> {
    pub root: PageTableNode<C>,
}
Expand description

A handle to a page table. A page table can track the lifetime of the mapped physical pages.

Fields§

§root: PageTableNode<C>

Implementations§

Source§

impl PageTable<KernelPtConfig>

Source

pub open spec fn create_user_pt_panic_condition( root_owner: NodeOwner<KernelPtConfig>, ) -> bool

{
    exists |i: usize| {
        KernelPtConfig::TOP_LEVEL_INDEX_RANGE().start <= i
            < KernelPtConfig::TOP_LEVEL_INDEX_RANGE().end
            && {
                let pte = root_owner.children_perm.value()[i as int];
                ||| !pte.is_present()
                ||| pte.is_last(root_owner.level())

            }
    }
}

Panic condition for Self::create_user_page_table: Some kernel root entry at index i in TOP_LEVEL_INDEX_RANGE is not a page table node (i.e., is absent or maps a huge frame).

Source§

impl<C: PageTableConfig> PageTable<C>

Source

pub open spec fn relates_owner( &self, owner: PageTableOwner<C>, regions: MetaRegionOwners, ) -> bool

{
    &&& owner.inv()
    &&& self.root.ptr.addr() == owner.0.value().node().slot_vaddr()
    &&& owner.metaregion_sound(regions)

}

Relates this executable page-table handle to its tracked ownership tree.

Source

pub exec fn empty() -> Self

Create a new empty page table.

Useful for the IOMMU page tables only.

Source

pub exec fn empty_with_owner<'rcu>() -> r : Self

with
Tracked(owner): Tracked<&mut Option<PageTableOwner<C>>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(guards): Tracked<&mut Guards>,
requires
old(regions).inv(),
ensures
final(owner)@ is Some,
final(owner)@->0.inv(),
(final(owner)@->0).0.value().is_node(),
r.root.ptr.addr() == (final(owner)@->0).0.value().node().slot_vaddr(),
(final(owner)@->0).0.value().metaregion_sound(*final(regions)),
final(regions).inv(),
final(guards).unlocked((final(owner)@->0).0.value().node().slot_vaddr()),
final(guards).guards == old(guards).guards,
old(regions)
    .contains(
        crate::specs::mm::frame::mapping::frame_to_index(
            (final(owner)@->0).0.value().meta_slot_paddr()->0,
        ),
    ),
!final(regions)
    .contains(
        crate::specs::mm::frame::mapping::frame_to_index(
            (final(owner)@->0).0.value().meta_slot_paddr()->0,
        ),
    ),
forall |i: int| {
    i
        != crate::specs::mm::frame::mapping::frame_to_index(
            (final(owner)@->0).0.value().meta_slot_paddr()->0,
        ) ==> final(regions).slot_owners[i] == old(regions).slot_owners[i]
},
forall |a: usize| old(guards).lock_held(a) ==> final(guards).lock_held(a),
forall |idx: int| (
    final(regions).slot_owners[idx].paths_in_pt
        == old(regions).slot_owners[idx].paths_in_pt
),
forall |kt: PageTableOwner<KernelPtConfig>| {
    kt.inv() && kt.metaregion_sound(*old(regions))
        ==> kt.metaregion_sound(*final(regions))
},
forall |kt: PageTableOwner<KernelPtConfig>| {
    kt.inv() && kt.metaregion_sound(*old(regions))
        ==> kt
            .0
            .subtree_satisfies(
                kt.0.value().path,
                |
                    e: crate::specs::mm::page_table::node::entry_owners::EntryOwner<
                        KernelPtConfig,
                    >,
                    p: vstd_extra::ghost_tree::TreePath<NR_ENTRIES>|
                (
                    e.meta_slot_paddr() is Some
                        ==> crate::specs::mm::frame::mapping::frame_to_index(
                            e.meta_slot_paddr()->0,
                        )
                            != crate::specs::mm::frame::mapping::frame_to_index(
                                (final(owner)@->0).0.value().meta_slot_paddr()->0,
                            )
                ),
            )
},
forall |kt: PageTableOwner<KernelPtConfig>| {
    kt.inv() && kt.metaregion_sound(*old(regions))
        ==> kt
            .0
            .subtree_satisfies(
                kt.0.value().path,
                |
                    e: crate::specs::mm::page_table::node::entry_owners::EntryOwner<
                        KernelPtConfig,
                    >,
                    p: vstd_extra::ghost_tree::TreePath<NR_ENTRIES>|
                {
                    e.is_frame() && e.parent_level > 1
                        ==> {
                            let pa = e.frame().mapped_pa;
                            let nr_pages = page_size::<PagingConsts>(e.parent_level)
                                / PAGE_SIZE;
                            forall |j: usize| {
                                0 < j < nr_pages
                                    ==> {
                                        let sub_idx = #[trigger]
                                        crate::specs::mm::frame::mapping::frame_to_index(
                                            (pa + j * PAGE_SIZE) as usize,
                                        );
                                        sub_idx
                                            != crate::specs::mm::frame::mapping::frame_to_index(
                                                (final(owner)@->0).0.value().meta_slot_paddr()->0,
                                            )
                                    }
                            }
                        }
                },
            )
},

Create a new empty page table together with its tracked ownership.

Source

pub uninterp spec fn root_paddr_spec(&self) -> Paddr

Source

pub exec fn root_paddr(&self) -> r : Paddr

returns
self.root_paddr_spec(),

The physical address of the root page table.

Obtaining the physical address of the root page table is safe, however, using it or providing it to the hardware will be unsafe since the page table node may be dropped, resulting in UAF.

Source

pub exec fn cursor_mut<'rcu, G: InAtomicMode>( &'rcu self, guard: &'rcu G, va: &Range<Vaddr>, ) -> r : Result<(CursorMut<'rcu, C, G>, Tracked<CursorOwner<'rcu, C>>), PageTableError>

with
Tracked(owner): Tracked<PageTableOwner<C>>,
Ghost(root_guard): Ghost<PageTableGuard<'rcu, C>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(guards): Tracked<&mut Guards>,
requires
self.relates_owner(owner, *old(regions)),
owner.0.value().node().relate_guard(root_guard),
0 < va.end <= C::LOCKED_END_BOUND_spec(),
ensures
Cursor::<C, G>::cursor_new_success_conditions(*va)
    ==> {
        &&& r is Ok
        &&& r.unwrap().0.0.invariants(*r.unwrap().1, *final(regions), *final(guards))
        &&& r.unwrap().1.in_locked_range()
        &&& r.unwrap().0.0.level == r.unwrap().0.0.guard_level
        &&& r.unwrap().0.0.guard_level == NR_LEVELS as PagingLevel
        &&& r.unwrap().0.0.va < r.unwrap().0.0.barrier_va.end
        &&& r.unwrap().0.0.va == va.start
        &&& r.unwrap().0.0.barrier_va == *va

    },
!Cursor::<C, G>::cursor_new_success_conditions(*va) ==> r is Err,
forall |item: C::Item| {
    CursorMut::<'rcu, C, G>::item_not_mapped(item, *old(regions))
        ==> CursorMut::<'rcu, C, G>::item_not_mapped(item, *final(regions))
},
forall |idx: int| {
    old(regions).ref_count(idx) != REF_COUNT_UNUSED
        ==> final(regions).slot_owners[idx].paths_in_pt
            == old(regions).slot_owners[idx].paths_in_pt
},
forall |idx: int| {
    old(regions).contains(idx) && old(regions).ref_count(idx) != REF_COUNT_UNUSED
        ==> final(regions).ref_count(idx) == old(regions).ref_count(idx)
            && final(regions).slot_owners[idx].usage
                == old(regions).slot_owners[idx].usage
},

Create a new cursor exclusively accessing the virtual address range for mapping.

If another cursor is already accessing the range, the new cursor may wait until the previous cursor is dropped.

Source

pub exec fn cursor<'rcu, G: InAtomicMode>( &'rcu self, guard: &'rcu G, va: &Range<Vaddr>, ) -> r : Result<(Cursor<'rcu, C, G>, Tracked<CursorOwner<'rcu, C>>), PageTableError>

with
Tracked(owner): Tracked<PageTableOwner<C>>,
Ghost(root_guard): Ghost<PageTableGuard<'rcu, C>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(guards): Tracked<&mut Guards>,
requires
self.relates_owner(owner, *old(regions)),
owner.0.value().node().relate_guard(root_guard),
0 < va.end <= C::LOCKED_END_BOUND_spec(),
ensures
Cursor::<C, G>::cursor_new_success_conditions(*va)
    ==> {
        &&& r is Ok
        &&& r.unwrap().0.invariants(*r.unwrap().1, *final(regions), *final(guards))
        &&& r.unwrap().1.in_locked_range()
        &&& r.unwrap().0.level == r.unwrap().0.guard_level
        &&& r.unwrap().0.va < r.unwrap().0.barrier_va.end
        &&& r.unwrap().0.va == va.start
        &&& r.unwrap().0.barrier_va == *va
        &&& r.unwrap().1@.as_page_table_owner() == owner
        &&& r.unwrap().1@.continuations[3].path() == owner.0.value().path

    },
!Cursor::<C, G>::cursor_new_success_conditions(*va) ==> r is Err,
forall |idx: int| {
    old(regions).ref_count(idx) != REF_COUNT_UNUSED
        ==> final(regions).slot_owners[idx].paths_in_pt
            == old(regions).slot_owners[idx].paths_in_pt
},
(forall |i: int| {
    old(regions).contains(i) && old(regions).ref_count(i) != REF_COUNT_UNUSED
        ==> old(regions).ref_count(i) + 1 < REF_COUNT_MAX
})
    ==> (forall |i: int| (
        final(regions).contains(i) && final(regions).ref_count(i) != REF_COUNT_UNUSED
            ==> final(regions).ref_count(i) + 1 < REF_COUNT_MAX
    )),
forall |idx: int| (
    final(regions).ref_count(idx) >= REF_COUNT_MAX
        ==> old(regions).ref_count(idx) == final(regions).ref_count(idx)
),
forall |idx: int| {
    old(regions).ref_count(idx) >= REF_COUNT_MAX
        ==> final(regions).ref_count(idx) == old(regions).ref_count(idx)
},

Create a new cursor exclusively accessing the virtual address range for querying.

If another cursor is already accessing the range, the new cursor may wait until the previous cursor is dropped. The modification to the mapping by the cursor may also block or be overridden by the mapping of another cursor.

Auto Trait Implementations§

§

impl<C> !RefUnwindSafe for PageTable<C>

§

impl<C> !UnwindSafe for PageTable<C>

§

impl<C> Freeze for PageTable<C>

§

impl<C> Send for PageTable<C>

§

impl<C> Sync for PageTable<C>

§

impl<C> Unpin for PageTable<C>
where C: Unpin,

§

impl<C> UnsafeUnpin for PageTable<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
§

impl<T> Conv for T

§

fn conv<T>(self) -> T
where Self: Into<T>,

Converts self into T using Into<T>. Read more
§

impl<T> FmtForward for T

§

fn fmt_binary(self) -> FmtBinary<Self>
where Self: Binary,

Causes self to use its Binary implementation when Debug-formatted.
§

fn fmt_display(self) -> FmtDisplay<Self>
where Self: Display,

Causes self to use its Display implementation when Debug-formatted.
§

fn fmt_lower_exp(self) -> FmtLowerExp<Self>
where Self: LowerExp,

Causes self to use its LowerExp implementation when Debug-formatted.
§

fn fmt_lower_hex(self) -> FmtLowerHex<Self>
where Self: LowerHex,

Causes self to use its LowerHex implementation when Debug-formatted.
§

fn fmt_octal(self) -> FmtOctal<Self>
where Self: Octal,

Causes self to use its Octal implementation when Debug-formatted.
§

fn fmt_pointer(self) -> FmtPointer<Self>
where Self: Pointer,

Causes self to use its Pointer implementation when Debug-formatted.
§

fn fmt_upper_exp(self) -> FmtUpperExp<Self>
where Self: UpperExp,

Causes self to use its UpperExp implementation when Debug-formatted.
§

fn fmt_upper_hex(self) -> FmtUpperHex<Self>
where Self: UpperHex,

Causes self to use its UpperHex implementation when Debug-formatted.
§

fn fmt_list(self) -> FmtList<Self>
where &'a Self: for<'a> IntoIterator,

Formats each item in a sequence. 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

§

impl<T> FromSpecImpl<T> for T

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> T

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

§

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

§

fn pipe<R>(self, func: impl FnOnce(Self) -> R) -> R
where Self: Sized,

Pipes by value. This is generally the method you want to use. Read more
§

fn pipe_ref<'a, R>(&'a self, func: impl FnOnce(&'a Self) -> R) -> R
where R: 'a,

Borrows self and passes that borrow into the pipe function. Read more
§

fn pipe_ref_mut<'a, R>(&'a mut self, func: impl FnOnce(&'a mut Self) -> R) -> R
where R: 'a,

Mutably borrows self and passes that borrow into the pipe function. Read more
§

fn pipe_borrow<'a, B, R>(&'a self, func: impl FnOnce(&'a B) -> R) -> R
where Self: Borrow<B>, B: 'a + ?Sized, R: 'a,

Borrows self, then passes self.borrow() into the pipe function. Read more
§

fn pipe_borrow_mut<'a, B, R>( &'a mut self, func: impl FnOnce(&'a mut B) -> R, ) -> R
where Self: BorrowMut<B>, B: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.borrow_mut() into the pipe function. Read more
§

fn pipe_as_ref<'a, U, R>(&'a self, func: impl FnOnce(&'a U) -> R) -> R
where Self: AsRef<U>, U: 'a + ?Sized, R: 'a,

Borrows self, then passes self.as_ref() into the pipe function.
§

fn pipe_as_mut<'a, U, R>(&'a mut self, func: impl FnOnce(&'a mut U) -> R) -> R
where Self: AsMut<U>, U: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.as_mut() into the pipe function.
§

fn pipe_deref<'a, T, R>(&'a self, func: impl FnOnce(&'a T) -> R) -> R
where Self: Deref<Target = T>, T: 'a + ?Sized, R: 'a,

Borrows self, then passes self.deref() into the pipe function.
§

fn pipe_deref_mut<'a, T, R>( &'a mut self, func: impl FnOnce(&'a mut T) -> R, ) -> R
where Self: DerefMut<Target = T> + Deref, T: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.deref_mut() into the pipe function.
§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

impl<A> SpecEq<Tracked<A>> for A

§

impl<T> Tap for T

§

fn tap(self, func: impl FnOnce(&Self)) -> Self

Immutable access to a value. Read more
§

fn tap_mut(self, func: impl FnOnce(&mut Self)) -> Self

Mutable access to a value. Read more
§

fn tap_borrow<B>(self, func: impl FnOnce(&B)) -> Self
where Self: Borrow<B>, B: ?Sized,

Immutable access to the Borrow<B> of a value. Read more
§

fn tap_borrow_mut<B>(self, func: impl FnOnce(&mut B)) -> Self
where Self: BorrowMut<B>, B: ?Sized,

Mutable access to the BorrowMut<B> of a value. Read more
§

fn tap_ref<R>(self, func: impl FnOnce(&R)) -> Self
where Self: AsRef<R>, R: ?Sized,

Immutable access to the AsRef<R> view of a value. Read more
§

fn tap_ref_mut<R>(self, func: impl FnOnce(&mut R)) -> Self
where Self: AsMut<R>, R: ?Sized,

Mutable access to the AsMut<R> view of a value. Read more
§

fn tap_deref<T>(self, func: impl FnOnce(&T)) -> Self
where Self: Deref<Target = T>, T: ?Sized,

Immutable access to the Deref::Target of a value. Read more
§

fn tap_deref_mut<T>(self, func: impl FnOnce(&mut T)) -> Self
where Self: DerefMut<Target = T> + Deref, T: ?Sized,

Mutable access to the Deref::Target of a value. Read more
§

fn tap_dbg(self, func: impl FnOnce(&Self)) -> Self

Calls .tap() only in debug builds, and is erased in release builds.
§

fn tap_mut_dbg(self, func: impl FnOnce(&mut Self)) -> Self

Calls .tap_mut() only in debug builds, and is erased in release builds.
§

fn tap_borrow_dbg<B>(self, func: impl FnOnce(&B)) -> Self
where Self: Borrow<B>, B: ?Sized,

Calls .tap_borrow() only in debug builds, and is erased in release builds.
§

fn tap_borrow_mut_dbg<B>(self, func: impl FnOnce(&mut B)) -> Self
where Self: BorrowMut<B>, B: ?Sized,

Calls .tap_borrow_mut() only in debug builds, and is erased in release builds.
§

fn tap_ref_dbg<R>(self, func: impl FnOnce(&R)) -> Self
where Self: AsRef<R>, R: ?Sized,

Calls .tap_ref() only in debug builds, and is erased in release builds.
§

fn tap_ref_mut_dbg<R>(self, func: impl FnOnce(&mut R)) -> Self
where Self: AsMut<R>, R: ?Sized,

Calls .tap_ref_mut() only in debug builds, and is erased in release builds.
§

fn tap_deref_dbg<T>(self, func: impl FnOnce(&T)) -> Self
where Self: Deref<Target = T>, T: ?Sized,

Calls .tap_deref() only in debug builds, and is erased in release builds.
§

fn tap_deref_mut_dbg<T>(self, func: impl FnOnce(&mut T)) -> Self
where Self: DerefMut<Target = T> + Deref, T: ?Sized,

Calls .tap_deref_mut() only in debug builds, and is erased in release builds.
§

impl<T> TryConv for T

§

fn try_conv<T>(self) -> Result<T, Self::Error>
where Self: TryInto<T>,

Attempts to convert self into T using TryInto<T>. Read more
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>