Struct GlobalMemOwner 

pub struct GlobalMemOwner {
    pub regions: MetaRegionOwners,
    pub pt: PageTableOwner<UserPtConfig>,
    pub tlb: TlbModel,
    pub memory: Map<Paddr, FrameContents>,
}

Global memory invariants

A GlobalMemOwner object ties together the components that are used in different layers of the OSTD system. It is the object about which we state the invariants of the memory system as a whole.

Verification Structure

Operations in mm take pieces of the global state as mutable arguments, and guarantee that their invariants are preserved. This guarantees that, at the end of each operation, the overall internal_invariants of the system hold. We then prove that the internal invariants imply the top-level properties that we want the memory system to obey.

Fields

regions: MetaRegionOwners

MetaRegionOwners is the fundamental data structure of the frame module, tracking the allocation of metadata slots and their permissions.

pt: PageTableOwner<UserPtConfig>

PageTableOwner tracks the tree structure of the page table. It can be converted to a [CursorOwner] for traversal and updates. A well-formed CursorOwner can be converted back into a PageTableOwner with consistent mappings, ensuring that its internal invariants are preserved.

tlb: TlbModel

TlbModel tracks the mappings in the TLB. It can flush mappings and it can load new ones from the page table.

memory: Map<Paddr, FrameContents>

FrameContents tracks the contents of a frame for use in the [VirtMem] library.

Implementations

impl GlobalMemOwner

pub closed spec fn page_table_mappings(self) -> Set<Mapping>

The set of mappings in the page table is determined by PageTableOwner::view_rec.

pub open spec fn page_table_mappings_disjoint_vaddrs(self) -> bool

{
    let pt_mappings = self.page_table_mappings();
    forall |m1: Mapping, m2: Mapping| (
        pt_mappings has m1 && pt_mappings has m2 && m1 != m2
            ==> Mapping::disjoint_vaddrs(m1, m2)
    )
}

Top-level property: the page table mappings are disjoint in the virtual address space.

pub open spec fn page_table_mappings_well_formed(self) -> bool

{
    let pt_mappings = self.page_table_mappings();
    forall |m: Mapping| pt_mappings has m ==> #[trigger] m.inv()
}

Top-level property: the page table mappings are well-formed. See Mapping::inv.

pub open spec fn tlb_mappings_disjoint_vaddrs(self) -> bool

{
    let tlb_mappings = self.tlb.mappings;
    forall |m1: Mapping, m2: Mapping| (
        tlb_mappings has m1 && tlb_mappings has m2 && m1 != m2
            ==> Mapping::disjoint_vaddrs(m1, m2)
    )
}

Top-level property: the TLB mappings are disjoint in the virtual address space.

pub open spec fn tlb_mappings_disjoint_paddrs(self) -> bool

{
    let tlb_mappings = self.tlb.mappings;
    forall |m1: Mapping, m2: Mapping| (
        tlb_mappings has m1 && tlb_mappings has m2 && m1 != m2
            ==> Mapping::disjoint_paddrs(m1, m2)
    )
}

Top-level property: the TLB mappings are disjoint in the physical address space.

pub open spec fn tlb_mappings_well_formed(self) -> bool

{
    let tlb_mappings = self.tlb.mappings;
    forall |m: Mapping| tlb_mappings has m ==> #[trigger] m.inv()
}

Top-level property: the TLB mappings are well-formed.

pub open spec fn invariants(self) -> bool

{
    &&& self.page_table_mappings_disjoint_vaddrs()
    &&& self.page_table_mappings_well_formed()

}

Top-level properties: the page table mappings are disjoint in the virtual address space and well-formed. Disjointness in the physical address space is intentionally not claimed — shared frame mappings (Phase 3 of the paths_in_pt refactor) legitimately map the same paddr at multiple vaddrs.

pub open spec fn internal_invariants(self) -> bool

{
    &&& self.regions.inv()
    &&& self.pt.inv()
    &&& self.pt.metaregion_sound(self.regions)
    &&& self.tlb.consistent_with_pt(self.pt.view())

}

Internal invariants for GlobalMemOwner: the page table is consistent with the TLB and with the allocated regions, and the internal invariants of each component hold. Note that some API functions break the consistency between the page table and the TLB, making it the responsibility of the caller to restore it by flushing the TLB.

pub proof fn internal_invariants_imply_top_level_properties(self)

requires

self.internal_invariants(),

ensures

self.invariants(),

If the internal invariants hold, then the top-level properties hold.