ostd::mm::vm_space

Struct CursorMut

pub struct CursorMut<'a, A: InAtomicMode> {
    pub pt_cursor: CursorMut<'a, UserPtConfig, A>,
    pub flusher: TlbFlusher<'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>§flusher: TlbFlusher<'a>

Implementations§

Source §

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

Source

pub open spec fn query_requires( 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) -> res : 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(self).pt_cursor.inner.invariants(*old(owner), *old(regions), *old(guards)),

old(owner).in_locked_range(),

ensures

self.pt_cursor.inner.invariants(*owner, *regions, *guards),

old(self).pt_cursor.inner.query_some_condition(*owner)
    ==> {
        &&& res is Ok
        &&& self.pt_cursor.inner.query_some_ensures(*owner, res.unwrap())

    },

!old(self).pt_cursor.inner.query_some_condition(*owner)
    ==> {
        &&& res is Ok
        &&& self.pt_cursor.inner.query_none_ensures(*owner, res.unwrap())

    },

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.

§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<'a, UserPtConfig>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(guards): Tracked<&mut Guards<'a, UserPtConfig>>,

requires

old(self).pt_cursor.inner.invariants(*old(owner), *old(regions), *old(guards)),

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

old(owner).in_locked_range(),

len % PAGE_SIZE == 0,

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

ensures

self.pt_cursor.inner.invariants(*owner, *regions, *guards),

res is Some
    ==> {
        &&& res.unwrap() == self.pt_cursor.inner.va
        &&& owner.level < owner.guard_level
        &&& owner.in_locked_range()

    },

Moves the cursor forward to the next mapped virtual address.

This is the same as Cursor::find_next.

§Verified Properties

§Preconditions

Liveness: The cursor must be within the locked range and below the guard level. 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<'a, UserPtConfig>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(guards): Tracked<&mut Guards<'a, UserPtConfig>>,

requires

old(self).pt_cursor.inner.invariants(*old(owner), *old(regions), *old(guards)),

!old(self).pt_cursor.inner.jump_panic_condition(va),

ensures

self.pt_cursor.inner.invariants(*owner, *regions, *guards),

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

    },

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

Jump to the virtual address.

This is the same as Cursor::jump.

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

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

returns

self.pt_cursor.inner.va,

Get the virtual address of the current slot.

Source

pub exec fn flusher(&self) -> &TlbFlusher<'a>

Get the dedicated TLB flusher for this cursor.

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>, regions: MetaRegionOwners, ) -> 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
    &&& level < self.pt_cursor.inner.guard_level
    &&& 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
    &&& crate::mm::page_table::CursorMut::<
        'a,
        UserPtConfig,
        A,
    >::item_not_mapped(item, regions)
    &&& crate::mm::page_table::CursorMut::<
        'a,
        UserPtConfig,
        A,
    >::item_slot_in_regions(item, regions)

}

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>>,
Tracked(tlb_model): Tracked<&mut TlbModel>,

requires

old(tlb_model).inv(),

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, *old(regions)),

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.

§Verified Properties

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

§Safety

The preconditions of this function require that the frame to be mapped is disjoint from any other mapped frames. If this is not the case, the global memory invariants will be violated. If the allocator implementation is correct, the user shouldn’t be able to create such a frame object in the first place, but currently a proof of that is outside of the verification boundary. Because this function flushes the TLB if it unmaps a page, it preserves TLB consistency.

Source

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

with

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

requires

len > 0,

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,

old(self).pt_cursor.inner.invariants(*old(cursor_owner), *old(regions), *old(guards)),

old(cursor_owner).in_locked_range(),

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

old(tlb_model).inv(),

ensures

self.pt_cursor.inner.invariants(*cursor_owner, *regions, *guards),

old(self)
    .pt_cursor
    .inner
    .model(*old(cursor_owner))
    .unmap_spec(len, self.pt_cursor.inner.model(*cursor_owner), r),

tlb_model.inv(),

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,

old(owner).cur_entry_owner().is_frame(),

op.requires((old(owner).cur_entry_owner().frame.unwrap().prop,)),

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.