pub struct KVirtArea {
pub range: Range<Vaddr>,
}Expand description
Kernel virtual area.
A kernel virtual area manages a range of memory in VMALLOC_VADDR_RANGE.
It can map a portion or the entirety of its virtual memory pages to
physical memory, whether tracked with metadata or not.
It is the caller’s responsibility to ensure TLB coherence before using the mapped virtual address on a certain CPU.
Fields§
§range: Range<Vaddr>Implementations§
Source§impl KVirtArea
impl KVirtArea
Sourcepub open spec fn query_some_condition(self, owner: KVirtAreaOwner, addr: Vaddr) -> bool
pub open spec fn query_some_condition(self, owner: KVirtAreaOwner, addr: Vaddr) -> bool
{ owner.cursor_view_at(addr).present() }Whether there is a mapped item at the page containing the address.
Sourcepub open spec fn query_some_ensures(
self,
owner: KVirtAreaOwner,
addr: Vaddr,
r: Option<MappedItem>,
) -> bool
pub open spec fn query_some_ensures( self, owner: KVirtAreaOwner, addr: Vaddr, r: Option<MappedItem>, ) -> bool
{ r is Some && owner.cursor_view_at(addr).query_item_spec(r.unwrap()) is Some }Postcondition when a mapping exists at the page.
The returned item corresponds to the abstract mapping given by
query_item_spec.
Sourcepub open spec fn query_none_ensures(r: Option<MappedItem>) -> bool
pub open spec fn query_none_ensures(r: Option<MappedItem>) -> bool
{ r is None }Postcondition when no mapping exists at the page.
Sourcepub exec fn query<A: InAtomicMode>(&self, addr: Vaddr) -> r : Option<MappedItem>
pub exec fn query<A: InAtomicMode>(&self, addr: Vaddr) -> r : Option<MappedItem>
Tracked(owner): Tracked<KVirtAreaOwner>,self.inv(),self.range.start <= addr && addr < self.range.end,self.query_some_condition(owner, addr) ==> self.query_some_ensures(owner, addr, r),!self.query_some_condition(owner, addr) ==> Self::query_none_ensures(r),Queries the mapping at the given virtual address.
Returns the mapped item at the page containing addr, or None if there is no mapping.
§Preconditions
- The kernel virtual area invariant holds (
inv). - The address is within the virtual area’s range.
§Postconditions
- If there is a mapped item at the page containing the address ([
query_some_condition]), it is returned ([query_some_ensures]). - If there is no mapping at that page,
Noneis returned ([query_none_ensures]).
Sourcepub exec fn map_frames<'a, T: AnyUFrameMeta, A: InAtomicMode + 'a>(
area_size: usize,
map_offset: usize,
frames: Vec<Frame<T>>,
prop: PageProperty,
) -> Self
pub exec fn map_frames<'a, T: AnyUFrameMeta, A: InAtomicMode + 'a>( area_size: usize, map_offset: usize, frames: Vec<Frame<T>>, prop: PageProperty, ) -> Self
Tracked(owner): Tracked<KVirtAreaOwner>,
Tracked(entry_owners): Tracked<&mut Seq<EntryOwner<KernelPtConfig>>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(guards): Tracked<&mut Guards<'a, KernelPtConfig>>,
Tracked(guard_perm): Tracked<GuardPerm<'a, KernelPtConfig>>,0 < area_size,map_offset < area_size,map_offset % PAGE_SIZE == 0,area_size <= usize::MAX / 2,old(entry_owners).len() == frames.len(),frames.len() as int * PAGE_SIZE as int + map_offset as int <= area_size as int,forall |i: int| {
0 <= i < old(entry_owners).len() ==> (#[trigger] old(entry_owners)[i]).inv()
},forall |i: int| {
0 <= i < frames.len()
==> frame_entry_wf(frames[i], prop, #[trigger] old(entry_owners)[i])
},forall |i: int| {
0 <= i < frames.len()
==> CursorMut::<
'a,
KernelPtConfig,
A,
>::item_not_mapped(
MappedItem::Tracked(frame_as_dynframe(#[trigger] frames[i]), prop),
*old(regions),
)
},forall |i: int, j: int| {
0 <= i < j < frames.len()
==> (#[trigger] old(entry_owners)[i]).frame.unwrap().mapped_pa
!= (#[trigger] old(entry_owners)[j]).frame.unwrap().mapped_pa
},Create a kernel virtual area and map tracked pages into it.
The created virtual area will have a size of area_size, and the pages
will be mapped starting from map_offset in the area.
§Panics
This function panics if
Sourcepub unsafe exec fn map_untracked_frames<'a, A: InAtomicMode + 'a>(
area_size: usize,
map_offset: usize,
pa_range: Range<Paddr>,
prop: PageProperty,
) -> Self
pub unsafe exec fn map_untracked_frames<'a, A: InAtomicMode + 'a>( area_size: usize, map_offset: usize, pa_range: Range<Paddr>, prop: PageProperty, ) -> Self
Tracked(owner): Tracked<KVirtAreaOwner>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(guards): Tracked<&mut Guards<'a, KernelPtConfig>>,
Tracked(guard_perm): Tracked<GuardPerm<'a, KernelPtConfig>>,0 < area_size,area_size <= usize::MAX / 2,map_offset % PAGE_SIZE == 0,map_offset < area_size,pa_range.end as nat - pa_range.start as nat <= area_size as nat - map_offset as nat,pa_range.end <= MAX_PADDR,pa_range.start % PAGE_SIZE == 0,pa_range.end % PAGE_SIZE == 0,old(regions).paddr_range_not_mapped(pa_range),Creates a kernel virtual area and maps untracked frames into it.
The created virtual area will have a size of area_size, and the
physical addresses will be mapped starting from map_offset in
the area.
You can provide a 0..0 physical range to create a virtual area without
mapping any physical memory.
§Panics
This function panics if