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>
impl<'rcu, A: InAtomicMode> Cursor<'rcu, A>
Sourcepub open spec fn invariants(
self,
owner: CursorOwner<'rcu, UserPtConfig>,
regions: MetaRegionOwners,
guards: Guards<'rcu, UserPtConfig>,
) -> bool
pub open spec fn invariants( self, owner: CursorOwner<'rcu, UserPtConfig>, regions: MetaRegionOwners, guards: Guards<'rcu, UserPtConfig>, ) -> bool
{
&&& self.0.inv()
&&& self.0.wf(owner)
&&& owner.inv()
&&& regions.inv()
&&& owner.children_not_locked(guards)
&&& owner.nodes_locked(guards)
&&& owner.relate_region(regions)
&&& !owner.popped_too_high
}Sourcepub open spec fn query_success_requires(self) -> bool
pub open spec fn query_success_requires(self) -> bool
{ self.0.barrier_va.start <= self.0.va < self.0.barrier_va.end }Sourcepub open spec fn query_success_ensures(
self,
view: CursorView<UserPtConfig>,
range: Range<Vaddr>,
item: Option<MappedItem>,
) -> bool
pub open spec fn query_success_ensures( self, view: CursorView<UserPtConfig>, range: Range<Vaddr>, item: Option<MappedItem>, ) -> bool
{
if view.present() {
let found_item = view.query_item_spec();
&&& range.start == found_item.va_range.start
&&& range.end == found_item.va_range.end
&&& item is Some
&&& meta_to_frame(item.unwrap().frame.ptr.addr()) == found_item.pa_range.start
} else {
&&& range.start == self.0.va
&&& item is None
}
}Sourcepub exec fn query(&mut self) -> r : Result<(Range<Vaddr>, Option<MappedItem>), Error>
pub exec fn query(&mut self) -> r : Result<(Range<Vaddr>, Option<MappedItem>), Error>
Tracked(owner): Tracked <& mut CursorOwner <'rcu,UserPtConfig>>,
Tracked(regions): Tracked <& mut MetaRegionOwners>,
Tracked(guards): Tracked <& mut Guards <'rcu,UserPtConfig>>,old(self).invariants(*old(owner), *old(regions), *old(guards)),self.invariants(*owner, *regions, *guards),self.query_success_requires()
==> {
&&& r is Ok
&&& self.query_success_ensures(self.0.model(*owner), r.unwrap().0, r.unwrap().1)
},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
In addition to the standard well-formedness conditions, the function will give an error if the cursor is outside of the locked range.
§Postconditions
If the cursor is valid, the result of the lookup is given by query_success_ensures.
The mapping that is returned corresponds to the abstract mapping given by query_item_spec.
Sourcepub exec fn find_next(&mut self, len: usize) -> res : Option<Vaddr>
pub exec fn find_next(&mut self, len: usize) -> res : Option<Vaddr>
Tracked(owner): Tracked <& mut CursorOwner <'rcu,UserPtConfig>>,
Tracked(regions): Tracked <& mut MetaRegionOwners>,
Tracked(guards): Tracked <& mut Guards <'rcu,UserPtConfig>>,old(owner).inv(),old(self).0.wf(*old(owner)),old(regions).inv(),old(self).0.level < old(self).0.guard_level,old(self).0.inv(),old(owner).in_locked_range(),old(owner).children_not_locked(*old(guards)),old(owner).nodes_locked(*old(guards)),old(owner).relate_region(*old(regions)),!old(owner).popped_too_high,len % PAGE_SIZE() == 0,old(self).0.va + len <= old(self).0.barrier_va.end,owner.inv(),self.0.wf(*owner),regions.inv(),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.
§Panics
Panics if the length is longer than the remaining range of the cursor.
Sourcepub exec fn jump(&mut self, va: Vaddr) -> Result<(), Error>
pub exec fn jump(&mut self, va: Vaddr) -> Result<(), Error>
Tracked(owner): Tracked <& mut CursorOwner <'rcu,UserPtConfig>>,
Tracked(regions): Tracked <& mut MetaRegionOwners>,
Tracked(guards): Tracked <& mut Guards <'rcu,UserPtConfig>>,old(owner).inv(),old(self).0.wf(*old(owner)),old(self).0.level < old(self).0.guard_level,old(self).0.inv(),old(owner).in_locked_range(),old(owner).children_not_locked(*old(guards)),old(owner).nodes_locked(*old(guards)),old(owner).relate_region(*old(regions)),Jump to the virtual address.