ostd::mm::vm_space

Struct CursorMut

pub struct CursorMut<'a, A: InAtomicMode> {
    pub pt_cursor: CursorMut<'a, UserPtConfig, A>,
}

Expand description

The cursor for modifying the mappings in VM space.

It exclusively owns a sub-tree of the page table, preventing others from reading or modifying the same sub-tree.

Fields§

§pt_cursor: CursorMut<'a, UserPtConfig, A>

Implementations§

Source §

impl<'a, A: InAtomicMode> CursorMut<'a, A>

Source

pub open spec fn query_requries( cursor: Self, owner: CursorOwner<'a, UserPtConfig>, guard_perm: PointsTo<PageTableGuard<'a, UserPtConfig>>, regions: MetaRegionOwners, ) -> bool

{
    &&& cursor.pt_cursor.inner.wf(owner)
    &&& owner.inv()
    &&& regions.inv()

}

Source

pub open spec fn query_ensures( old_cursor: Self, new_cursor: Self, owner: CursorOwner<'a, UserPtConfig>, guard_perm: PointsTo<PageTableGuard<'a, UserPtConfig>>, old_regions: MetaRegionOwners, new_regions: MetaRegionOwners, r: Result<(Range<Vaddr>, Option<MappedItem>), Error>, ) -> bool

{
    &&& new_regions.inv()
    &&& new_cursor.pt_cursor.inner.wf(owner)

}

Source

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

with

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

requires

old(owner).inv(),

old(self).pt_cursor.inner.wf(*old(owner)),

old(regions).inv(),

old(self).pt_cursor.inner.inv(),

old(owner).children_not_locked(*old(guards)),

old(owner).nodes_locked(*old(guards)),

old(owner).relate_region(*old(regions)),

old(owner).in_locked_range(),

!old(owner).popped_too_high,

Queries the mapping at the current virtual address.

This is the same as Cursor::query.

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

Source

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

with

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

requires

old(owner).inv(),

old(self).pt_cursor.inner.wf(*old(owner)),

old(regions).inv(),

old(self).pt_cursor.inner.level < old(self).pt_cursor.inner.guard_level,

old(self).pt_cursor.inner.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).pt_cursor.inner.va + len <= old(self).pt_cursor.inner.barrier_va.end,

ensures

owner.inv(),

self.pt_cursor.inner.wf(*owner),

regions.inv(),

Moves the cursor forward to the next mapped virtual address.

This is the same as Cursor::find_next.

Source

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

with

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

requires

old(owner).inv(),

old(self).pt_cursor.inner.wf(*old(owner)),

old(self).pt_cursor.inner.level < old(self).pt_cursor.inner.guard_level,

old(self).pt_cursor.inner.inv(),

Jump to the virtual address.

This is the same as Cursor::jump.

Source

pub exec fn virt_addr(&self) -> r : Vaddr

Get the virtual address of the current slot.

Source

pub open spec fn map_cursor_inv( self, cursor_owner: CursorOwner<'a, UserPtConfig>, guards: Guards<'a, UserPtConfig>, regions: MetaRegionOwners, ) -> bool

{
    &&& cursor_owner.inv()
    &&& self.pt_cursor.inner.wf(cursor_owner)
    &&& self.pt_cursor.inner.inv()
    &&& cursor_owner.children_not_locked(guards)
    &&& cursor_owner.nodes_locked(guards)
    &&& cursor_owner.relate_region(regions)
    &&& !cursor_owner.popped_too_high
    &&& regions.inv()

}

Collects the invariants of the cursor, its owner, and associated tracked structures. The cursor must be well-formed with respect to its owner. This will hold before and after the call to map.

Source

pub open spec fn map_cursor_requires( self, cursor_owner: CursorOwner<'a, UserPtConfig>, ) -> bool

{
    &&& cursor_owner.in_locked_range()
    &&& self.pt_cursor.inner.level < self.pt_cursor.inner.guard_level
    &&& self.pt_cursor.inner.va < self.pt_cursor.inner.barrier_va.end

}

These conditions must hold before the call to map but may not be maintained after the call. The cursor must be within the locked range and below the guard level, but it may move outside the range if the frame being mapped is exactly the length of the remaining range.

Source

pub open spec fn map_item_requires( self, frame: UFrame, prop: PageProperty, entry_owner: EntryOwner<UserPtConfig>, ) -> bool

{
    let item = MappedItem {
        frame: frame,
        prop: prop,
    };
    let (paddr, level, prop0) = UserPtConfig::item_into_raw_spec(item);
    &&& prop == prop0
    &&& entry_owner.frame.unwrap().mapped_pa == paddr
    &&& entry_owner.frame.unwrap().prop == prop
    &&& level <= UserPtConfig::HIGHEST_TRANSLATION_LEVEL()
    &&& 1 <= level <= NR_LEVELS()
    &&& Child::Frame(paddr, level, prop0).wf(entry_owner)
    &&& self.pt_cursor.inner.va + page_size(level) <= self.pt_cursor.inner.barrier_va.end
    &&& entry_owner.inv()
    &&& self.pt_cursor.inner.va % page_size(level) == 0

}

Collects the conditions that must hold on the frame being mapped. The frame must be well-formed with respect to the entry owner. When converted into a MappedItem, its physical address must also match, and its level must be between 1 and the highest translation level.

Source

pub open spec fn map_item_ensures( self, frame: UFrame, prop: PageProperty, old_cursor_view: CursorView<UserPtConfig>, cursor_view: CursorView<UserPtConfig>, ) -> bool

{
    let item = MappedItem {
        frame: frame,
        prop: prop,
    };
    let (paddr, level, prop0) = UserPtConfig::item_into_raw_spec(item);
    cursor_view == old_cursor_view.map_spec(paddr, page_size(level), prop)
}

The result of a call to map. Constructs a Mapping from the frame being mapped and the cursor’s current virtual address. The page table’s cursor view will be updated with this mapping, replacing the previous mapping (if any).

Source

pub exec fn map(&mut self, frame: UFrame, prop: PageProperty)

with

Tracked(cursor_owner): Tracked <& mut CursorOwner <'a,UserPtConfig>>,
Tracked(entry_owner): Tracked <EntryOwner <UserPtConfig>>,
Tracked(regions): Tracked <& mut MetaRegionOwners>,
Tracked(guards): Tracked <& mut Guards <'a,UserPtConfig>>,

requires

old(self).map_cursor_requires(*old(cursor_owner)),

old(self).map_cursor_inv(*old(cursor_owner), *old(guards), *old(regions)),

old(self).map_item_requires(frame, prop, entry_owner),

ensures

self.map_cursor_inv(*cursor_owner, *guards, *regions),

old(self)
    .map_item_ensures(
        frame,
        prop,
        old(self).pt_cursor.inner.model(*old(cursor_owner)),
        self.pt_cursor.inner.model(*cursor_owner),
    ),

Map a frame into the current slot.

This method will bring the cursor to the next slot after the modification.

§Preconditions

The cursor must be within the locked range and below the guard level, and the frame must fit within the remaining range of the cursor. The cursor must satisfy all invariants, and the frame must be well-formed when converted into a MappedItem (map_item_requires).

§Postconditions

After the call, the cursor will satisfy all invariants, and will map the frame into the current slot according to map_spec. After the call, the TLB will not contain any entries for the virtual address range being mapped (TODO).

Source

pub exec fn unmap(&mut self, len: usize) -> r : usize

requires

len % PAGE_SIZE() == 0,

old(self).pt_cursor.inner.va % PAGE_SIZE() == 0,

old(self).pt_cursor.inner.va + len <= KERNEL_VADDR_RANGE().end as int,

Clears the mapping starting from the current slot, and returns the number of unmapped pages.

This method will bring the cursor forward by len bytes in the virtual address space after the modification.

Already-absent mappings encountered by the cursor will be skipped. It is valid to unmap a range that is not mapped.

It must issue and dispatch a TLB flush after the operation. Otherwise, the memory safety will be compromised. Please call this function less to avoid the overhead of TLB flush. Using a large len is wiser than splitting the operation into multiple small ones.

§Panics

Panics if:

the length is longer than the remaining range of the cursor;
the length is not page-aligned.

Source

pub exec fn protect_next( &mut self, len: usize, op: impl FnOnce(PageProperty) -> PageProperty, ) -> r : Option<Range<Vaddr>>

with

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

requires

old(regions).inv(),

old(owner).inv(),

!old(owner).cur_entry_owner().is_absent(),

old(self).pt_cursor.inner.wf(*old(owner)),

old(self).pt_cursor.inner.inv(),

old(owner).in_locked_range(),

!old(owner).popped_too_high,

old(owner).children_not_locked(*old(guards)),

old(owner).nodes_locked(*old(guards)),

old(owner).relate_region(*old(regions)),

len % PAGE_SIZE() == 0,

old(self).pt_cursor.inner.level < NR_LEVELS(),

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

Applies the operation to the next slot of mapping within the range.

The range to be found in is the current virtual address with the provided length.

The function stops and yields the actually protected range if it has actually protected a page, no matter if the following pages are also required to be protected.

It also makes the cursor moves forward to the next page after the protected one. If no mapped pages exist in the following range, the cursor will stop at the end of the range and return None.

Note that it will NOT flush the TLB after the operation. Please make the decision yourself on when and how to flush the TLB using [Self::flusher].