Hi Ben, The kernel requires knowledge of the platform layout at configuration/compilation time. My understanding is that on a platform like the RPI the RAM available for the CPU is shared with the GPU and while isn't statically defined, is still user controlled by a boot config file. Changes to the config file that change the amount of ram available to the kernel would require a reconfiguration of the kernel. You can take a look at how this is handled for the qemu-arm-virt platform, where the qemu instance can have an arbitrary amount of memory: https://github.com/seL4/seL4/blob/master/src/plat/qemu-arm-virt/config.cmake.... The build scripts update the dts based on how much memory is available. If you don't want to continuously change the kernel build upon changes to the RPI4's memory layout, you could fix a minimum size of memory that the kernel has as a memory node in the device tree. Any additional address ranges will still get given to userlevel as device untyped memory but will only be able to be used as frames and won't be able to be used for kernel objects that the kernel writes to, such as CNodes or page tables. Userlevel could then dynamically interpret the memory layout based on the supplied device tree and still use the memory that the GPU isn't using. The camkes-arm-vm/camkes also requires knowledge of what RAM will be at configuration/compilation time in order to statically allocate memory resources also.