ostd/mm/frame/
untyped.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Untyped physical memory management.
3//!
4//! As detailed in [`crate::mm::frame`], untyped memory can be accessed with
5//! relaxed rules but we cannot create references to them. This module provides
6//! the declaration of untyped frames and segments, and the implementation of
7//! extra functionalities (such as [`VmIo`]) for them.
8use vstd::prelude::*;
9
10use super::*;
11use crate::mm::io::{VmReader, VmWriter};
12use crate::specs::mm::frame::meta_owners::MetaSlotStorage;
13
14verus! {
15
16/// The metadata of untyped frame.
17///
18/// If a structure `M` implements [`AnyUFrameMeta`], it can be used as the
19/// metadata of a type of untyped frames [`Frame<M>`]. All frames of such type
20/// will be accessible as untyped memory.
21pub trait AnyUFrameMeta: AnyFrameMeta {
22
23}
24
25/// A smart pointer to an untyped frame with any metadata.
26///
27/// The metadata of the frame is not known at compile time but the frame must
28/// be an untyped one. An [`UFrame`] as a parameter accepts any type of
29/// untyped frame metadata.
30///
31/// The usage of this frame will not be changed while this object is alive.
32/// Verus doesn't let us do very much with `dyn` traits, so instead of a `dyn AnyFrameMeta`
33/// we use `MetaSlotStorage`, a type that is a tagged union of the metadata types we've worked with so far.
34pub type UFrame = Frame<MetaSlotStorage>;
35
36/// A physical memory range that is untyped.
37///
38/// Untyped frames or segments can be safely read and written by the kernel or
39/// the user.
40pub trait UntypedMem {
41    /// Borrows a reader that can read the untyped memory.
42    fn reader(&self) -> VmReader<'_>;
43
44    /// Borrows a writer that can write the untyped memory.
45    fn writer(&self) -> VmWriter<'_>;
46}
47
48} // verus!
ostd/mm/frame/untyped.rs

ostd/mm/frame/
untyped.rs
