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

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(),

ensures

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

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

    },

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

    },

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)),

old(self).0.level < old(self).0.guard_level,

old(owner).in_locked_range(),

len % PAGE_SIZE == 0,

old(self).0.va + len <= old(self).0.barrier_va.end,

ensures

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

res is Some
    ==> {
        &&& res.unwrap() == self.0.va
        &&& owner.level < owner.guard_level
        &&& 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

Liveness: The cursor must be within the locked range and below the guard level.
Liveness: The length must be page-aligned and less than or equal to the remaining range of the cursor.

§Postconditions

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.
If not, it will return None. The cursor may stop at any address after len bytes, but it will not move past the barrier address.

§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. The locking mechanism prevents data races.

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(self).0.level < old(self).0.guard_level,

old(owner).in_locked_range(),

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

ensures

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

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

    },

!(self.0.barrier_va.start <= va < 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

The cursor must be within the locked range and below the guard level.

§Postconditions

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

§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