Struct Cursor 

pub struct Cursor<'a, A: InAtomicMode>(pub Cursor<'a, UserPtConfig, A>);

The cursor for querying over the VM space without modifying it.

It exclusively owns a sub-tree of the page table, preventing others from reading or modifying the same sub-tree. Two read-only cursors can not be created from the same virtual address range either.

Tuple Fields

0: Cursor<'a, UserPtConfig, A>

Implementations

impl<'rcu, A: InAtomicMode> Cursor<'rcu, A>

pub open spec fn query_success_requires(self) -> bool

{ self.0.barrier_va.start <= self.0.va < self.0.barrier_va.end }

pub open spec fn query_success_ensures( self, view: CursorView<UserPtConfig>, range: Range<Vaddr>, item: Option<MappedItem>, ) -> bool

{
    if view.present() {
        &&& item is Some
        &&& view.query_item_spec(item->0) == Some(range)

    } else {
        &&& range.start == self.0.va
        &&& item is None

    }
}

impl<'rcu, A: InAtomicMode> Cursor<'rcu, A>

pub exec fn query(&mut self) -> r : Result<(Range<Vaddr>, Option<MappedItem>), Error>

with

Tracked(owner): Tracked<&mut CursorOwner<'rcu, UserPtConfig>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(guards): Tracked<&mut Guards>,

requires

old(self).0.invariants(*old(owner), *old(regions), *old(guards)),

old(self).0.query_panic_condition(*old(owner), *old(regions)) ==> may_panic(),

ensures

final(self).0.invariants(*final(owner), *final(regions), *final(guards)),

!old(self).0.query_panic_condition(*old(owner), *old(regions)),

old(owner).in_locked_range() ==> r is Ok,

r matches Ok(
    state,
) ==> final(self).0.query_some_condition(*final(owner))
    ==> final(self).0.query_some_ensures(*final(owner), state),

r matches Ok(
    state,
) ==> !final(self).0.query_some_condition(*final(owner))
    ==> final(self).0.query_none_ensures(*final(owner), state),

old(owner)@.mappings == final(owner)@.mappings,

Queries the mapping at the current virtual address.

If the cursor is pointing to a valid virtual address that is locked, it will return the virtual address range and the mapped item.

Preconditions

• All system invariants must hold
• Liveness: The function will return an error if the cursor is not within the locked range

Postconditions

• If there is a mapped item at the current virtual address ([query_some_condition]), it is returned along with the virtual address range that it maps ([query_success_ensures]).
• The mapping that is returned corresponds to the abstract mapping given by query_item_spec.
• If there is no mapped item at the current virtual address ([query_none_condition]), it returns None, and the virtual address range of the cursor’s current position.

Safety

• This function preserves all memory invariants.
• The locking mechanism prevents data races.

pub exec fn find_next(&mut self, len: usize) -> res : Option<Vaddr>

with

Tracked(owner): Tracked<&mut CursorOwner<'rcu, UserPtConfig>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(guards): Tracked<&mut Guards>,

requires

old(self).0.invariants(*old(owner), *old(regions), *old(guards)),

old(self).0.find_next_panic_condition(len) ==> may_panic(),

ensures

!old(self).0.find_next_panic_condition(len),

final(self).0.invariants(*final(owner), *final(regions), *final(guards)),

res is Some
    ==> {
        &&& res->0 == final(self).0.va
        &&& final(owner).level <= final(owner).guard_level
        &&& final(owner).in_locked_range()

    },

Moves the cursor forward to the next mapped virtual address.

If there is mapped virtual address following the current address within next len bytes, it will return that mapped address. In this case, the cursor will stop at the mapped address.

Otherwise, it will return None. And the cursor may stop at any address after len bytes.

Verified Properties

Preconditions

• Safety Invariants: The page table cursor safety invariants ([crate::mm::page_table::Cursor::invariants]) must hold before the call.
• Liveness: In order to avoid a panic, the length must be page-aligned and less than or equal to the remaining range of the cursor.

Postconditions

• Safety Invariants: Page table cursor safety invariants are preserved.
• Correctness: If there is a mapped address after the current address within the next len bytes, it will move the cursor to the next mapped address and return it.
• Correctness: If the metadata region was well-formed before the call, it will be well-formed after.

Panics

This method panics if the length is longer than the remaining range of the cursor.

Safety

This function preserves all memory invariants. Because it panics rather than move the cursor to an invalid address, it ensures that the cursor is safe to use after the call.

pub exec fn jump(&mut self, va: Vaddr) -> res : Result<(), Error>

with

Tracked(owner): Tracked<&mut CursorOwner<'rcu, UserPtConfig>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(guards): Tracked<&mut Guards>,

requires

old(self).0.invariants(*old(owner), *old(regions), *old(guards)),

old(self).0.jump_panic_condition(va) ==> may_panic(),

ensures

!old(self).0.jump_panic_condition(va),

final(self).0.invariants(*final(owner), *final(regions), *final(guards)),

final(self).0.barrier_va.start <= va < final(self).0.barrier_va.end
    ==> {
        &&& res is Ok
        &&& final(self).0.va == va

    },

!(final(self).0.barrier_va.start <= va < final(self).0.barrier_va.end) ==> res is Err,

Jumps to the virtual address.

If the target address is out of the range, this method will return Err.

Panics

This method panics if the address has bad alignment.

Verified Properties

Preconditions

• Safety Invariants: The page table cursor safety invariants ([crate::mm::page_table::Cursor::invariants]) must hold before the call.
• Liveness: The function will panic if the target va is not aligned to the base page size.

Postconditions

• Safety Invariants: Page table cursor safety invariants are preserved.
• Correctness: If the target va is within the cursor’s locked range, the result will be Ok and the cursor’s virtual address will be set to va.
• Correctness: If the target va is outside the locked range, the result is Err.
• Correctness: If the metadata region was well-formed before the call, it will be well-formed after.

Safety

This function preserves all memory invariants. Because it throws an error rather than move the cursor to an invalid address, it ensures that the cursor is safe to use after the call. The locking mechanism prevents data races.

pub exec fn virt_addr(&self) -> Vaddr

returns

self.0.va,

Get the virtual address of the current slot.