Modules§
Structs§
Constants§
- FRAME_
METADATA_ RANGE - Kernel virtual address range for storing the page frame metadata.
- KERNEL_
VADDR_ RANGE - The kernel address space. There are the high canonical addresses defined in most 48-bit width architectures.
- MAX_
NR_ PAGES - MAX_
PADDR - Parameterized maximum physical address.
- MAX_
USERSPACE_ VADDR - The maximum virtual address of user space (non inclusive).
- NR_
ENTRIES - The maximum number of entries in a page table node
- NR_
LEVELS - The maximum level of a page table node.
- PAGE_
FLAG_ MAPPING - PAGE_
FLAG_ MAPPING_ SPEC - PAGE_
INVERTED_ FLAG_ MAPPING - PAGE_
INVERTED_ FLAG_ MAPPING_ SPEC - PAGE_
PRIV_ MAPPING - PAGE_
PRIV_ MAPPING_ SPEC - PAGE_
SIZE - Page size.
- PHYS_
ADDR_ MASK - Masks of the physical address.
Functions§
- activate_
page_ ⚠table - current_
page_ table_ paddr - current_
page_ table_ paddr_ spec - lemma_
linear_ mapping_ base_ vaddr_ properties - lemma_
max_ paddr_ range - lemma_
meta_ frame_ vaddr_ properties - lemma_
mod_ 0_ add - lemma_
nr_ subpage_ per_ huge_ eq_ nr_ entries - lemma_
paddr_ to_ vaddr_ properties - lemma_
vaddr_ to_ paddr_ properties - paddr_
to_ vaddr - paddr_
to_ vaddr_ spec - tlb_
flush_ addr - tlb_
flush_ addr_ range - tlb_
flush_ all_ excluding_ global - tlb_
flush_ all_ including_ global - vaddr_
to_ paddr - vaddr_
to_ paddr_ spec