Struct GlobalMemView

Source

pub struct GlobalMemView {
    pub pt_mappings: Set<Mapping>,
    pub tlb_mappings: Set<Mapping>,
    pub unmapped_pas: Set<Paddr>,
    pub memory: Map<Paddr, FrameContents>,
}

Expand description

A GlobalMemView is a more abstract view of memory that elides most of the details. The API specifications of higher-level objects like VmSpaceOwner use this view.

Fields§

§pt_mappings: Set<Mapping>§tlb_mappings: Set<Mapping>§unmapped_pas: Set<Paddr>§memory: Map<Paddr, FrameContents>

Implementations§

Source §

impl GlobalMemView

Source

pub open spec fn addr_transl(self, va: usize) -> Option<(usize, usize)>

{
    let mappings = self
        .tlb_mappings
        .filter(|m: Mapping| m.va_range.start <= va < m.va_range.end);
    if 0 < mappings.len() {
        let m = mappings.choose();
        let off = va - m.va_range.start;
        Some((m.pa_range.start, off as usize))
    } else {
        None
    }
}

Source

pub open spec fn is_mapped(self, pa: usize) -> bool

{
    exists |m: Mapping| {
        self.tlb_mappings.contains(m) && m.pa_range.start <= pa < m.pa_range.end
    }
}

Source

pub open spec fn all_pas_accounted_for(self) -> bool

{
    forall |pa: Paddr| {
        0 <= pa < MAX_PADDR
            ==> #[trigger] self.is_mapped(pa) || #[trigger]
                self.unmapped_pas.contains(pa)
    }
}

Source

pub open spec fn pas_uniquely_mapped(self) -> bool

{
    forall |m1: Mapping, m2: Mapping| {
        self.tlb_mappings.contains(m1) && self.tlb_mappings.contains(m2) && m1 != m2
            ==> m1.pa_range.end <= m2.pa_range.start
                || m2.pa_range.end <= m1.pa_range.start
    }
}

Source

pub open spec fn unmapped_correct(self) -> bool

{ forall |pa: Paddr| self.is_mapped(pa) <==> !self.unmapped_pas.contains(pa) }

Source

pub open spec fn take_view_spec(self, vaddr: usize, len: usize) -> (Self, MemView)

{
    let range_end = vaddr + len;
    let leave_mappings: Set<Mapping> = self
        .tlb_mappings
        .filter(|m: Mapping| m.va_range.end <= vaddr || m.va_range.start > range_end);
    let take_mappings = self
        .tlb_mappings
        .filter(|m: Mapping| m.va_range.start < range_end && m.va_range.end > vaddr);
    let leave_pas = Set::new(|pa: usize| {
        exists |m: Mapping| {
            leave_mappings.contains(m) && m.pa_range.start <= pa < m.pa_range.end
        }
    });
    let take_pas = Set::new(|pa: usize| {
        exists |m: Mapping| {
            take_mappings.contains(m) && m.pa_range.start <= pa < m.pa_range.end
        }
    });
    (
        GlobalMemView {
            tlb_mappings: leave_mappings,
            memory: self.memory.restrict(leave_pas),
            ..self
        },
        MemView {
            mappings: take_mappings,
            memory: self.memory.restrict(take_pas),
        },
    )
}

Source

pub proof fn take_view(tracked &mut self, vaddr: usize, len: usize) -> tracked view : MemView

ensures

*final(self) == old(self).take_view_spec(vaddr, len).0,

view == old(self).take_view_spec(vaddr, len).1,

Source

pub open spec fn return_view_spec(self, view: MemView) -> Self

{
    GlobalMemView {
        tlb_mappings: self.tlb_mappings.union(view.mappings),
        memory: self.memory.union_prefer_right(view.memory),
        ..self
    }
}

Source

pub proof fn return_view(&mut self, view: MemView)

ensures

*final(self) == old(self).return_view_spec(view),

Source

pub open spec fn tlb_flush_vaddr_spec(self, vaddr: Vaddr) -> Self

{
    let tlb_mappings = self
        .tlb_mappings
        .filter(|m: Mapping| m.va_range.end <= vaddr || vaddr < m.va_range.start);
    GlobalMemView {
        tlb_mappings,
        ..self
    }
}

Source

pub proof fn tlb_flush_vaddr(&mut self, vaddr: Vaddr)

requires

old(self).inv(),

ensures

*final(self) == old(self).tlb_flush_vaddr_spec(vaddr),

final(self).inv(),

Source

pub open spec fn tlb_soft_fault_spec(self, vaddr: Vaddr) -> Self

{
    let mapping = self
        .pt_mappings
        .filter(|m: Mapping| m.va_range.start <= vaddr < m.va_range.end)
        .choose();
    GlobalMemView {
        tlb_mappings: self.tlb_mappings.insert(mapping),
        ..self
    }
}

Source

pub proof fn tlb_soft_fault(tracked &mut self, vaddr: Vaddr)

requires

old(self).inv(),

old(self).addr_transl(vaddr) is None,

ensures

*final(self) == old(self).tlb_soft_fault_spec(vaddr),

final(self).inv(),

Source

pub open spec fn pt_map_spec(self, m: Mapping) -> Self

{
    let pt_mappings = self.pt_mappings.insert(m);
    let unmapped_pas = self
        .unmapped_pas
        .difference(Set::new(|pa: usize| m.pa_range.start <= pa < m.pa_range.end));
    GlobalMemView {
        pt_mappings,
        unmapped_pas,
        ..self
    }
}

Source

pub proof fn pt_map(&mut self, m: Mapping)

requires

forall |pa: Paddr| {
    m.pa_range.start <= pa < m.pa_range.end ==> old(self).unmapped_pas.contains(pa)
},

old(self).inv(),

ensures

*final(self) == old(self).pt_map_spec(m),

Source

pub open spec fn pt_unmap_spec(self, m: Mapping) -> Self

{
    let pt_mappings = self.pt_mappings.remove(m);
    let unmapped_pas = self
        .unmapped_pas
        .union(Set::new(|pa: usize| m.pa_range.start <= pa < m.pa_range.end));
    GlobalMemView {
        pt_mappings,
        unmapped_pas,
        ..self
    }
}

Source

pub proof fn pt_unmap(&mut self, m: Mapping)

requires

old(self).pt_mappings.contains(m),

old(self).inv(),

ensures

*final(self) == old(self).pt_unmap_spec(m),

final(self).inv(),

Source

pub proof fn lemma_va_mapping_unique(self, va: usize)

requires

self.inv(),

ensures

self
    .tlb_mappings
    .filter(|m: Mapping| m.va_range.start <= va < m.va_range.end)
    .is_singleton(),

Trait Implementations§

Source §

impl Inv for GlobalMemView

Source §

open spec fn inv(self) -> bool

{
    &&& forall |m: Mapping| {
        self.tlb_mappings.contains(m)
            ==> {
                &&& m.inv()
                &&& forall |pa: Paddr| {
                    m.pa_range.start <= pa < m.pa_range.end
                        ==> {
                            &&& self.memory.dom().contains(pa)

                        }
                }
                &&& self.memory.contains_key(m.pa_range.start)
                &&& self.memory[m.pa_range.start].size == m.page_size
                &&& self.memory[m.pa_range.start].inv()

            }
    }
    &&& forall |m: Mapping| {
        forall |n: Mapping| {
            self.tlb_mappings.contains(m)
                ==> (self.tlb_mappings.contains(n)
                    ==> (m != n
                        ==> #[trigger] m.va_range.end <= n.va_range.start
                            || n.va_range.end <= m.va_range.start))
        }
    }
    &&& self.tlb_mappings.finite()
    &&& self.pt_mappings.finite()
    &&& self.memory.dom().finite()
    &&& self.all_pas_accounted_for()
    &&& self.pas_uniquely_mapped()
    &&& self.unmapped_correct()

}