Thanks for the reply. I think your last point is the issue that I was having. I had almost
everything working for the RPi4, however when I attempted to build the CAmkES project I
could never seem to provide enough memory even though it compiled correctly. This meant
that during boot I would get several untyped-retype errors, the number of which would
depend on how much memory I declared in the overlay-dts.
My efforts were focused on simply attempting to get the vm_minimal project working, but
due to the memory above 1GB being treated as highmem I had no way of addressing the rest
of this at compile time, so I was stuck with the initial 1GB which just didn't seem
to be enough to run the vm_minimal project. This did surprise me, and I wonder if you have
any insight into the requirements of the vm_minimal image and why this might have
Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the
Registered in England & Wales. Registered No: 00267550
The information contained in this e-mail and any attachments is proprietary to Roke Manor
Research Limited and
must not be passed to any third party without permission. This communication is for
information only and shall
not create or change any contractual relationship.
From: Mcleod, Kent (Data61, Kensington NSW) <Kent.Mcleod(a)data61.csiro.au>
Sent: 18 March 2020 01:43
To: Turner, Ben <ben.turner(a)roke.co.uk>uk>; devel(a)sel4.systems
Subject: Re: RPi4: DTS memory device and vm_minimal
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:
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.