forked from Imagelibrary/seL4
aarch64: fixup address space layout docs for hyp
Fixes #957 I removed the notes about TK1 since it's not just TK1. Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
This commit is contained in:
Julia Vassiliki
committed by
Indan Zupancic
Indan Zupancic
parent
57a909f615
commit
7099f9d543
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user