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 <[email protected]> wrote: > On Tue, Aug 25, 2020 at 10:27 AM Michael Neises <[email protected]> > 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/dc354df3222766b9d36672575194e33f4edda9ac/vm-linux-helpers.cmake#L155 > > > > 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 > an > > executable to the filesystem, so I'm not sure how to begin debugging > 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.dts#L38 > ): > /* 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 > > [email protected] > > https://sel4.systems/lists/listinfo/devel > _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
