[patch-axel-12] rework physical address space limits

CHANGES

@@ -44,6 +44,8 @@ Upcoming release: BREAKING
   This change is reflected in the definition of the seL4_UserTop constant that holds the largest user virtual address.
 * aarch32 VM fault messages now deliver original (untranslated) faulting IP in a hypervisor context, matching
   aarch64 behaviour.
+* Added CONFIG_PHYS_ADDR_SPACE_BITS (KernelPhysAddressSpaceBits), from this CONFIG_PHYS_ADDR_TOP (KernelPhysAddrTop)
+  gets derived in the generic CMake files. PADDR_USER_DEVICE_TOP (KernelPaddrUserTop) is kept as an alias.
 
 ## Upgrade Notes
 ---

config.cmake

@@ -202,7 +202,7 @@ if(DEFINED KernelDTSList AND (NOT "${KernelDTSList}" STREQUAL ""))
                 --compat-strings-out "${compatibility_outfile}" --c-header --header-out
                 "${device_dest}" --hardware-config "${config_file}" --hardware-schema
                 "${config_schema}" --yaml --yaml-out "${platform_yaml}" --sel4arch
-                "${KernelSel4Arch}" --addrspace-max "${KernelPaddrUserTop}"
+                "${KernelSel4Arch}" --phys-addr-space-bits "${KernelPhysAddressSpaceBits}"
             RESULT_VARIABLE error
         )
         if(error)
@@ -224,7 +224,13 @@ endif()
 
 # Enshrine common variables in the config
 config_set(KernelHaveFPU HAVE_FPU "${KernelHaveFPU}")
-config_set(KernelPaddrUserTop PADDR_USER_DEVICE_TOP "${KernelPaddrUserTop}")
+
+config_set(KernelPhysAddressSpaceBits PHYS_ADDR_SPACE_BITS "${KernelPhysAddressSpaceBits}")
+# Calculate the highest address that this still in the physical address space
+# here in CMake, so we derive integers that are inside the target's C inter
+# range.
+math(EXPR KernelPhysAddrTop "(1 << ${KernelPhysAddressSpaceBits}) - 1")
+config_set(KernelPhysAddrTop PHYS_ADDR_TOP "SEL4_WORD_CONST(${KernelPhysAddrTop})")
 
 # System parameters
 config_string(

include/arch/arm/arch/64/mode/hardware.h

@@ -215,8 +215,8 @@
    asserts check that the kernel config won't lead to UTs being created that aren't
    representable. */
 #ifndef __ASSEMBLER__
-compile_assert(ut_max_less_than_cannonical, CONFIG_PADDR_USER_DEVICE_TOP <= BIT(47));
+compile_assert(ut_max_less_than_cannonical, CONFIG_PHYS_ADDR_SPACE_BITS <= 47);
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
-compile_assert(ut_max_is_cannonical, (PPTR_BASE + CONFIG_PADDR_USER_DEVICE_TOP) <= BIT(48));
+compile_assert(ut_max_is_cannonical, PPTR_BASE + CONFIG_PHYS_ADDR_TOP <= BIT(48));
 #endif
 #endif

include/arch/riscv/arch/32/mode/hardware.h

@@ -31,7 +31,7 @@
 
 /* The first physical address to map into the kernel's physical memory
  * window */
-#define PADDR_BASE physBase
+#define PADDR_BASE ROUND_DOWN(physBase,22)
 
 /* The base address in virtual memory to use for the 1:1 physical memory
  * mapping */
@@ -48,13 +48,14 @@
 
 /* The physical memory address to use for mapping the kernel ELF
  *
- * This represents the physical address that the kernel image will be linked to. This needs to
- * be on a 1gb boundary as we currently require being able to creating a mapping to this address
- * as the largest frame size */
-#define KERNEL_ELF_PADDR_BASE UL_CONST(0x84000000)
+ * This represents the physical address that the kernel image will be linked to.
+ * physBase can be any value, but needs to be low enough within a single large page
+ * so that the kernel image doesn't cross a 2^22 mapping boundary.
+ */
+#define KERNEL_ELF_PADDR_BASE physBase
 
 /* The base address in virtual memory to use for the kernel ELF mapping */
-#define KERNEL_ELF_BASE UL_CONST(0xFF800000)
+#define KERNEL_ELF_BASE (UL_CONST(0xFF800000) + (KERNEL_ELF_PADDR_BASE & MASK(22)))
 
 /* The base address in virtual memory to use for the kernel device
  * mapping region. These are mapped in the kernel page table. */

include/arch/riscv/arch/64/mode/hardware.h

@@ -89,10 +89,8 @@
 #define PPTR_TOP UL_CONST(0xFFFFFFFF80000000)
 
 /* The physical memory address to use for mapping the kernel ELF */
-/* This represents the physical address that the kernel image will be linked to. This needs to
- * be on a 1gb boundary as we currently require being able to creating a mapping to this address
- * as the largest frame size */
-#define KERNEL_ELF_PADDR_BASE (physBase + UL_CONST(0x4000000))
+/* This represents the physical address that the kernel image will be linked to. */
+#define KERNEL_ELF_PADDR_BASE physBase
 
 /* The base address in virtual memory to use for the kernel ELF mapping */
 #define KERNEL_ELF_BASE (PPTR_TOP + (KERNEL_ELF_PADDR_BASE & MASK(30)))

include/config.h

@@ -13,8 +13,17 @@
 #define ENABLE_SMP_SUPPORT
 #endif
 
+/* keep some names for legacy compatibility */
+#ifdef CONFIG_ARCH_ARM
+#if (CONFIG_PHYS_ADDR_SPACE_BITS == 40)
+#define CONFIG_ARM_PA_SIZE_BITS_40 1
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
-#ifdef CONFIG_ARM_PA_SIZE_BITS_40
-#define AARCH64_VSPACE_S2_START_L1
-#endif
-#endif
+#define AARCH64_VSPACE_S2_START_L1 CONFIG_AARCH64_VSPACE_S2_START_L1
+#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
+#elif (CONFIG_PHYS_ADDR_SPACE_BITS == 44)
+#define CONFIG_ARM_PA_SIZE_BITS_44 1
+#endif /* PHYS_ADDR_SPACE_BITS */
+#endif /* CONFIG_ARCH_ARM */
+
+/* CONFIG_PADDR_USER_DEVICE_TOP is no longer set by the CMake configuration. */
+#define CONFIG_PADDR_USER_DEVICE_TOP CONFIG_PHYS_ADDR_TOP

src/arch/arm/config.cmake

@@ -10,39 +10,75 @@ if(KernelArchARM)
     set_property(TARGET kernel_config_target APPEND PROPERTY TOPLEVELTYPES pde_C)
 endif()
 
-set(KernelArmPASizeBits40 OFF)
-set(KernelArmPASizeBits44 OFF)
-if(KernelArmCortexA35)
+if(KernelArmCortexA7)
+    # nothing special
+elseif(KernelArmCortexA8)
+    # nothing special
+elseif(KernelArmCortexA9)
+    # nothing special
+elseif(KernelArmCortexA15)
+    # supports a 40-bit physical address space via LPAE
+elseif(KernelArmCortexA17)
+    # supports a 40-bit physical address space via LPAE
+elseif(KernelArmCortexA35)
     set(KernelArmICacheVIPT ON)
-    set(KernelArmPASizeBits40 ON)
-    math(EXPR KernelPaddrUserTop "(1 << 40)")
+    set(KernelPhysAddressSpaceBits 40)
 elseif(KernelArmCortexA53)
     set(KernelArmICacheVIPT ON)
-    set(KernelArmPASizeBits40 ON)
-    math(EXPR KernelPaddrUserTop "(1 << 40)")
+    set(KernelPhysAddressSpaceBits 40)
 elseif(KernelArmCortexA55)
     set(KernelArmICacheVIPT ON)
-    set(KernelArmPASizeBits40 ON)
-    math(EXPR KernelPaddrUserTop "(1 << 40)")
+    set(KernelPhysAddressSpaceBits 40)
 elseif(KernelArmCortexA57)
-    set(KernelArmPASizeBits44 ON)
-    math(EXPR KernelPaddrUserTop "(1 << 44)")
+    set(KernelPhysAddressSpaceBits 44)
+#elseif(KernelArmCortexA65)
+#    set(KernelPhysAddressSpaceBits 44)
 elseif(KernelArmCortexA72)
-    # For Cortex-A72 in AArch64 state, the physical address range is 44 bits
-    # (https://developer.arm.com/documentation/100095/0001/memory-management-unit/about-the-mmu)
-    set(KernelArmPASizeBits44 ON)
-    math(EXPR KernelPaddrUserTop "(1 << 44)")
+    # https://developer.arm.com/documentation/100095/0003/Memory-Management-Unit/About-the-MMU
+    set(KernelPhysAddressSpaceBits 44)
+#elseif(KernelArmCortexA73)
+#    set(KernelPhysAddressSpaceBits 40)
+#elseif(KernelArmCortexA75)
+#    set(KernelPhysAddressSpaceBits 44)
+#elseif(KernelArmCortexA76)
+#    set(KernelPhysAddressSpaceBits 40)
+#elseif(KernelArmCortexA77)
+#    set(KernelPhysAddressSpaceBits 40)
+#elseif(KernelArmCortexA78)
+#    set(KernelPhysAddressSpaceBits 40)
+#elseif(KernelArmCortexA78AE)
+#    set(KernelPhysAddressSpaceBits 48)
+#elseif(KernelArmCortexA510)
+#    set(KernelPhysAddressSpaceBits 40)
+#elseif(KernelArmCortexA710)
+#    set(KernelPhysAddressSpaceBits 40)
+else()
+    # In ARMv8, ID_AA64MMFR0_EL1.PARange gives the physical address space size,
+    # values are:
+    #   0:     32 bits (4 GB)
+    #   1:     36 bits (64 GB)
+    #   2:     40 bits (1 TB)
+    #   3:     42 bits (4 TB)
+    #   4:     44 bits (16 TB)
+    #   5:     48 bits (256 TB)
+    #   6:     52 bits (4 PB, added in Armv8.2-A, implies FEAT_LPA)
+    #   7-15:  reserved
+    # A general comparison table for can be found at
+    # https://developer.arm.com/-/media/Arm%20Developer%20Community/PDF/Cortex-A%20R%20M%20datasheets/Arm%20Cortex-A%20Comparison%20Table_v4.ashx
+    message(FATAL_ERROR "unsupported ARM core")
 endif()
-config_set(KernelArmPASizeBits40 ARM_PA_SIZE_BITS_40 "${KernelArmPASizeBits40}")
-config_set(KernelArmPASizeBits44 ARM_PA_SIZE_BITS_44 "${KernelArmPASizeBits44}")
+
 config_set(KernelArmICacheVIPT ARM_ICACHE_VIPT "${KernelArmICacheVIPT}")
 
+# In 32-bit mode (AARCH32) seL4 can handle a maximum physical address space of
+# 32 bits, even if the core supports LPAE that technically allows mapping pages
+# from larger addresses.
 if(KernelSel4ArchAarch32)
-    # 64-bit targets may be building in 32-bit mode,
-    # so make sure maximum paddr is 32-bit.
-    math(EXPR KernelPaddrUserTop "(1 << 32) - 1")
+    set(KernelPhysAddressSpaceBits 32)
 endif()
 
+config_set(KernelArmICacheVIPT ARM_ICACHE_VIPT "${KernelArmICacheVIPT}")
+
 include(src/arch/arm/armv/armv7-a/config.cmake)
 include(src/arch/arm/armv/armv8-a/config.cmake)
 
@@ -91,7 +127,7 @@ config_option(
 
 config_option(KernelArmGicV3 ARM_GIC_V3_SUPPORT "Build support for GICv3" DEFAULT OFF)
 
-if(KernelArmPASizeBits40 AND ARM_HYPERVISOR_SUPPORT)
+if((KernelPhysAddressSpaceBits EQUAL 40) AND ARM_HYPERVISOR_SUPPORT)
     config_set(KernelAarch64VspaceS2StartL1 AARCH64_VSPACE_S2_START_L1 "ON")
 else()
     config_set(KernelAarch64VspaceS2StartL1 AARCH64_VSPACE_S2_START_L1 "OFF")

src/arch/riscv/config.cmake

@@ -50,21 +50,25 @@ endif()
 
 if(KernelSel4ArchRiscV32)
     set(KernelPTLevels 2 CACHE STRING "" FORCE)
-endif()
-if(KernelPTLevels EQUAL 2)
-    if(KernelSel4ArchRiscV32)
-        # seL4 on RISCV32 uses 32-bit ints for addresses,
-        # so limit the maximum paddr to 32-bits.
-        math(EXPR KernelPaddrUserTop "(1 << 32) - 1")
+    # Actually, RV32 with Sv32 supports a 34-bit (16 GiByte) physical address
+    # space. However, we only support a 32-bit address space at the moment when
+    # targeting 32-bit architectures.
+    set(KernelPhysAddressSpaceBits 32)
+elseif(KernelSel4ArchRiscV64)
+    # The RISC-V privileged spec v1.12 defines that RV64 always uses a 56-bit
+    # physical address space.
+    if(KernelPTLevels EQUAL 3)
+        # structures.bf limits us to a 39-bit physical address space in Sv39
+        # mode with a 39-bit VA space and 3 page table levels
+        set(KernelPhysAddressSpaceBits 39)
     else()
-        math(EXPR KernelPaddrUserTop "1 << 34")
+        # Sv48: 48-bit VA space with 4 page table levels (unsupported)
+        # Sv57: 57-bit VA space with 5 page table levels (unsupported)
+        # Sv64: details still unclear
+        message(FATAL_ERROR "KernelPTLevels=${KernelPTLevels} is unsupported")
     endif()
-elseif(KernelPTLevels EQUAL 3)
-    # RISC-V technically supports 56-bit paddrs,
-    # but structures.bf limits us to using 39 of those bits.
-    math(EXPR KernelPaddrUserTop "1 << 39")
-elseif(KernelPTLevels EQUAL 4)
-    math(EXPR KernelPaddrUserTop "1 << 56")
+else()
+    message(FATAL_ERROR "unsuppored RISC-V architecture")
 endif()
 
 if(KernelRiscvExtD)

src/arch/riscv/kernel/vspace.c

@@ -108,6 +108,8 @@ BOOT_CODE VISIBLE void map_kernel_window(void)
     /* mapping of KERNEL_ELF_BASE (virtual address) to kernel's
      * KERNEL_ELF_PHYS_BASE  */
     assert(CONFIG_PT_LEVELS > 1 && CONFIG_PT_LEVELS <= 4);
+    /* Kernel image finishes before KDEV_BASE */
+    assert(KDEV_BASE >= (word_t)ki_end);
 
     /* kernel window starts at PPTR_BASE */
     word_t pptr = PPTR_BASE;

src/arch/x86/config.cmake

@@ -346,9 +346,9 @@ config_option(
 
 if(KernelSel4ArchIA32)
     set(KernelSetTLSBaseSelf ON)
-    math(EXPR KernelPaddrUserTop "0xffff0000")
+    set(KernelPhysAddressSpaceBits 32)
 else()
-    math(EXPR KernelPaddrUserTop "1 << 47")
+    set(KernelPhysAddressSpaceBits 47)
 endif()
 if(KernelSel4ArchX86_64 AND NOT KernelFSGSBaseInst)
     set(KernelSetTLSBaseSelf ON)

src/kernel/boot.c

@@ -666,9 +666,10 @@ BOOT_CODE bool_t create_untypeds(cap_t root_cnode_cap,
         start = ndks_boot.reserved[i].end;
     }
 
-    if (start < CONFIG_PADDR_USER_DEVICE_TOP) {
+    if (start < CONFIG_PHYS_ADDR_TOP) {
         region_t reg = paddr_to_pptr_reg((p_region_t) {
-            start, CONFIG_PADDR_USER_DEVICE_TOP
+            .start = start,
+            .end = CONFIG_PHYS_ADDR_TOP
         });
 
         if (!create_untypeds_for_region(root_cnode_cap, true, reg, first_untyped_slot)) {

src/plat/ariane/overlay-ariane.dts

@@ -1,5 +1,6 @@
 /*
  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ * Copyright 2021, HENSOLDT Cyber
  *
  * SPDX-License-Identifier: GPL-2.0-only
  */
@@ -9,4 +10,20 @@
 		seL4,kernel-devices =
 		    &{/soc/interrupt-controller@c000000};
 	};
+
+    /* Reserve 2 MiB for SBI at the start of RAM (0x80000000 - 0x80200000). This
+     * is exactly one "megapage" in the MMU table. It leaves plenty of space for
+     * further SBI experimenting, given the known usage (as of June 2021) is:
+     * - BBL: 76 KiB (= 0x13000)
+     * - OpenSBI: 128 KiB (= 0x20000) with PMP protection
+     */
+    reserved-memory {
+        #address-cells = <0x01>;
+        #size-cells = <0x01>;
+        ranges;
+        sbi@80000000 {
+            reg = <0x80000000 0x200000>;
+            no-map;
+        };
+    };
 };

src/plat/hifive/overlay-hifive.dts

@@ -1,5 +1,6 @@
 /*
  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ * Copyright 2021, HENSOLDT Cyber
  *
  * SPDX-License-Identifier: GPL-2.0-only
  */
@@ -9,4 +10,22 @@
 		seL4,kernel-devices =
 		    &{/soc/interrupt-controller@c000000};
 	};
+
+    reserved-memory {
+        #address-cells = <0x01>;
+        #size-cells = <0x01>;
+        ranges;
+
+        /* Reserve 2 MiB for SBI at the start of RAM (0x80000000 - 0x80200000).
+         * This is exactly one "megapage" in the MMU table. It leaves plenty of
+         * space for further SBI experimenting, given the known usage (as of
+         * June 2021) is:
+         * - BBL: 76 KiB (= 0x13000)
+         * - OpenSBI: 128 KiB (= 0x20000) with PMP protection
+         */
+        sbi@80000000 {
+            reg = <0x80000000 0x200000>;
+            no-map;
+        };
+    };
 };