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.cmak…. 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.