Thank you for your fast response, Kent. Is there a way for me to use the remaining 1.5GiB to create other kernel objects? It's important not only that I have the two calls I mentioned previously, but also I will later add a third camkes component, which I believe will exacerbate the problem. I don't know much about capDL yet, so any pointers would be greatly appreciated. Best, Michael On Mon, Aug 24, 2020 at 10:23 PM Kent Mcleod wrote:

On Tue, Aug 25, 2020 at 10:27 AM Michael Neises wrote:

...

Hello,

I'm trying to build a camkes app, but when I attempt to run it on an Odroid-xu4, I get the following error just before the boot halts:

"Ran out of untyped memory while creating objects"

I've narrowed the error down to two calls to a this function:

https://github.com/SEL4PROJ/camkes-vm-linux/blob/dc354df3222766b9d3667257519...

...

When I use only one call, the image boots nicely. If I use both calls, I get the above error. My understanding is that this function simply adds

...

executable to the filesystem, so I'm not sure how to begin debugging

an this.

...

Is it possible that the filesystem is actually "too big" for sel4 to boot successfully?

This is likely the issue. This is the odroid-xu4 memory definition that Untypeds are created out of ( https://github.com/seL4/seL4/blob/master/src/plat/exynos5/overlay-exynos5422... ): /* HACK: 0xe0000000..0xff000000 is the largest contiguous region * in the kernel window; we clamp to that and discard memory * after the ASID PD hole (0xff200000..0xfff00000). This is a * workaround for userspace tools (hardware_gen, elfloader, etc) * which are not yet aware of the memory hole. */ memory@40000000 { reg = <0x60000000 0x1f000000>; };

vm-memory@40000000 { reg = <0x40000000 0x20000000>; };

That's setting the memory node to ~512MiB, so if your capDL spec is trying to declare more objects than can be created by that amount of memory, the loader will run out of untypeds and generate the error that you see. Assuming that the odroid-xu4 has 2GiB of memory available, there is still 1.5GiB that is accessible as device untyped (which can be used to create memory mappings, but not to create other kernel objects such as CNodes) but by default the capDL loader doesn't currently know how to use these for creating pages out of.

...

Please advise!

Best, Michael Neises _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

On Tue, 25 Aug 2020, 15:04 Heiser, Gernot (Data61, Kensington NSW), wrote:

On 25 Aug 2020, at 14:51, Michael Neises mailto:neisesmichael@gmail.com> wrote:

Is there a way for me to use the remaining 1.5GiB to create other kernel objects? It's important not only that I have the two calls I mentioned previously, but also I will later add a third camkes component, which I believe will exacerbate the problem. I don't know much about capDL yet, so any pointers would be greatly appreciated.

Any kernel objects (i.e. kernel metadata objects such as page tables, TCBs, Cnodes etc) must be allocated in 0.5GiB the kernel window to be accessible. However, unless you’re building an extremely unusual system, you shouldn’t need 0.5GiB of kernel objects. Frames that can only be mapped into address spaces can be created from “device untyped”, without using up the 0.5GiB kernel window.

In this case it is most likely the frames from loading the initial ELF binaries (one of which contains the large Linux images in the .data sections). However, there is a limitation on which frames can be created from device untyped as the kernel won't let you perform cache maintenance operations (required for unifying the icache when starting the system) on device untyped as this could cause a kernel abort if a virtual address doesn't correspond to valid memory. There seems to be at least 2 ways for increasing the Linux kernel limit: - Change the Camkes/capDL tooling to try and allocate all non-executable segments in all of the ELFs to device untyped frames - Fix the issue on aarch32 hyp where the kernel window is unnecessarily limited to .5GiB as it executes in its own EL2 address space that isn't shared with User apps and so could use the full 4GiB.

Gernot _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel