PageTableConfig

ostd::mm::page_table

Trait PageTableConfig 

Source 
pub unsafe trait PageTableConfig:
    Clone
    + Debug
    + Send
    + Sync
    + 'static {
    type E: PageTableEntryTrait;
    type C: PagingConstsTrait;
    type Item: Clone;

    // Required methods
    spec fn TOP_LEVEL_INDEX_RANGE_spec() -> Range<usize>;
    exec fn TOP_LEVEL_INDEX_RANGE() -> r : Range<usize>;
    exec fn TOP_LEVEL_CAN_UNMAP() -> b : bool;
    spec fn item_into_raw_spec(
        item: Self::Item,
    ) -> (Paddr, PagingLevel, PageProperty);
    exec fn item_into_raw(item: Self::Item) -> res : (Paddr, PagingLevel, PageProperty);
    spec fn item_from_raw_spec(
        paddr: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    ) -> Self::Item;
    exec fn item_from_raw(
        paddr: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    ) -> Self::Item;

    // Provided method
    open spec fn TOP_LEVEL_CAN_UNMAP_spec() -> bool { ... }
}
Expand description

The configurations of a page table.

It abstracts away both the usage and the architecture specifics from the general page table implementation. For examples:

  • the managed virtual address range;
  • the trackedness of physical mappings;
  • the PTE layout;
  • the number of page table levels, etc.

§Safety

The implementor must ensure that the item_into_raw and item_from_raw are implemented correctly so that:

  • item_into_raw consumes the ownership of the item;
  • if the provided raw form matches the item that was consumed by item_into_raw, item_from_raw restores the exact item that was consumed by item_into_raw.

Required Associated Types§

Source

type E: PageTableEntryTrait

The type of the page table entry.

Source

type C: PagingConstsTrait

The paging constants.

Source

type Item: Clone

The item that can be mapped into the virtual memory space using the page table.

Usually, this item is a [crate::mm::Frame], which we call a “tracked” frame. The page table can also do “untracked” mappings that only maps to certain physical addresses without tracking the ownership of the mapped physical frame. The user of the page table APIs can choose by defining this type and the corresponding methods item_into_raw and item_from_raw.

Required Methods§

Source

spec fn TOP_LEVEL_INDEX_RANGE_spec() -> Range<usize>

The index range at the top level (C::NR_LEVELS) page table.

When configured with this value, the PageTable instance will only be allowed to manage the virtual address range that is covered by this range. The range can be smaller than the actual allowed range specified by the hardware MMU (limited by C::ADDRESS_WIDTH).

Source

exec fn TOP_LEVEL_INDEX_RANGE() -> r : Range<usize>

ensures
r == Self::TOP_LEVEL_INDEX_RANGE_spec(),
Source

exec fn TOP_LEVEL_CAN_UNMAP() -> b : bool

ensures
b == Self::TOP_LEVEL_CAN_UNMAP_spec(),
Source

spec fn item_into_raw_spec(item: Self::Item) -> (Paddr, PagingLevel, PageProperty)

Consumes the item and returns the physical address, the paging level, and the page property.

The ownership of the item will be consumed, i.e., the item will be forgotten after this function is called.

Source

exec fn item_into_raw(item: Self::Item) -> res : (Paddr, PagingLevel, PageProperty)

ensures
1 <= res.1 <= NR_LEVELS(),
res == Self::item_into_raw_spec(item),
Source

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

Restores the item from the physical address and the paging level.

There could be transformations after PageTableConfig::item_into_raw and before PageTableConfig::item_from_raw, which include:

  • splitting and coalescing the items, for example, splitting one item into 512 level - 1 items with and contiguous physical addresses;
  • protecting the items, for example, changing the page property.

Splitting and coalescing maintains ownership rules, i.e., if one physical address is within the range of one item, after splitting/ coalescing, there should be exactly one item that contains the address.

§Safety

The caller must ensure that:

  • the physical address and the paging level represent a page table item or part of it (as described above);
  • either the ownership of the item is properly transferred to the return value, or the return value is wrapped in a core::mem::ManuallyDrop that won’t outlive the original item.

A concrete trait implementation may require the caller to ensure that

Source

exec fn item_from_raw( paddr: Paddr, level: PagingLevel, prop: PageProperty, ) -> Self::Item

Provided Methods§

Source

open spec fn TOP_LEVEL_CAN_UNMAP_spec() -> bool

{ true }

If we can remove the top-level page table entries.

This is for the kernel page table, whose second-top-level page tables need 'static lifetime to be shared with user page tables. Other page tables do not need to set this to false.

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§