[seL4] RPi4: DTS memory device and vm_minimal

Hi, I have been attempting to get the vm_minimal application running on the Raspberry Pi 4 platform, and I have managed to get to the point where I need to define the memory regions for the kernel and virtual machine. The issue is that I do not know what the correct values (if any) would be needed in the overlay-rpi4.dts that I have created. From what I have found to this point, the Pi platform implements a memory system that means it is not possible to define memory regions in a DTS file. These memory regions are user-defined and are not known until runtime. I think I know what the answer will be to this; is there a way to overcome the oddities of the RPi4 memory setup when attempting to create a seL4 CAmkES VM linux image? Thanks, Ben Turner Senior Engineer Roke Manor Research Ltd Tel: +44 (0)1794 833721 ben.turner@roke.co.uk<mailto:ben.turner@roke.co.uk> ________________________________________ 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. ________________________________________