RTOS/seL4
1
0
Fork 0
forked from Imagelibrary/seL4
Code Pull Requests Activity

aarch64,cortex-a53,hyp: Reduce seL4_UserTop value

Browse Source 
This ensures that no frames can be mapped that would overwrite the
currently stored VMID for the vspace.

Signed-off-by: Kent McLeod <kent@kry10.com>
This commit is contained in:
Kent McLeod
2020-10-15 15:35:47 +11:00
parent 40edd02c22
commit b86bce2d4b
2 changed files with 10 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
CHANGES
View File

@@ -28,6 +28,10 @@ Upcoming release: BREAKING
* aarch32: Moved TPIDRURO (PL0 Read-Only Thread ID register) to TCB register context from VCPU registers. This means
changes to this register from user level have to go via seL4_TCB_Write Registers instead of seL4_ARM_VCPU_WriteRegs.
* aarch64,cortex-a53,hyp: Reduce seL4_UserTop when on a cortex-a53 platform and KernelArmHypervisorSupport is set.
This is because the kernel uses the last slot in the top level VSpace object for storing the assigned VMID and so
any addresses that are addressed by the final slot are not accessible.
This would apply to any CPU that have 40bit stage 2 translation input address.
## Upgrade Notes
---

7
libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h
View File

@@ -260,6 +260,8 @@ SEL4_SIZE_SANITY(seL4_PUDEntryBits, seL4_PUDIndexBits, seL4_PUDBits);
#define seL4_IPCBufferSizeBits 10
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
/* 1 slot at the end of the vspace is used to hold the VMID assigned to the vspace */
#define seL4_VSpaceReservedSlots 1
/* The userspace occupies the range 0x0 to 0xfffffffffff.
* The stage-1 translation is disabled, and the stage-2
* translation input addree size is constrained by the
@@ -271,7 +273,10 @@ SEL4_SIZE_SANITY(seL4_PUDEntryBits, seL4_PUDIndexBits, seL4_PUDBits);
#if defined(CONFIG_ARM_PA_SIZE_BITS_44)
#define seL4_UserTop 0x00000fffffffffff
#elif defined(CONFIG_ARM_PA_SIZE_BITS_40)
#define seL4_UserTop 0x000000ffffffffff
/* Currently other definitions of seL4_UserTop already have free slots at the end and don't need to subtract for seL4_VSpaceReservedSlots.
* Each slot used requires subtracting 1GiB from the top address.
*/
#define seL4_UserTop (0x000000ffffffffff - seL4_VSpaceReservedSlots * 0x40000000)
#else
#error "Unknown physical address width"
#endif