Skip to main content

PageTableEntryTrait

ostd::mm::page_table

Trait PageTableEntryTrait 

Source 
pub trait PageTableEntryTrait:
    Clone
    + Copy
    + Debug
    + Default
    + Sized
    + Pod
    + PodOnce
    + Send
    + Sync
    + 'static {

Show 22 methods    // Required methods
    spec fn new_absent_spec() -> Self;
    exec fn new_absent() -> res : Self;
    spec fn is_present_spec(&self) -> bool;
    exec fn is_present(&self) -> bool;
    spec fn new_page_spec(
        paddr: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    ) -> Self;
    spec fn new_page_req(
        paddr: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    ) -> bool;
    exec fn new_page(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> res : Self;
    spec fn new_pt_spec(paddr: Paddr) -> Self;
    exec fn new_pt(paddr: Paddr) -> res : Self;
    spec fn paddr_spec(&self) -> Paddr;
    exec fn paddr(&self) -> res : Paddr;
    spec fn prop_spec(&self) -> PageProperty;
    exec fn prop(&self) -> PageProperty;
    spec fn set_prop_req(self, prop: PageProperty) -> bool;
    exec fn set_prop(&mut self, prop: PageProperty);
    spec fn is_last_spec(&self, level: PagingLevel) -> bool;
    exec fn is_last(&self, level: PagingLevel) -> bool;
    spec fn as_usize_spec(self) -> usize;
    proof fn lemma_page_table_entry_properties();
    proof fn lemma_paddr_is_page_aligned(self);

    // Provided methods
    exec fn as_usize(self) -> usize { ... }
    fn from_usize(pte_raw: usize) -> Self { ... }

}
Expand description

A trait that abstracts architecture-specific page table entries (PTEs).

Note that a default PTE should be a PTE that points to nothing.

Required Methods§

Source

spec fn new_absent_spec() -> Self

Source

exec fn new_absent() -> res : Self

ensures
res.paddr() % PAGE_SIZE == 0,
res.paddr() < MAX_PADDR,
!res.is_present(),
returns
Self::new_absent(),

Create a set of new invalid page table flags that indicates an absent page.

Note that currently the implementation requires an all zero PTE to be an absent PTE.

Source

spec fn is_present_spec(&self) -> bool

Source

exec fn is_present(&self) -> bool

returns
self.is_present_spec(),

Returns if the PTE points to something.

For PTEs created by Self::new_absent, this method should return false. For PTEs created by Self::new_page or Self::new_pt and modified with Self::set_prop, this method should return true.

Source

spec fn new_page_spec(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> Self

Source

spec fn new_page_req(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> bool

The preconditions for creating a new page-mapping PTE.

Source

exec fn new_page(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> res : Self

requires
paddr < MAX_PADDR,
Self::new_page_req(paddr, level, prop),
ensures
res.paddr() == paddr & !((PAGE_SIZE - 1) as usize),
paddr % PAGE_SIZE == 0 ==> res.paddr() == paddr,
res.paddr() % PAGE_SIZE == 0,
res.paddr() < MAX_PADDR,
res.is_present(),
res.is_last(level),
res.prop() == prop,
returns
Self::new_page(paddr, level, prop),

Creates a new PTE that maps to a page.

Source

spec fn new_pt_spec(paddr: Paddr) -> Self

Source

exec fn new_pt(paddr: Paddr) -> res : Self

requires
paddr < MAX_PADDR,
ensures
res.paddr() == paddr & !((PAGE_SIZE - 1) as usize),
paddr % PAGE_SIZE == 0 ==> res.paddr() == paddr,
res.paddr() % PAGE_SIZE == 0,
res.paddr() < MAX_PADDR,
res.is_present(),
forall |level: PagingLevel| !res.is_last(level),
returns
Self::new_pt(paddr),

Create a new PTE that map to a child page table.

Source

spec fn paddr_spec(&self) -> Paddr

Returns the physical address from the PTE.

The physical address recorded in the PTE is either:

  • the physical address of the next-level page table, or
  • the physical address of the page that the PTE maps to.
Source

exec fn paddr(&self) -> res : Paddr

ensures
res % PAGE_SIZE == 0,
returns
self.paddr(),
Source

spec fn prop_spec(&self) -> PageProperty

Source

exec fn prop(&self) -> PageProperty

returns
self.prop(),
Source

spec fn set_prop_req(self, prop: PageProperty) -> bool

The preconditions for setting the page property of a PTE.

Source

exec fn set_prop(&mut self, prop: PageProperty)

requires
old(self).set_prop_req(prop),
ensures
!old(self).is_present() ==> *old(self) == *final(self),
old(self).is_present()
    ==> {
        &&& final(self).prop() == prop
        &&& final(self).paddr() == old(self).paddr()
        &&& final(self).is_present()
        &&& forall |level: PagingLevel| {
            old(self).is_last(level) ==> final(self).is_last(level)
        }

    },
Source

spec fn is_last_spec(&self, level: PagingLevel) -> bool

Source

exec fn is_last(&self, level: PagingLevel) -> bool

returns
self.is_last_spec(level),

Returns if the PTE maps a page rather than a child page table.

The method needs to know the level of the page table where the PTE resides, since architectures like x86-64 have a huge bit only in intermediate levels.

Source

spec fn as_usize_spec(self) -> usize

Source

proof fn lemma_page_table_entry_properties()

ensures
Self::new_absent().paddr() % PAGE_SIZE == 0,
Self::new_absent().paddr() < MAX_PADDR,
!Self::new_absent().is_present(),
forall |level: PagingLevel| 1 < level ==> !Self::new_absent().is_last(level),
forall |paddr: Paddr, level: PagingLevel, prop: PageProperty| {
    Self::new_page_req(paddr, level, prop)
        && (prop.cache is Writeback || prop.cache is Writethrough
            || prop.cache is Uncacheable)
        ==> {
            &&& Self::new_page(paddr, level, prop).is_present()
            &&& (paddr < MAX_PADDR
                ==> Self::new_page(paddr, level, prop).paddr()
                    == paddr & !((PAGE_SIZE - 1) as usize))
            &&& (paddr < MAX_PADDR && paddr % PAGE_SIZE == 0
                ==> Self::new_page(paddr, level, prop).paddr() == paddr)
            &&& Self::new_page(paddr, level, prop).prop() == prop
            &&& Self::new_page(paddr, level, prop).is_last(level)

        }
},
forall |paddr: Paddr| {
    &&& Self::new_pt(paddr).is_present()
    &&& (paddr < MAX_PADDR
        ==> Self::new_pt(paddr).paddr() == paddr & !((PAGE_SIZE - 1) as usize))
    &&& (paddr < MAX_PADDR && paddr % PAGE_SIZE == 0
        ==> Self::new_pt(paddr).paddr() == paddr)
    &&& forall |level: PagingLevel| !Self::new_pt(paddr).is_last(level)

},

Absent (zero) PTE has well-formed paddr for match_pte.

Source

proof fn lemma_paddr_is_page_aligned(self)

ensures
self.paddr() % PAGE_SIZE == 0,

Provided Methods§

Source

exec fn as_usize(self) -> usize

returns
self.as_usize(),

Converts the PTE into a raw usize value.

Source

exec fn from_usize(pte_raw: usize) -> Self

Converts the raw usize value into a PTE.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§