Struct DmaCoherent 

pub struct DmaCoherent<M: AnyUFrameMeta + ?Sized> {
    pub inner: RwArc<AtomicDataWithOwner<DmaCoherentInner<M>, DmaCoherentInnerOwner<M>>>,
}

A coherent (or consistent) DMA mapping, which guarantees that the device and the CPU can access the data in parallel.

The mapping will be destroyed automatically when the object is dropped.

Fields

inner: RwArc<AtomicDataWithOwner<DmaCoherentInner<M>, DmaCoherentInnerOwner<M>>>

Implementations

impl<M: AnyUFrameMeta + ?Sized + OwnerOf> DmaCoherent<M>

pub exec fn map( segment: Segment<M>, is_cache_coherent: bool, ) -> r : Result<Self, DmaError>

requires

segment.inv(),

ensures

r matches Ok(r) ==> r.inner.wf(),

Creates a coherent DMA mapping backed by segment.

The is_cache_coherent argument specifies whether the target device can access main memory in a CPU-cache-coherent way.

impl<M: AnyUFrameMeta + ?Sized> DmaCoherent<M>

pub exec fn read_inner( &self, ) -> r : RwLockReadGuard<'_, AtomicDataWithOwner<DmaCoherentInner<M>, DmaCoherentInnerOwner<M>>, PreemptDisabled>

ensures

self.inner.wf(),

r@.inv(),

Acquires a read guard for the inner DMA-coherent state.

impl<M: AnyUFrameMeta + ?Sized + OwnerOf> DmaCoherent<M>

pub exec fn daddr(&self) -> r : Daddr

requires

self.inner.wf(),

ensures

self.inner.wf(),

Returns the starting device address.

pub exec fn paddr(&self) -> r : Paddr

requires

self.inner.wf(),

ensures

self.inner.wf(),

Returns the starting physical address.

pub exec fn nframes(&self) -> r : usize

requires

self.inner.wf(),

ensures

self.inner.wf(),

Returns the number of frames.

pub exec fn nbytes(&self) -> r : usize

requires

self.inner.wf(),

ensures

self.inner.wf(),

Returns the number of bytes in the DMA mapping.

pub exec fn reader<'a>(&'a self) -> r : VmReader<'a, Infallible>

with

->
reader_perm: Tracked<VmIoOwner>,

requires

self.inner.wf(),

ensures

self.inner.wf(),

r.inv(),

reader_perm@.inv(),

reader_perm@.is_kernel,

reader_perm@.has_read_view(),

r.wf(reader_perm@),

KERNEL_BASE_VADDR <= r.cursor.range@.start,

r.cursor.range@.end <= KERNEL_END_VADDR,

Returns a reader to read data from it.

pub exec fn writer<'a>(&'a self) -> r : VmWriter<'a, Infallible>

with

->
writer_perm: Tracked<VmIoOwner>,

requires

self.inner.wf(),

ensures

self.inner.wf(),

r.inv(),

writer_perm@.inv(),

writer_perm@.is_kernel,

writer_perm@.has_write_view(),

r.wf(writer_perm@),

Returns a writer to write data into it.

Trait Implementations

impl<M: AnyUFrameMeta + ?Sized> Clone for DmaCoherent<M>

exec fn clone(&self) -> r : Self

ensures

r == self,

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<M: AnyUFrameMeta + ?Sized + OwnerOf> HasDaddr for DmaCoherent<M>

exec fn daddr(&self) -> Daddr

impl<M: AnyUFrameMeta + ?Sized + OwnerOf> HasPaddr for DmaCoherent<M>

exec fn paddr(&self) -> Paddr

impl<M: AnyUFrameMeta + ?Sized> Inv for DmaCoherent<M>

open spec fn inv(self) -> bool

{ true }

impl<M: AnyUFrameMeta + ?Sized + Send + Sync + OwnerOf> VmIoOnce for DmaCoherent<M>

closed spec fn obeys_vmio_once_read_requires() -> bool

closed spec fn obeys_vmio_once_write_requires() -> bool

closed spec fn obeys_vmio_once_read_ensures() -> bool

closed spec fn obeys_vmio_once_write_ensures() -> bool

exec fn read_once<T: PodOnce>(&self, offset: usize) -> Result<T, Error>

exec fn write_once<T: PodOnce>( &self, offset: usize, new_val: &T, ) -> Result<(), Error>