Skip to main content

CursorMut

ostd::mm::vm_space

Struct CursorMut 

Source 
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 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

}
Source

pub open spec fn item_wf( 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_slot_in_regions(item, regions)

}
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)
}
Source§

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

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(),
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).pt_cursor.inner.invariants(*final(owner), *final(regions), *final(guards)),
old(owner).in_locked_range() ==> res is Ok,
res matches Ok(
    state,
) ==> final(self).pt_cursor.inner.query_some_condition(*final(owner))
    ==> final(self).pt_cursor.inner.query_some_ensures(*final(owner), state),
res matches Ok(
    state,
) ==> !final(self).pt_cursor.inner.query_some_condition(*final(owner))
    ==> final(self).pt_cursor.inner.query_none_ensures(*final(owner), state),
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.

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
  • Safety Invariants: The page table cursor safety invariants ([crate::mm::page_table::Cursor::invariants]) must hold before the call.
§Postconditions
  • Safety Invariants: Page table cursor safety invariants are preserved.
  • Correctness: If the cursor is within the locked range, the result is Ok.
  • Correctness: 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]).
  • Correctness: The mapping that is returned corresponds to the abstract mapping given by query_item_spec.
  • Correctness: 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.
  • Correctness: If the metadata region was well-formed before the call, it will be well-formed after.
  • Safety: The mappings in the page table are not affected.
  • Safety: The soundness of individual entries are not affected.
§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)),
ensures
!old(self).pt_cursor.inner.find_next_panic_condition(len),
final(self).pt_cursor.inner.invariants(*final(owner), *final(regions), *final(guards)),
res is Some
    ==> {
        &&& res.unwrap() == final(self).pt_cursor.inner.va
        &&& final(owner).level < final(owner).guard_level
        &&& final(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
  • 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<'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
!old(self).pt_cursor.inner.jump_panic_condition(va),
final(self).pt_cursor.inner.invariants(*final(owner), *final(regions), *final(guards)),
final(self).pt_cursor.inner.barrier_va.start <= va
    < final(self).pt_cursor.inner.barrier_va.end
    ==> {
        &&& res is Ok
        &&& final(self).pt_cursor.inner.va == va

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

Jump to the virtual address.

This is the same as Cursor::jump.

§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

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(&mut self) -> ret : &mut TlbFlusher<'a>

ensures
*ret == old(self).flusher,
*final(ret) == final(self).flusher,

Get the dedicated TLB flusher for this cursor.

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).pt_cursor.inner.invariants(*old(cursor_owner), *old(regions), *old(guards)),
old(cursor_owner).in_locked_range(),
old(self).item_wf(frame, prop, entry_owner, *old(regions)),
ensures
!old(self)
    .pt_cursor
    .map_panic_conditions(MappedItem {
        frame: frame,
        prop: prop,
    }),
final(self)
    .pt_cursor
    .inner
    .invariants(*final(cursor_owner), *final(regions), *final(guards)),
old(self)
    .map_item_ensures(
        frame,
        prop,
        old(self).pt_cursor.inner.model(*old(cursor_owner)),
        final(self).pt_cursor.inner.model(*final(cursor_owner)),
    ),

Map a frame into the current slot.

This method will bring the cursor to the next slot after the modification. If there is an existing mapping at the current slot, it will be replaced and the TLB will be flushed for that entry.

§Verified Properties
§Preconditions
  • Safety Invariants: The page table cursor safety invariants (invariants) and the TLB invariant (TlbModel::inv) must hold before the call.
  • Liveness: The cursor must not be past the end of its locked range, and the frame’s level must fit within the remaining range, or the function will panic.
  • Bookkeeping: The frame must be well-formed with respect to its entry owner (item_wf).
§Postconditions
  • Safety Invariants: Page table cursor safety invariants are preserved.
  • Correctness: The page table view is updated with the new mapping according to map_item_ensures.
  • Correctness: If the metadata region was well-formed before the call and the frame was not already mapped, it will be well-formed after.
§Safety
  • For soundness purposes, it doesn’t matter if a frame is mapped multiple times in the same page table. There is still a clear definition of the behavior.
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
old(self).pt_cursor.inner.invariants(*old(cursor_owner), *old(regions), *old(guards)),
old(tlb_model).inv(),
ensures
!old(self).pt_cursor.inner.find_next_panic_condition(len),
final(self)
    .pt_cursor
    .inner
    .invariants(*final(cursor_owner), *final(regions), *final(guards)),
old(self)
    .pt_cursor
    .inner
    .model(*old(cursor_owner))
    .unmap_spec(len, final(self).pt_cursor.inner.model(*final(cursor_owner)), r),
final(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.

§Verified Properties
§Preconditions
  • Safety Invariants: The page table cursor safety invariants ([crate::mm::page_table::Cursor::invariants]) must hold before the call.
  • Safety Invariants: The TLB invariant (TlbModel::inv) must hold.
  • 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: The page table cursor safety invariants are preserved.
  • Safety Invariants: The TLB invariant is preserved.
  • Correctness: Unmaps a range of virtual addresses from the current address up to len bytes and returns the number of mappings that were removed.
  • Correctness: If the metadata region was well-formed before the call, it will be well-formed after.
§Panics

Panics if:

  • the length is longer than the remaining range of the cursor;
  • the length is not page-aligned.
§Safety
  • It is always sound to unmap pages. We flush unmapped pages from the TLB to ensure consistency.
  • TODO: formalizing and proving that this function preserves TLB consistency would be pretty straightforward and would be a nice addition to the correctness properties.
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(self).pt_cursor.inner.invariants(*old(owner), *old(regions), *old(guards)),
forall |p: PageProperty| op.requires((p,)),
ensures
!old(self).pt_cursor.inner.find_next_panic_condition(len),
final(self).pt_cursor.inner.invariants(*final(owner), *final(regions), *final(guards)),
final(self).pt_cursor.inner.barrier_va == old(self).pt_cursor.inner.barrier_va,

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.

§Verified Properties
§Preconditions
  • Safety Invariants: The page table cursor safety invariants (invariants) and the meta-region invariants must hold before the call.
  • The cursor must be within the locked range and below the guard level.
  • The current entry must be a mapped frame (not absent or a page table node).
  • Liveness: The length must be page-aligned and within the remaining cursor range.
§Postconditions
  • Correctness: If the metadata region was well-formed before the call, it will be well-formed after.
§Panics

Panics if the length is longer than the remaining range of the cursor.

§Safety
  • From a soundness perspective changing a userspace page’s prop field is safe.

Auto Trait Implementations§

§

impl<'a, A> Freeze for CursorMut<'a, A>

§

impl<'a, A> !RefUnwindSafe for CursorMut<'a, A>

§

impl<'a, A> Send for CursorMut<'a, A>
where A: Sync,

§

impl<'a, A> Sync for CursorMut<'a, A>
where A: Sync,

§

impl<'a, A> Unpin for CursorMut<'a, A>

§

impl<'a, A> UnsafeUnpin for CursorMut<'a, A>

§

impl<'a, A> !UnwindSafe for CursorMut<'a, A>

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> VERUS_SPEC__A

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

§

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> T

§

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

§

fn obeys_try_from_spec() -> bool

§

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

§

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>