diff --git a/include/arch/arm/arch/64/mode/hardware.h b/include/arch/arm/arch/64/mode/hardware.h index 2fe8a6dbf..a4b42ace5 100644 --- a/include/arch/arm/arch/64/mode/hardware.h +++ b/include/arch/arm/arch/64/mode/hardware.h @@ -12,62 +12,111 @@ #include /* + * For information on the architectural details of the Armv8-A address translation, + * refer to the ARM "Armv8-A Address Translation", document ID 100940. + * https://developer.arm.com/documentation/100940/latest/ + * * !defined(CONFIG_ARM_HYPERVISOR_SUPPORT) * - * 2^64 +-------------------+ - * | Kernel Page PDPT | --+ - * 2^64 - 2^39 +-------------------+ PPTR_BASE - * | TLB Bitmaps | | - * +-------------------+ | - * | | | - * | Unmapped | | - * | | | - * 2^64 - 2^48 +-------------------+ | - * | | | - * | Unaddressable | | - * | | | - * 2^48 +-------------------+ USER_TOP - * | | | - * | User | | - * | | | - * 0x0 +-------------------+ | - * | - * +-------------+ - * | - * v - * 2^64 +-------------------+ - * | | - * | | +------+ - * | Kernel Page Table | --> | PD | ----+ - * | | +------+ | - * | | | - * 2^64 - 2^30 +-------------------+ PPTR_TOP | - * | | | - * | Physical Memory | | - * | Window | | - * | | | - * +-------------------+ | - * | | | - * | | +------+ | - * | Kernel ELF | --> | PD | | - * | | +------+ | - * | | | - * +-------------------+ KERNEL_ELF_BASE | - * | | | - * | Physical Memory | | - * | Window | | - * | | | - * 2^64 - 2^39 +-------------------+ PPTR_BASE | - * | - * +---------------------+ - * | - * v - * 2^64 - 2^21 + 2^12 +-------------------+ - * | | - * | Kernel Devices | - * | | - * 2^64 - 2^21 +-------------------+ KDEV_BASE + * Per ARM ARM DDI 0487 (version L.b), in D8.2.4, VA bit[55] selects between + * TTBR1_EL1 and TTBR0_EL1, the two Translation Table base registers. + * seL4 follows the convention to use the "higher VA" (TTBR1_EL1) for kernel + * memory and the "lower VA" (TTBR0_EL1) for userspace memory. + * seL4 also does not enable the ARM "Address tagging" (D8.8) feature ( + * sometimes known as Top Byte Ignore) so virtual addresses need to be sign + * extended in VA[63:56]. * + * seL4 chooses to map only a single entry of the PGD translation base, + * using a singular PUD that covers 2^39 bits of virtual address space. + * Note that 2^39, 2^30, 2^21 corresponds to the memory ranges covered by + * a PUD, PD, and PT respectively. + * + * (PGD) + * | + * v + * 2^64 +-------------------+ --+ + * | | | + * | Kernel Mem Region | ---> (PUD) | + * | | | + * 2^64 - 2^39 +-------------------+ | Kernel Space (TTBR1) + * | | | + * | Unmapped | | + * | | | + * 2^64 - 2^48 +-------------------+ --+ + * | | + * | | + * | | + * | Unaddressable | + * | | + * | | + * | | + * 2^48 +-------------------+ --+ + * | Unmapped | | + * +-------------------+ USER_TOP | + * | | | User Space (TTBR0) + * | User | | + * | | | + * 0x0 +-------------------+ --+ + * + * + * The Kernel's PUD (`armKSGlobalKernelPUD`) is then split into several parts. + * + * - The physical memory window starts from the 0th PUD entry and extends + * up to the second-to-last PUD entry. This covers 255GiB and contains the + * virtual address for which the kernel ELF is mapped in to. + * + * The physical memory window is mapped using Large Pages. + * + * - The top entry of the PUD then contains the "kernel mappings" (more details below). + * + * (PUD) + * | + * v + * 2^64 +-------------------+ + * | | + * | Kernel Mappings | --> (PD) + * | | + * 2^64 - 2^30 +-------------------+ PPTR_TOP + * | | + * | | + * | | + * | Physical Memory | + * | Window | + * | | + * | | + * | ----------------- | KERNEL_ELF_TOP + * | Kernel ELF | + * | ----------------- | KERNEL_ELF_BASE (at `physBase()`) + * | | + * | | + * 2^64 - 2^39 +-------------------+ PPTR_BASE + * + * + * The kernel mappings PD (code: `armKSGlobalKernelPDs[kernel_mappings_pud_idx]`) + * then contains the: + * + * - Kernel Devices page table in the last entry of the PD. This points to the + * `armKSGlobalKernelPT` which points to 4K device pages. + * - Depending on configuration, the benchmarking log buffer. + * + * (PD ) + * | + * v + * 2^64 +------------------+ + * | | + * | Kernel Devices | --> (PT) + * | | + * 2^64 - 2^21 +------------------+ KDEV_BASE + * | | + * | Log Buffer | + * | | + * 2^64 - 2 * 2^21 +------------------+ KS_LOG_BASE + * | | + * | | + * | Unmapped | + * | | + * | | + * 2^64 - 2^30 +------------------+ */ /* @@ -83,10 +132,9 @@ * the 512 GiB at the top of that 48 bits of addressable * virtual memory. * - * In EL2 there is no canonical-high portion of the address space since - * address tagging is not supported in EL2. Therefore the kernel is linked - * to the canonical lower portion of the address space (all the unused top bits - * are set to 0, not 1). + * In EL2 there is only a TTBR0_EL2 register (unlike EL1 with TTBR0 and TTBR1) + * so the kernel is linked in the low 2^48 bits of the virtual address space, + * or "lower VA" in EL1 parlance. * * The memory map used by the EL2 kernel's separate address space * ends up looking something like this: @@ -114,56 +162,67 @@ * | | v * +-----------------------------------+ <- 0x0 * + * The layout of the kernel's virtual address space is very similar to + * non-hyp, but the kernel address space is distinct to userland (EL1/EL0). * - * 2^64 +-------------------+ - * | | - * | Unaddressable | - * | | - * 2^48 +-------------------+ - * | Kernel Page PDPT | --+ - * 2^48 - 2^39 +-------------------+ PPTR_BASE - * | TLB Bitmaps | | - * +-------------------+ | - * | | | - * | Unmapped | | - * | | | - * 0x0 +-------------------+ | - * | - * +-------------+ - * | - * v - * 2^48 +-------------------+ - * | | - * | | +------+ - * | Kernel Page Table | --> | PD | ----+ - * | | +------+ | - * | | | - * 2^48 - 2^30 +-------------------+ PPTR_TOP | - * | | | - * | Physical Memory | | - * | Window | | - * | | | - * +-------------------+ | - * | | | - * | | +------+ | - * | Kernel ELF | --> | PD | | - * | | +------+ | - * | | | - * +-------------------+ KERNEL_ELF_BASE | - * | | | - * | Physical Memory | | - * | Window | | - * | | | - * 2^48 - 2^39 +-------------------+ PPTR_BASE | - * | - * +---------------------+ - * | - * v - * 2^48 - 2^21 + 2^12 +-------------------+ - * | | - * | Kernel Devices | - * | | - * 2^48 - 2^21 +-------------------+ KDEV_BASE + * + * 2^48 +-------------------+ + * | | + * | Kernel Mem Region | ---+ (PUD) + * | | + * 2^48 - 2^39 +-------------------+ + * | | + * | | + * | Unmapped | + * | | + * | | + * 0x0 +-------------------+ + * + * + * For clarity, the diagrams are replicated below with adjusted + * virtual addresses. + * + * (PUD) + * | + * v + * 2^48 +-------------------+ + * | | + * | Kernel Mappings | --> (PD) + * | | + * 2^48 - 2^30 +-------------------+ PPTR_TOP + * | | + * | | + * | | + * | Physical Memory | + * | Window | + * | | + * | | + * | ----------------- | KERNEL_ELF_TOP + * | Kernel ELF | + * | ----------------- | KERNEL_ELF_BASE (at `physBase()`) + * | | + * | | + * 2^48 - 2^39 +-------------------+ PPTR_BASE + * + * + * (PD ) + * | + * v + * 2^48 +------------------+ + * | | + * | Kernel Devices | --> (PT) + * | | + * 2^48 - 2^21 +------------------+ KDEV_BASE + * | | + * | Log Buffer | + * | | + * 2^48 - 2 * 2^21 +------------------+ KS_LOG_BASE + * | | + * | | + * | Unmapped | + * | | + * | | + * 2^48 - 2^30 +------------------+ * */