ostd/mm/dma/
mod.rs

1// SPDX-License-Identifier: MPL-2.0
2mod dma_coherent;
3pub use dma_coherent::DmaCoherent;
4mod dma_stream;
5#[cfg(ktest)]
6mod test;
7
8use alloc::collections::BTreeSet;
9use vstd::{predicate::Predicate as DataPredicate, prelude::*};
10
11use crate::sync::{
12    AtomicDataWithOwner, Once, PreemptDisabled, SpinLock, SpinLockGuard, TrivialPred,
13};
14
15use super::Paddr;
16
17verus! {
18
19pub tracked struct DmaMappingSetOwner {}
20
21impl DataPredicate<SpinLock<BTreeSet<Paddr>, PreemptDisabled>> for DmaMappingSetOwner {
22    open spec fn predicate(&self, v: SpinLock<BTreeSet<Paddr>, PreemptDisabled>) -> bool {
23        v.wf()
24    }
25}
26
27/// Set of all physical addresses with dma mapping.
28exec static DMA_MAPPING_SET: Once<
29    SpinLock<BTreeSet<Paddr>, PreemptDisabled>,
30    DmaMappingSetOwner,
31    TrivialPred,
32>
33    ensures
34        DMA_MAPPING_SET.wf(),
35{
36    Once::new(Ghost(TrivialPred))
37}
38
39#[inline(always)]
40pub fn init() {
41    let lock = SpinLock::new(BTreeSet::new());
42
43    proof {
44        use_type_invariant(&lock);
45    }
46
47    let data = AtomicDataWithOwner::new(lock, Tracked(DmaMappingSetOwner {  }));
48
49    DMA_MAPPING_SET.init(data);
50}
51
52/// The device address.
53///
54/// If a device performs DMA to read or write system
55/// memory, the addresses used by the device are device addresses.
56/// Daddr can distinguish the address space used by cpu side and
57/// the address space used by device side.
58pub type Daddr = usize;
59
60#[derive(PartialEq)]
61pub enum DmaType {
62    Direct,
63    Iommu,
64}
65
66#[derive(Debug, PartialEq)]
67pub enum DmaError {
68    InvalidArgs,
69    AlreadyMapped,
70}
71
72/// A trait for types that have mapped address in the device address space.
73pub trait HasDaddr {
74    /// Gets the base address of the mapping in the
75    /// device address space.
76    fn daddr(&self) -> Daddr;
77}
78
79#[verifier::inline]
80pub open spec fn is_valid_daddr(d: Daddr) -> bool {
81    true
82}
83
84/// Checks whether the physical addresses has dma mapping.
85/// Fail if they have been mapped, otherwise insert them.
86#[verus_spec(
87    requires
88        start_paddr + num_pages * crate::mm::PAGE_SIZE <= usize::MAX,
89)]
90fn check_and_insert_dma_mapping(start_paddr: Paddr, num_pages: usize) -> bool {
91    match DMA_MAPPING_SET.get() {
92        None => false,
93        Some(mapping_set) => {
94            let mut mapping_set = mapping_set.lock();
95            let mut i = 0;
96
97            #[verus_spec(
98                invariant
99                    i <= num_pages,
100                    start_paddr + num_pages * crate::mm::PAGE_SIZE <= usize::MAX,
101                decreases
102                    num_pages - i,
103            )]
104            while i < num_pages {
105                let paddr = start_paddr + (i * crate::mm::PAGE_SIZE);
106                if mapping_set.contains(&paddr) {
107                    return false;
108                }
109                i += 1;
110            }
111
112            i = 0;
113            #[verus_spec(
114                invariant
115                    i <= num_pages,
116                    start_paddr + num_pages * crate::mm::PAGE_SIZE <= usize::MAX,
117                decreases
118                    num_pages - i,
119            )]
120            while i < num_pages {
121                let paddr = start_paddr + (i * crate::mm::PAGE_SIZE);
122                // Failure: complex arguments to $mut parameters are currently unsupported
123                // mapping_set.insert(paddr);
124                i += 1;
125            }
126
127            true
128        },
129    }
130}
131
132#[verifier::external_body]
133pub fn dma_type() -> DmaType {
134    unimplemented!()
135}
136
137} // verus!
138/*
139use alloc::collections::BTreeSet;
140
141pub use dma_coherent::DmaCoherent;
142pub use dma_stream::{DmaDirection, DmaStream, DmaStreamSlice};
143use inherit_methods_macro::inherit_methods;
144use spin::Once;
145
146use super::Paddr;
147use crate::{arch::iommu::has_dma_remapping, mm::PAGE_SIZE, sync::SpinLock};
148
149
150
151
152#[inherit_methods(from = "(**self)")]
153impl<T: HasDaddr> HasDaddr for &T {
154    fn daddr(&self) -> Daddr;
155}
156
157/// Set of all physical addresses with dma mapping.
158static DMA_MAPPING_SET: Once<SpinLock<BTreeSet<Paddr>>> = Once::new();
159
160pub fn dma_type() -> DmaType {
161    if has_dma_remapping() {
162        DmaType::Iommu
163    } else {
164        DmaType::Direct
165    }
166}
167
168pub fn init() {
169    DMA_MAPPING_SET.call_once(|| SpinLock::new(BTreeSet::new()));
170}
171
172/// Checks whether the physical addresses has dma mapping.
173/// Fail if they have been mapped, otherwise insert them.
174fn check_and_insert_dma_mapping(start_paddr: Paddr, num_pages: usize) -> bool {
175    let mut mapping_set = DMA_MAPPING_SET.get().unwrap().disable_irq().lock();
176    // Ensure that the addresses used later will not overflow
177    start_paddr.checked_add(num_pages * PAGE_SIZE).unwrap();
178    for i in 0..num_pages {
179        let paddr = start_paddr + (i * PAGE_SIZE);
180        if mapping_set.contains(&paddr) {
181            return false;
182        }
183    }
184    for i in 0..num_pages {
185        let paddr = start_paddr + (i * PAGE_SIZE);
186        mapping_set.insert(paddr);
187    }
188    true
189}
190
191/// Removes a physical address from the dma mapping set.
192fn remove_dma_mapping(start_paddr: Paddr, num_pages: usize) {
193    let mut mapping_set = DMA_MAPPING_SET.get().unwrap().disable_irq().lock();
194    // Ensure that the addresses used later will not overflow
195    start_paddr.checked_add(num_pages * PAGE_SIZE).unwrap();
196    for i in 0..num_pages {
197        let paddr = start_paddr + (i * PAGE_SIZE);
198        mapping_set.remove(&paddr);
199    }
200}
201*/
ostd/mm/dma/mod.rs

ostd/mm/dma/
mod.rs
