ostd::mm::vm_space

Struct Cursor

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

Expand description

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§

Source §

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

Source

pub open spec fn query_success_requires(self) -> bool

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

Source

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.unwrap()) == Some(range)

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

    }
}

Source §

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

Source

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<'rcu, UserPtConfig>>,

requires

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

old(owner).in_locked_range(),

forall |i: usize| {
    old(regions).slot_owners.contains_key(i)
        && old(regions).slot_owners[i].inner_perms.ref_count.value()
            != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED
        ==> old(regions).slot_owners[i].inner_perms.ref_count.value() + 1
            < crate::specs::mm::frame::meta_owners::REF_COUNT_MAX
},

ensures

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

final(self).0.query_some_condition(*final(owner))
    ==> {
        &&& r is Ok
        &&& final(self).0.query_some_ensures(*final(owner), r.unwrap())

    },

!final(self).0.query_some_condition(*final(owner))
    ==> {
        &&& r is Ok
        &&& final(self).0.query_none_ensures(*final(owner), r.unwrap())

    },

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

forall |e: EntryOwner<UserPtConfig>| {
    #[trigger] e.inv() && e.metaregion_sound(*old(regions))
        ==> e.metaregion_sound(*final(regions))
},

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.

Source

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<'rcu, UserPtConfig>>,

requires

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

ensures

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

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

res is Some
    ==> {
        &&& res.unwrap() == 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.

Source

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<'rcu, UserPtConfig>>,

requires

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

old(owner).in_locked_range(),

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,

Jump to the virtual address.

This function will move the cursor to the given virtual address. If the target address is not in the locked range, it will return an error.

§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.

§Panics

This method panics if the target address is not aligned to the page size.

§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.

Source