Skip to main content

PagingConstsTrait

ostd::mm

Trait PagingConstsTrait 

Source 
pub trait PagingConstsTrait:
    Clone
    + Debug
    + Send
    + Sync
    + 'static {

Show 14 methods    // Required methods
    spec fn BASE_PAGE_SIZE_spec() -> usize;
    exec fn BASE_PAGE_SIZE() -> res : usize;
    spec fn NR_LEVELS_spec() -> PagingLevel;
    exec fn NR_LEVELS() -> res : PagingLevel;
    spec fn HIGHEST_TRANSLATION_LEVEL_spec() -> PagingLevel;
    exec fn HIGHEST_TRANSLATION_LEVEL() -> PagingLevel;
    spec fn PTE_SIZE_spec() -> usize;
    exec fn PTE_SIZE() -> res : usize;
    spec fn ADDRESS_WIDTH_spec() -> usize;
    exec fn ADDRESS_WIDTH() -> res : usize;
    spec fn VA_SIGN_EXT_spec() -> bool;
    exec fn VA_SIGN_EXT() -> bool;
    proof fn lemma_paging_consts_requirements();

    // Provided method
    proof fn lemma_paging_consts_properties() { ... }

}
Expand description

A minimal set of constants that determines the paging system. This provides an abstraction over most paging modes in common architectures.

Required Methods§

Source

spec fn BASE_PAGE_SIZE_spec() -> usize

Source

exec fn BASE_PAGE_SIZE() -> res : usize

returns
Self::BASE_PAGE_SIZE(),

The smallest page size. This is also the page size at level 1 page tables.

Source

spec fn NR_LEVELS_spec() -> PagingLevel

Source

exec fn NR_LEVELS() -> res : PagingLevel

returns
Self::NR_LEVELS(),

The number of levels in the page table. The numbering of levels goes from deepest node to the root node. For example, the level 1 to 5 on AMD64 corresponds to Page Tables, Page Directory Tables, Page Directory Pointer Tables, Page-Map Level-4 Table, and Page-Map Level-5 Table, respectively.

Source

spec fn HIGHEST_TRANSLATION_LEVEL_spec() -> PagingLevel

Source

exec fn HIGHEST_TRANSLATION_LEVEL() -> PagingLevel

returns
Self::HIGHEST_TRANSLATION_LEVEL(),

The highest level that a PTE can be directly used to translate a VA. This affects the the largest page size supported by the page table.

Source

spec fn PTE_SIZE_spec() -> usize

Source

exec fn PTE_SIZE() -> res : usize

returns
Self::PTE_SIZE(),

The size of a PTE.

Source

spec fn ADDRESS_WIDTH_spec() -> usize

Source

exec fn ADDRESS_WIDTH() -> res : usize

returns
Self::ADDRESS_WIDTH(),

The address width may be BASE_PAGE_SIZE.ilog2() + NR_LEVELS * IN_FRAME_INDEX_BITS. If it is shorter than that, the higher bits in the highest level are ignored.

Source

spec fn VA_SIGN_EXT_spec() -> bool

Source

exec fn VA_SIGN_EXT() -> bool

returns
Self::VA_SIGN_EXT(),

Whether virtual addresses are sign-extended.

The sign bit of a Vaddr is the bit at index PagingConstsTrait::ADDRESS_WIDTH - 1. If this constant is true, bits in Vaddr that are higher than the sign bit must be equal to the sign bit. If an address violates this rule, both the hardware and OSTD should reject it.

Otherwise, if this constant is false, higher bits must be zero.

Regardless of sign extension, Vaddr is always not signed upon calculation. That means, 0xffff_ffff_ffff_0000 < 0xffff_ffff_ffff_0001 is true.

Source

proof fn lemma_paging_consts_requirements()

ensures
0 < Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() <= Self::BASE_PAGE_SIZE(),
0 < Self::BASE_PAGE_SIZE(),
is_pow2(Self::BASE_PAGE_SIZE() as int),
Self::NR_LEVELS() > 0,
is_pow2(Self::PTE_SIZE() as int),
0 < Self::PTE_SIZE() <= Self::BASE_PAGE_SIZE(),
0 < Self::ADDRESS_WIDTH() < usize::BITS,
Self::BASE_PAGE_SIZE().ilog2()
    + (Self::BASE_PAGE_SIZE() / Self::PTE_SIZE()).ilog2() * (Self::NR_LEVELS() - 1)
    <= Self::ADDRESS_WIDTH(),
Self::BASE_PAGE_SIZE() == PAGE_SIZE,
Self::NR_LEVELS() == NR_LEVELS,
Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() == NR_ENTRIES,

The requirements of the paging constants so that the memory management system can work correctly.

NOTE: The postcondition is designed to be minimal, to actually be used in proofs, call lemma_paging_consts_properties instead to get all the properties that are derived from the requirements.

FIXME： General architecture support. All configs in vostd use the same value for the per-config NR_LEVELS() as the architecture-level constant NR_LEVELS (= 4 for x86_64). This is implicit in the cursor framework: CursorOwner::inv() hardcodes self.level <= NR_LEVELS (const) for cursors over any C: PagingConstsTrait, so a config whose NR_LEVELS_spec() exceeded NR_LEVELS would be unusable. This lemma exposes that equality as a usable fact so generic proofs can chain level != C::NR_LEVELS_spec() to level < NR_LEVELS (e.g. Cursor::find_next_impl’s PageTable-branch gate ⟹ CursorMut::take_next’s replace_cur_entry discharge).

Provided Methods§

Source

proof fn lemma_paging_consts_properties()

ensures
0 < Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() <= Self::BASE_PAGE_SIZE(),
0 < Self::BASE_PAGE_SIZE(),
is_pow2(Self::BASE_PAGE_SIZE() as int),
Self::NR_LEVELS() > 0,
is_pow2(Self::PTE_SIZE() as int),
0 < Self::PTE_SIZE() <= Self::BASE_PAGE_SIZE(),
0 < Self::ADDRESS_WIDTH() < usize::BITS,
Self::BASE_PAGE_SIZE().ilog2()
    + (Self::BASE_PAGE_SIZE() / Self::PTE_SIZE()).ilog2() * (Self::NR_LEVELS() - 1)
    <= Self::ADDRESS_WIDTH(),
Self::BASE_PAGE_SIZE() == PAGE_SIZE,
Self::NR_LEVELS() == NR_LEVELS,
Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() == NR_ENTRIES,

The derived properties of the paging constants.

NOTE: Implementations of PagingConstsTrait do not need to implement this lemma, the proof is automatically inherited from the default implementation.

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§