[patch-axel-29a] QEMU 32-bit RAM

src/plat/qemu-arm-virt/config.cmake

@@ -130,12 +130,19 @@ if(KernelPlatformQEMUArmVirt)
             endif()
 
             if(NOT DEFINED QEMU_MEMORY)
-                # Having 1 GiB of memory as default is a legacy from the past
-                # that is kept for compatibility. It should be increased to
-                # 2 GiB, which seems a good trade-off nowadays. It's sufficient
-                # for test/demo systems, but still something the host can
-                # provide without running short on resources.
-                set(QEMU_MEMORY "1024")
+                if(KernelSel4ArchAarch32)
+                    # The memory starts at 1 GiB (0x40000000), so 3 GiB can be
+                    # accessed using 32-bit addresses. While the LPAE MMU model
+                    # supports accessing a 1 TiB (40-bit) physical address
+                    # space, the 32-bit version of seL4 can access physical
+                    # addresses in the 32-bit range only.
+                    set(QEMU_MEMORY "8192")
+                else()
+                    # Having 3 GiB of memory as default seems a good trade-off.
+                    # It's sufficient for test/demo systems, but still something
+                    # the host can provide without running short on resources.
+                    set(QEMU_MEMORY "3072")
+                endif()
             endif()
 
             if(KernelMaxNumNodes)
@@ -219,6 +226,10 @@ if(KernelPlatformQEMUArmVirt)
 
     list(APPEND KernelDTSList "${QEMU_DTS}" "${CMAKE_CURRENT_LIST_DIR}/overlay-qemu-arm-virt.dts")
 
+    if(KernelSel4ArchAarch32)
+        list(APPEND KernelDTSList "${CMAKE_CURRENT_LIST_DIR}/overlay-qemu-arm-virt32.dts")
+    endif()
+
     if(KernelArmHypervisorSupport OR KernelSel4ArchArmHyp)
         list(APPEND KernelDTSList "${CMAKE_CURRENT_LIST_DIR}/overlay-reserve-vm-memory.dts")
     endif()

src/plat/qemu-arm-virt/overlay-qemu-arm-virt32.dts

@@ -0,0 +1,29 @@
+/*
+ * Copyright 2022, HENSOLDT Cyber
+ *
+ *  * SPDX-License-Identifier: BSD-3-Clause
+ */
+
+/ {
+    reserved-memory {
+        #address-cells = <0x02>;
+        #size-cells = <0x02>;
+        ranges;
+
+        /* The 32-bit version of seL4 can handle a 32-bit physical
+         * address space (4 GiB) only, even if LPAE allows using a
+         * 40-bit physical address space. For now, reserving any memory
+         * starting at 0xffffffff is the easiest way to cope with
+         * platform configurations having pyhsical memory of exactly
+         * 4 GiB or above. The long-term fix is improving the seL4 build
+         * scripts to be aware of the 4 GiB limitation and never create
+         * any regions above. Furthermore, a way needs to be found to
+         * support using exactly 4 GiB also.
+         */
+        reserved-memory@ffffffff{
+            reg = < 0x00000000 0xffffffff 0xffffffff 0x00000001 >;
+            no-map;
+        };
+
+    };
+};

src/plat/qemu-riscv-virt/config.cmake

@@ -189,6 +189,10 @@ if(KernelPlatformQEMURiscVVirt)
 
     list(APPEND KernelDTSList "${QEMU_DTS}" "${CMAKE_CURRENT_LIST_DIR}/overlay-qemu-riscv-virt.dts")
 
+    if(KernelSel4ArchRiscV32)
+        list(APPEND KernelDTSList "${CMAKE_CURRENT_LIST_DIR}/overlay-qemu-riscv-virt32.dts")
+    endif()
+
     # QEMU emulates a SiFive PLIC/CLINT with 127 interrupt sources by default.
     # The CLINT timer pretends to run at 10 MHz, but this speed may not hold in
     # practical measurements.

src/plat/qemu-riscv-virt/overlay-qemu-riscv-virt32.dts

@@ -0,0 +1,29 @@
+/*
+ * Copyright 2022, HENSOLDT Cyber
+ *
+ *  * SPDX-License-Identifier: BSD-3-Clause
+ */
+
+/ {
+    reserved-memory {
+        #address-cells = <0x02>;
+        #size-cells = <0x02>;
+        ranges;
+
+        /* The 32-bit version of seL4 can handle a 32-bit physical
+         * address space (4 GiB) only, even if SV32 allows using a
+         * 34-bit physical address space. For now, reserving any memory
+         * starting at 0xffffffff is the easiest way to cope with
+         * platform configurations having pyhsical memory of exactly
+         * 4 GiB or above. The long-term fix is improving the seL4 build
+         * scripts to be aware of the 4 GiB limitation and never create
+         * any regions above. Furthermore, a way needs to be found to
+         * support using exactly 4 GiB also.
+         */
+        reserved-memory@ffffffff{
+            reg = < 0x00000000 0xffffffff 0xffffffff 0x00000001 >;
+            no-map;
+        };
+
+    };
+};