Re: [seL4] "Ran out of untyped memory"

25 Aug 2020

      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