Trait PageTableConfig

Source

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

Show 13 methods    // 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;
    proof fn axiom_nr_subpage_per_huge_eq_nr_entries();
    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;
    proof fn clone_ensures_concrete(
        item: Self::Item,
        pa: Paddr,
        old_regions: MetaRegionOwners,
        new_regions: MetaRegionOwners,
        res: Self::Item,
    );
    proof fn item_roundtrip(
        item: Self::Item,
        paddr: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    );
    proof fn clone_requires_concrete(
        item: Self::Item,
        pa: Paddr,
        level: PagingLevel,
        prop: PageProperty,
        regions: MetaRegionOwners,
    );

    // Provided methods
    open spec fn LEADING_BITS_spec() -> usize { ... }
    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 Item: RCClone

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

proof fn axiom_nr_subpage_per_huge_eq_nr_entries()

ensures

Self::C::BASE_PAGE_SIZE() / Self::C::PTE_SIZE() == NR_ENTRIES,

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),

res.0 % crate::specs::arch::mm::PAGE_SIZE == 0,

res.0 < crate::specs::arch::mm::MAX_PADDR,

res.0 % crate::mm::page_table::cursor::page_size(res.1) == 0,

res.0 + crate::mm::page_table::cursor::page_size(res.1)
    <= crate::specs::arch::mm::MAX_PADDR,

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

the [super::PageFlags::AVAIL1] flag is the same as that returned from PageTableConfig::item_into_raw.

Source

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

returns

Self::item_from_raw_spec(paddr, level, prop),

Source

proof fn clone_ensures_concrete( item: Self::Item, pa: Paddr, old_regions: MetaRegionOwners, new_regions: MetaRegionOwners, res: Self::Item, )

requires

item.clone_ensures(old_regions, new_regions, res),

Self::item_into_raw_spec(item).0 == pa,

res == item,

new_regions.inv(),

new_regions.slots =~= old_regions.slots,

new_regions.slot_owners.dom() =~= old_regions.slot_owners.dom(),

ensures

forall |i: usize| {
    i != frame_to_index(pa)
        ==> (#[trigger] new_regions.slot_owners[i] == old_regions.slot_owners[i])
},

new_regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.value()
    == old_regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.value() + 1,

new_regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.id()
    == old_regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.id(),

new_regions.slot_owners[frame_to_index(pa)].inner_perms.storage
    == old_regions.slot_owners[frame_to_index(pa)].inner_perms.storage,

new_regions.slot_owners[frame_to_index(pa)].inner_perms.vtable_ptr
    == old_regions.slot_owners[frame_to_index(pa)].inner_perms.vtable_ptr,

new_regions.slot_owners[frame_to_index(pa)].inner_perms.in_list
    == old_regions.slot_owners[frame_to_index(pa)].inner_perms.in_list,

new_regions.slot_owners[frame_to_index(pa)].paths_in_pt
    == old_regions.slot_owners[frame_to_index(pa)].paths_in_pt,

new_regions.slot_owners[frame_to_index(pa)].self_addr
    == old_regions.slot_owners[frame_to_index(pa)].self_addr,

new_regions.slot_owners[frame_to_index(pa)].raw_count
    == old_regions.slot_owners[frame_to_index(pa)].raw_count,

new_regions.slot_owners[frame_to_index(pa)].usage
    == old_regions.slot_owners[frame_to_index(pa)].usage,

Proves that clone_ensures for Self::Item implies concrete per-field properties on MetaRegionOwners. Each PageTableConfig implementor proves this by unfolding its MappedItem::clone_ensures → Frame::clone_ensures. Proves that after clone, the slot at frame_to_index(pa) has the expected per-field properties. Implementors unfold their MappedItem::clone_ensures to Frame::clone_ensures and connect pa to the frame’s internal pointer address.

Source

proof fn item_roundtrip( item: Self::Item, paddr: Paddr, level: PagingLevel, prop: PageProperty, )

ensures

Self::item_into_raw_spec(item) == (paddr, level, prop)
    <==> Self::item_from_raw_spec(paddr, level, prop) == item,

Source

proof fn clone_requires_concrete( item: Self::Item, pa: Paddr, level: PagingLevel, prop: PageProperty, regions: MetaRegionOwners, )

requires

regions.inv(),

Self::item_from_raw_spec(pa, level, prop) == item,

crate::mm::frame::meta::has_safe_slot(pa),

regions.slots.contains_key(frame_to_index(pa)),

regions.slot_owners.contains_key(frame_to_index(pa)),

regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.value() > 0,

regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.value() + 1
    < crate::specs::mm::frame::meta_owners::REF_COUNT_MAX,

ensures

item.clone_requires(regions),

Proves item.clone_requires(regions) from the concrete frame-slot facts delivered by metaregion_sound plus the non-saturation bound propagated from Cursor::query. Implementors unfold their MappedItem::clone_requires to Frame::clone_requires and connect pa to the frame’s internal pointer address.

Provided Methods§

Source

open spec fn LEADING_BITS_spec() -> usize

{ 0 }

The leading bits [48, 64) of every virtual address managed by this config.

Concretely, a mapping m in this page table has m.va_range.start / 2^48 == LEADING_BITS_spec(). For non-sign-extended configurations (e.g. UserPtConfig) this is 0. For x86-64 kernel PT it is 0xffff (sign-extended high half). The type is wide enough to carry arbitrary bit patterns, so the model can accommodate future configurations that place their managed range at a non-canonical fixed offset.

Combined with TOP_LEVEL_INDEX_RANGE_spec, this fully determines the managed VA range, computed as vaddr_range_bounds_spec::<Self>. Callers that previously used VADDR_RANGE_spec() should use vaddr_range_bounds_spec::<C>() directly — the inclusive (start, end_inclusive) form avoids the end == usize::MAX + 1 overflow that plagues Range<Vaddr> for sign-extended kernel configurations.

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§

Source §

Trait PageTableConfig Copy item path

§Safety

Required Associated Types§

type E: PageTableEntryTrait

type C: PagingConstsTrait

type Item: RCClone

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

proof fn axiom_nr_subpage_per_huge_eq_nr_entries()

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

§Safety

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

proof fn clone_ensures_concrete( item: Self::Item, pa: Paddr, old_regions: MetaRegionOwners, new_regions: MetaRegionOwners, res: Self::Item, )

proof fn item_roundtrip( item: Self::Item, paddr: Paddr, level: PagingLevel, prop: PageProperty, )

proof fn clone_requires_concrete( item: Self::Item, pa: Paddr, level: PagingLevel, prop: PageProperty, regions: MetaRegionOwners, )

Provided Methods§

open spec fn LEADING_BITS_spec() -> usize

open spec fn TOP_LEVEL_CAN_UNMAP_spec() -> bool

Dyn Compatibility§

Implementors§

impl PageTableConfig for UserPtConfig

type E = PageTableEntry

type C = PagingConsts

type Item = MappedItem

Trait PageTableConfig