Skip to main content

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: RCClone;


Show 22 methods    // Required methods
    spec fn TOP_LEVEL_INDEX_RANGE_spec() -> Range<usize>;
    exec fn TOP_LEVEL_INDEX_RANGE() -> Range<usize>;
    exec fn TOP_LEVEL_CAN_UNMAP() -> bool;
    spec fn item_into_raw_spec(
        item: Self::Item,
    ) -> (Paddr, PagingLevel, PageProperty);
    exec fn item_into_raw(item: Self::Item) -> (Paddr, PagingLevel, PageProperty);
    spec fn item_from_raw_spec(
        paddr: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    ) -> Self::Item;
    unsafe fn item_from_raw(
        paddr: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    ) -> Self::Item;
    spec fn tracked(item: Self::Item) -> bool;
    spec fn item_well_formed(item: Self::Item) -> bool;
    spec fn raw_item_well_formed(
        pa: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    ) -> bool;
    proof fn lemma_raw_item_well_formed_preserved(
        pa: Paddr,
        level: PagingLevel,
        old_prop: PageProperty,
        new_prop: PageProperty,
    );
    proof fn lemma_raw_item_well_formed_split(
        pa: Paddr,
        level: PagingLevel,
        prop: PageProperty,
        child_pa: Paddr,
        child_idx: usize,
    );
    proof fn lemma_item_from_raw_well_formed(
        pa: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    );
    proof fn lemma_item_into_raw_roundtrip(
        pa: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    );
    proof fn lemma_item_from_raw_roundtrip(
        item: Self::Item,
        pa: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    );
    proof fn lemma_clone_ensures_concrete(
        item: Self::Item,
        pa: Paddr,
        old_regions: MetaRegionOwners,
        new_regions: MetaRegionOwners,
        res: Self::Item,
    );
    proof fn lemma_clone_requires_concrete(
        item: Self::Item,
        pa: Paddr,
        level: PagingLevel,
        prop: PageProperty,
        regions: MetaRegionOwners,
    );
    proof fn lemma_page_table_config_constant_requirements();

    // Provided methods
    open spec fn LEADING_BITS_spec() -> usize { ... }
    fn TOP_LEVEL_CAN_UNMAP_spec() -> bool { ... }
    fn LOCKED_END_BOUND_spec() -> int { ... }
    fn lemma_page_table_config_constant_properties() { ... }

}
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: 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>

Source

exec fn TOP_LEVEL_INDEX_RANGE() -> Range<usize>

returns
Self::TOP_LEVEL_INDEX_RANGE(),

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_CAN_UNMAP() -> bool

returns
Self::TOP_LEVEL_CAN_UNMAP(),

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.

Source

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

Source

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

requires
Self::item_well_formed(item),
ensures
1 <= level <= NR_LEVELS,
valid_frame_paddr(paddr),
paddr % page_size(level) == 0,
paddr + page_size(level) <= MAX_PADDR,
Self::raw_item_well_formed(paddr, level, prop),
Self::E::new_page_req(paddr, level, prop),
returns
Self::item_into_raw_spec(item),

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

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

Source

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

requires
valid_frame_paddr(paddr),
Self::raw_item_well_formed(paddr, level, prop),
ensures
Self::item_well_formed(res),
returns
Self::item_from_raw_spec(paddr, level, prop),

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

spec fn tracked(item: Self::Item) -> bool

Whether cloning this item bumps a slot’s refcount. For ref-counted items (e.g. MappedItem::Tracked), true; for items where clone is a no-op (e.g. MappedItem::Untracked for kernel MMIO frames), false.

Source

spec fn item_well_formed(item: Self::Item) -> bool

Per-config predicate that captures the structural well-formedness an item reconstructed via PageTableConfig::item_from_raw must satisfy. This may include both ownership invariants and restrictions on raw-only property bits.

Source

spec fn raw_item_well_formed( pa: Paddr, level: PagingLevel, prop: PageProperty, ) -> bool

Per-config predicate that captures the well-formedness of raw properties produced via PageTableConfig::item_into_raw must satisfy.

Source

proof fn lemma_raw_item_well_formed_preserved( pa: Paddr, level: PagingLevel, old_prop: PageProperty, new_prop: PageProperty, )

requires
valid_frame_paddr(pa),
Self::raw_item_well_formed(pa, level, old_prop),
Self::tracked(Self::item_from_raw(pa, level, new_prop))
    == Self::tracked(Self::item_from_raw(pa, level, old_prop)),
ensures
Self::raw_item_well_formed(pa, level, new_prop),

Changing properties without changing trackedness preserves a canonical raw item.

Source

proof fn lemma_raw_item_well_formed_split( pa: Paddr, level: PagingLevel, prop: PageProperty, child_pa: Paddr, child_idx: usize, )

requires
valid_frame_paddr(pa),
Self::raw_item_well_formed(pa, level, prop),
Self::E::new_page_req(pa, level, prop),
level > 1,
child_idx < NR_ENTRIES,
child_pa == pa + child_idx * page_size((level - 1) as PagingLevel),
ensures
Self::raw_item_well_formed(child_pa, (level - 1) as PagingLevel, prop),
Self::E::new_page_req(child_pa, (level - 1) as PagingLevel, prop),

Splitting a canonical huge-page raw item yields canonical child raw items.

Source

proof fn lemma_item_from_raw_well_formed( pa: Paddr, level: PagingLevel, prop: PageProperty, )

requires
valid_frame_paddr(pa),
Self::raw_item_well_formed(pa, level, prop),
ensures
Self::item_well_formed(Self::item_from_raw(pa, level, prop)),

The item produced by PageTableConfig::item_from_raw is well-formed.

Source

proof fn lemma_item_into_raw_roundtrip( pa: Paddr, level: PagingLevel, prop: PageProperty, )

requires
valid_frame_paddr(pa),
Self::raw_item_well_formed(pa, level, prop),
ensures
Self::item_into_raw(Self::item_from_raw(pa, level, prop)) == (pa, level, prop),

Re-encoding a canonical raw item preserves the complete raw representation.

Source

proof fn lemma_item_from_raw_roundtrip( item: Self::Item, pa: Paddr, level: PagingLevel, prop: PageProperty, )

requires
valid_frame_paddr(pa),
Self::item_well_formed(item),
Self::item_into_raw(item) == (pa, level, prop),
ensures
Self::item_from_raw(pa, level, prop) == item,

Decoding the raw representation produced from a well-formed item restores that item.

Source

proof fn lemma_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: int| {
    i != frame_to_index(pa)
        ==> (#[trigger] new_regions.slot_owners[i] == old_regions.slot_owners[i])
},
Self::tracked(item)
    ==> {
        &&& 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)].slot_vaddr
            == old_regions.slot_owners[frame_to_index(pa)].slot_vaddr
        &&& new_regions.slot_owners[frame_to_index(pa)].usage
            == old_regions.slot_owners[frame_to_index(pa)].usage

    },
!Self::tracked(item)
    ==> new_regions.slot_owners[frame_to_index(pa)]
        == old_regions.slot_owners[frame_to_index(pa)],
Self::tracked(item)
    ==> new_regions.frame_obligations
        == old_regions.frame_obligations.insert(frame_to_index(pa)),
!Self::tracked(item) ==> new_regions.frame_obligations == old_regions.frame_obligations,

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 lemma_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,
Self::raw_item_well_formed(pa, level, prop),
valid_frame_paddr(pa),
regions.slots.contains_key(frame_to_index(pa)),
regions.slot_owners.contains_key(frame_to_index(pa)),
Self::tracked(item)
    ==> regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.value() > 0,
Self::tracked(item)
    ==> regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.value()
        != REF_COUNT_UNUSED,
Self::tracked(item)
    ==> (regions.slot_owners[frame_to_index(pa)].inner_perms.ref_count.value()
        < REF_COUNT_MAX || may_panic()),
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.

Source

proof fn lemma_page_table_config_constant_requirements()

ensures
core::mem::size_of::<Self::E>() == Self::C::PTE_SIZE(),
Self::TOP_LEVEL_INDEX_RANGE().start < Self::TOP_LEVEL_INDEX_RANGE().end,
Self::TOP_LEVEL_INDEX_RANGE().end
    <= pow2(
        (Self::C::ADDRESS_WIDTH()
            - pte_index_bit_offset_spec::<Self::C>(Self::C::NR_LEVELS())) as nat,
    ),
Self::TOP_LEVEL_INDEX_RANGE().end
    * pow2(pte_index_bit_offset_spec::<Self::C>(Self::C::NR_LEVELS()) as nat)
    <= usize::MAX,
Self::LEADING_BITS_spec() != 0usize
    ==> (Self::C::VA_SIGN_EXT()
        && ((Self::TOP_LEVEL_INDEX_RANGE().start
            * pow2(pte_index_bit_offset_spec::<Self::C>(Self::C::NR_LEVELS()) as nat))
            / (pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int)) % 2 == 1),
(Self::C::VA_SIGN_EXT()
    && (((Self::TOP_LEVEL_INDEX_RANGE().start
        * pow2(pte_index_bit_offset_spec::<Self::C>(Self::C::NR_LEVELS()) as nat))
        / (pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int)) % 2 == 1))
    ==> {
        &&& Self::LEADING_BITS_spec() * 0x1_0000_0000_0000int
            == 0x1_0000_0000_0000_0000int - pow2(Self::C::ADDRESS_WIDTH() as nat)

    },
Self::LEADING_BITS_spec() < 0x1_0000_usize,
pow2(
    (Self::C::ADDRESS_WIDTH()
        - pte_index_bit_offset_spec::<Self::C>(Self::C::NR_LEVELS())) as nat,
) == NR_ENTRIES,

The requirements of the page table configuration 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_page_table_config_constant_properties instead to get all the properties that are derived from the requirements.

FIXME： General architecture support. Move properties only relevant to paging constants to PagingConstsTrait.

Provided Methods§

Source

open spec fn LEADING_BITS_spec() -> usize

{ 0 }

VERIFICATION only: 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, this fully determines the managed VA range, computed as vaddr_range_spec::<Self>. Callers that previously used VADDR_RANGE_spec() should use vaddr_range_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 }
Source

open spec fn LOCKED_END_BOUND_spec() -> int

{ 0x1_0000_0000_0000_0000int }

VERIFICATION only: Upper bound on locked_range().end for cursors of this config.

May be tighter than the structural vaddr_range_spec().1 + 1 when the actual sources of cursor ranges (e.g. the kvirt allocator for KernelPtConfig) draw from a sub-window of the configured VA range. KernelPtConfig overrides this to FRAME_METADATA_BASE_VADDR, which the kvirt_alloc_range_bounds axiom enforces. This bound is what allows the cursor’s move_forward proof to discharge prefix.idx[NR_LEVELS - 1] + 1 < NR_ENTRIES at the top-level boundary — the structural bound only gives <= NR_ENTRIES for configurations whose TOP_LEVEL_INDEX_RANGE.end == NR_ENTRIES.

Default: usize::MAX + 1 (no tightening over the structural bound).

Source

proof fn lemma_page_table_config_constant_properties()

ensures
Self::TOP_LEVEL_INDEX_RANGE().end <= NR_ENTRIES,
core::mem::size_of::<Self::E>() == Self::C::PTE_SIZE(),
Self::TOP_LEVEL_INDEX_RANGE().start < Self::TOP_LEVEL_INDEX_RANGE().end,
Self::TOP_LEVEL_INDEX_RANGE().end
    <= pow2(
        (Self::C::ADDRESS_WIDTH()
            - pte_index_bit_offset_spec::<Self::C>(Self::C::NR_LEVELS())) as nat,
    ),
Self::TOP_LEVEL_INDEX_RANGE().end
    * pow2(pte_index_bit_offset_spec::<Self::C>(Self::C::NR_LEVELS()) as nat)
    <= usize::MAX,
Self::LEADING_BITS_spec() != 0usize
    ==> (Self::C::VA_SIGN_EXT()
        && ((Self::TOP_LEVEL_INDEX_RANGE().start
            * pow2(pte_index_bit_offset_spec::<Self::C>(Self::C::NR_LEVELS()) as nat))
            / (pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int)) % 2 == 1),
(Self::C::VA_SIGN_EXT()
    && (((Self::TOP_LEVEL_INDEX_RANGE().start
        * pow2(pte_index_bit_offset_spec::<Self::C>(Self::C::NR_LEVELS()) as nat))
        / (pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int)) % 2 == 1))
    ==> {
        &&& Self::LEADING_BITS_spec() * 0x1_0000_0000_0000int
            == 0x1_0000_0000_0000_0000int - pow2(Self::C::ADDRESS_WIDTH() as nat)

    },
Self::LEADING_BITS_spec() < 0x1_0000_usize,
pow2(
    (Self::C::ADDRESS_WIDTH()
        - pte_index_bit_offset_spec::<Self::C>(Self::C::NR_LEVELS())) as nat,
) == NR_ENTRIES,

NOTE: Implementations of PageTableConfig 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§

Source§

impl PageTableConfig for UserPtConfig

Source§

type E = PageTableEntry

Source§

type C = PagingConsts

Source§

type Item = MappedItem