pub exec fn store_pte<E: PageTableEntryTrait>(
ptr: ArrayPtr<E, NR_ENTRIES>,
new_val: E,
ordering: Ordering,
)Expand description
with
Tracked(perm): Tracked<&mut vstd_extra::array_ptr::PointsTo<E, NR_ENTRIES>>,old(perm).addr() == ptr.addr(),0 <= ptr.index < NR_ENTRIES,old(perm).is_init_all(),perm.value()[ptr.index as int] == new_val,perm.value() == old(perm).value().update(ptr.index as int, new_val),perm.addr() == old(perm).addr(),perm.is_init_all(),Stores a page table entry with an atomic instruction.
§Verification Design
We axiomatize this function as a store operation in the array that represents the page table node.
§Preconditions
- The pointer must be a valid pointer to the array that represents the page table node.
- The array must be initialized so that the verifier knows that it remains initialized after the store.
§Postconditions
- The new value is stored in 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.