diff --git a/include/arch/arm/arch/64/mode/hardware.h b/include/arch/arm/arch/64/mode/hardware.h index a4b42ace5..75faddb7f 100644 --- a/include/arch/arm/arch/64/mode/hardware.h +++ b/include/arch/arm/arch/64/mode/hardware.h @@ -45,11 +45,9 @@ * 2^64 - 2^48 +-------------------+ --+ * | | * | | - * | | * | Unaddressable | * | | * | | - * | | * 2^48 +-------------------+ --+ * | Unmapped | | * +-------------------+ USER_TOP | @@ -79,7 +77,6 @@ * 2^64 - 2^30 +-------------------+ PPTR_TOP * | | * | | - * | | * | Physical Memory | * | Window | * | | @@ -106,11 +103,11 @@ * | | * | Kernel Devices | --> (PT) * | | - * 2^64 - 2^21 +------------------+ KDEV_BASE + * 2^64 - 2^21 +------------------+ KDEV_BASE / KERNEL_PT_BASE * | | * | Log Buffer | * | | - * 2^64 - 2 * 2^21 +------------------+ KS_LOG_BASE + * 2^64 - 2 * 2^21 +------------------+ KS_LOG_PPTR * | | * | | * | Unmapped | @@ -127,69 +124,78 @@ * The EL2 mode kernel uses TTBR0_EL2 which covers the range of * 0x0 - 0x0000ffffffffffff (48 bits of vaddrspace). * - * The CPU on the TX1 only allows for 48-bits of addressable virtual memory. - * Within the seL4 EL2 kernel's separate vaddrspace, it uses - * the 512 GiB at the top of that 48 bits of addressable - * virtual memory. - * + * 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). * 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: + * The major difference to non-hyp mode, is that the kernel mem region is + * located in the second entry of the TTBR0_EL2 page table (PGD) rather than + * the topmost. This is because: * - * +-----------------------------------+ <- 0xFFFFFFFF_FFFFFFFF - * | Canonical high portion - unusable | - * | virtual addrs | - * +-----------------------------------+ <- PPTR_TOP: 256TiB mark (top of 48 bits) - * | seL4 EL2 kernel | ^ - * | | | - * | | 512GiB - * | | of EL2 kernel windowing - * | | into memory. - * | | | - * | | v - * +-----------------------------------+ <- PPTR_BASE: 256TiB minus 512GiB. - * | Unused virtual addresses within | ^ - * | the EL2 kernel's | | - * | separate vaddrspace. | Rest of the - * | | EL2 kernel - * | | vaddrspace, unused, - * | | which is the rest of - * | | the lower 256 TiB. - * | | | - * | | v - * +-----------------------------------+ <- 0x0 + * - The kernel expects to be able to create untypeds from 0 to + * KernelPaddrUserTop (CONFIG_PADDR_USER_TOP) which can be up to 2^44 in + * the current kernel. The kernel (proofs) expect addresses in these + * untypeds to be valid (i.e. canonical, not dereferencable) virtual + * addresses, but allows device UT addresses to exceed ("overflow") the + * bounds of the physical memory window (PPTR_BASE...PPTR_TOP) as it will + * not dereference them itself. In the EL1 translation regime, as we use + * the "upper VA" these kind of address overflows remain canonical as + * they wraparound into the "lower VA", which still consists of valid + * addresses. In the EL2 translation regime, which uses TTBR0_EL2 and + * virtual addresses are always between [0, 2^48), when we exceed the + * top of this address range the virtual addresses are non-canonical, + * and therefore no longer valid. * - * 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). + * The solution was to move the physical memory window (and thus the + * offset between physical and virtual addresses) down such that the full + * UT paddr range of 2^44 can fit within [0, 2^48). This likely will not + * work when the kernel implements adds support for 48-bit PA. + * + * - We use the second entry, not the first, as the lowest 512GiB of + * virtual addresses conflicted elfloader's direct mapping during boot. + * + * - Also see commit a94d90598fec484636b14e1b8d3643156e1e27b1, which + * introduced this behaviour. + * + * This gives us the address range from 2^39 to 2^40 (2^39 + 2^39). + * + * For clarity, the diagrams are replicated below with adjusted + * virtual addresses. * * + * 2^64 +-------------------+ + * | | + * | | + * | Unaddressable | + * | | + * | | * 2^48 +-------------------+ * | | - * | Kernel Mem Region | ---+ (PUD) - * | | - * 2^48 - 2^39 +-------------------+ - * | | * | | * | Unmapped | * | | * | | + * 2^40 +-------------------+ + * | | + * | Kernel Mem Region | ---+ (PUD) + * | | + * 2^39 +-------------------+ + * | | + * | Unmapped | + * | | * 0x0 +-------------------+ * * - * For clarity, the diagrams are replicated below with adjusted - * virtual addresses. - * * (PUD) * | * v - * 2^48 +-------------------+ + * 2^40 +-------------------+ * | | * | Kernel Mappings | --> (PD) * | | - * 2^48 - 2^30 +-------------------+ PPTR_TOP + * 2^40 - 2^30 +-------------------+ PPTR_TOP * | | * | | * | | @@ -202,27 +208,27 @@ * | ----------------- | KERNEL_ELF_BASE (at `physBase()`) * | | * | | - * 2^48 - 2^39 +-------------------+ PPTR_BASE + * 2^40 - 2^39 +-------------------+ PPTR_BASE * * * (PD ) * | * v - * 2^48 +------------------+ + * 2^40 +------------------+ * | | * | Kernel Devices | --> (PT) * | | - * 2^48 - 2^21 +------------------+ KDEV_BASE + * 2^40 - 2^21 +------------------+ KDEV_BASE / KERNEL_PT_BASE * | | * | Log Buffer | * | | - * 2^48 - 2 * 2^21 +------------------+ KS_LOG_BASE + * 2^40 - 2 * 2^21 +------------------+ KS_LOG_PPTR * | | * | | * | Unmapped | * | | * | | - * 2^48 - 2^30 +------------------+ + * 2^40 - 2^30 +------------------+ * */ @@ -236,16 +242,16 @@ /* The base address in virtual memory to use for the 1:1 physical memory * mapping */ #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT -#define PPTR_BASE UL_CONST(0x0000008000000000) +#define PPTR_BASE UL_CONST(0x0000008000000000) /* 2^40 - 2^39 */ #else -#define PPTR_BASE UL_CONST(0xffffff8000000000) +#define PPTR_BASE UL_CONST(0xffffff8000000000) /* 2^64 - 2^39 */ #endif -/* Top of the physical memory window */ +/* Top of the physical memory window, exclusive */ #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT -#define PPTR_TOP UL_CONST(0x000000ffc0000000) +#define PPTR_TOP UL_CONST(0x000000ffc0000000) /* 2^40 - 2^30 */ #else -#define PPTR_TOP UL_CONST(0xffffffffc0000000) +#define PPTR_TOP UL_CONST(0xffffffffc0000000) /* 2^64 - 2^30 */ #endif /* The physical memory address to use for mapping the kernel ELF */ @@ -259,11 +265,11 @@ #define KERNEL_ELF_BASE_RAW (PPTR_BASE_OFFSET + KERNEL_ELF_PADDR_BASE_RAW) /* This is a page table mapping at the end of the virtual address space - * to map objects with 4KiB pages rather than 4MiB large pages. */ + * to map objects with 4KiB pages rather than 2MiB large pages. */ #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT -#define KERNEL_PT_BASE UL_CONST(0x000000ffffe00000) +#define KERNEL_PT_BASE UL_CONST(0x000000ffffe00000) /* 2^40 - 2^21 */ #else -#define KERNEL_PT_BASE UL_CONST(0xffffffffffe00000) +#define KERNEL_PT_BASE UL_CONST(0xffffffffffe00000) /* 2^64 - 2^21 */ #endif /* The base address in virtual memory to use for the kernel device