Hi Kent,
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 happened?
Thanks,
Ben
________________________________________
Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group.
Registered in England & Wales. Registered No: 00267550
http://www.roke.co.uk
_______________________________________
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)
Sent: 18 March 2020 01:43
To: Turner, Ben ; devel@sel4.systems
Subject: Re: RPi4: DTS memory device and vm_minimal
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...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.
