load_pte

ostd::mm::page_table

Function load_pte 

Source 
pub exec fn load_pte<E: PageTableEntryTrait>(
    ptr: ArrayPtr<E, NR_ENTRIES>,
    ordering: Ordering,
) -> pte : E
Expand description
with
Tracked(perm): Tracked<&vstd_extra::array_ptr::PointsTo<E, NR_ENTRIES>>,
requires
perm.is_init(ptr.index as int),
perm.addr() == ptr.addr(),
0 <= ptr.index < NR_ENTRIES,
returns
perm.value()[ptr.index as int],

Loads a page table entry with an atomic instruction.

§Verification Design

§Preconditions

  • The pointer must be a valid pointer to the array that represents the page table node.
  • The array must be initialized at the target index.

§Postconditions

  • The value is loaded from the array at the given index.

§Safety

  • We require the caller to provide a permission token to ensure that this function is only called on a valid array and the pointer is in bounds.
  • Like an AtomicUsize::load in normal Rust, this function assumes that the value being loaded is an integer (and therefore can be safely cloned). We model the PTE as an abstract type, but in all actual implementations it is an integer. Importantly, it does not include any data that is unsafe to duplicate.