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};
12
13verus! {
14
15/// The metadata of untyped frame.
16///
17/// If a structure `M` implements [`AnyUFrameMeta`], it can be used as the
18/// metadata of a type of untyped frames [`Frame<M>`]. All frames of such type
19/// will be accessible as untyped memory.
20pub trait AnyUFrameMeta: AnyFrameMeta {
21
22}
23
24/// A smart pointer to an untyped frame with any metadata.
25///
26/// The metadata of the frame is not known at compile time but the frame must
27/// be an untyped one. An [`UFrame`] as a parameter accepts any type of
28/// untyped frame metadata.
29///
30/// The usage of this frame will not be changed while this object is alive.
31/// Verus doesn't let us do very much with `dyn` traits, so instead of a `dyn AnyFrameMeta`
32/// we use `MetaSlotStorage`, a type that is a tagged union of the metadata types we've worked with so far.
33pub type UFrame = Frame<MetaSlotStorage>;
34
35/// A physical memory range that is untyped.
36///
37/// Untyped frames or segments can be safely read and written by the kernel or
38/// the user.
39pub trait UntypedMem {
40    /// Borrows a reader that can read the untyped memory.
41    fn reader(&self) -> VmReader<'_>;
42
43    /// Borrows a writer that can write the untyped memory.
44    fn writer(&self) -> VmWriter<'_>;
45}
46
47} // verus!
ostd/mm/frame/untyped.rs

ostd/mm/frame/
untyped.rs
