Re: [seL4] RPi4: DTS memory device and vm_minimal

Hi Ben, Getting the memory configurations right can become pretty annoying as there are several different ways the memory can be insufficient and given that some of the "Untyped Retype: Insufficient memory" emitted are spurious it can quickly become pretty impossible to debug it all.  (There are some pending kernel patches that should remove the spurious kernel error messages). The memory requirements for a VM component in the vm_minimal app configuration come from a series of different constraints: - The Ram device that gets given to the guest needs to be directly mapped if the guest has access to any DMA capable devices and there isn't an IOMMU available to support a virtual-physical address space. - The VMM needs enough untyped objects to create all of the additional kernel objects required to support creating the guest.  These get used for creating threads, paging structures, VCPU objects etc. - In addition, camkes implicitly allocates the untyped objects required for setting up the VMMs address space and backing data for its code and data program segments. - All of these objects are initially allocated by the capdl-loader-app which has to be able to allocate everything from the initial untyped objects that the kernel provides to it at boot time. - The kernel creates the initial untypeds based on the static description of Ram it has, minus any memory that it uses for its own static memory usage. So when you try and run an app you can see an allocation failure it could be due to: - There isn't enough memory available in the system for the ELFLoader to load the kernel and user programs into. The system will crash before the kernel even has a chance to start. - The kernel doesn't have enough memory available to create the initial objects required to finish initializing it and the first user task (the capdl-loader-app).  The kernel init would crash at this point. - Then when the capdl-loader-app runs, the untypeds that it has been given may not be enough to fit all of the objects that it needs to create into.  The loader would print an error and crash at this point. - Then once the camkes VM component starts it might run out of memory while trying to setup the VM if it hasn't been configured properly. Or it might not have been given the untypeds corresponding to the exact Ram range it requires for creating the guest's Ram device.  - Then once the guest is started, it may run out of Ram while trying to bring up Linux.  And then Linux will print its own error message (or everything will appear to hang if this occurs before Linux has started writing to a console). Debugging these failures requires knowing which memory setting to change based on what part is failing. - vm0.simple_untyped24_pool = 12;  is the camkes configuration used to give 12 * 2^24 Untyped objects to the vm component.  If it is running out of memory while trying to setup the VM then increasing this is required. - vm0.untyped_mmios = ["0x40000000:28"]; // RAM is the configuration for giving the component the exact region of memory from [0x40000000, 0x40000000 + 2^28). If this can't be given to the component then the capdl-loader-app would print an error and stop loading the system.  If this happens, then that means either the kernel isn't making the right untypeds available at start up or that some other camkes component is trying to use the same memory. If the error is because of the first case, then we usually turn to creating a reserved region description in the device tree file for that platform so that the kernel doesn't use the memory and it is therefore ensured to be in the initial set of untypeds passed to memory. If there is less memory available in the system than what the camkes components are requesting, then the above configuration options need to be reduced if memory can't be unlocked from elsewhere somehow. On a system with at least 1GiB of memory available then it is more common that these options are too low or way too high. I'm not quite sure what you mean about the 1GB highmem issue sorry. Are you able to elaborate more? Kent.