iMX8MM boot failure with 8GiB of memory

seL4 kernel
1

We have been running with seL4 12.1.0 on an iMX8MM EVK with 2GiB of memory.

We have spun our own hardware and increased memory to 8GiB and up to now we’ve been running with the same memory profile as the EVK version of the code. But we now require some of that extra memory to be used.

The first problem I am having is that if inform seL4 that it has 8GiB of memory available it locks up during boot

memory@40000000 {
	device_type = "memory";
	reg = <0x00 0x40000000 0x02 0x00000000>;	// 8 GiB - boot fails
};

After some enabling of debug I have managed to get this output

Ignoring call to sys_rt_sigprocmask
Ignoring call to sys_gettid
sys_tkill assuming self kill
seL4 root server abort()ed
Debug halt syscall from user thread 0x823f86a400 “rootserver”
halting…
Kernel entry via Unknown syscall, word: 1

If I reduce the available memory down to 7GiB

memory@40000000 {
	device_type = "memory";
	reg = <0x00 0x40000000 0x01 0xC0000000>;	// 7 GiB boot ok
};

The system boots as expected.

A second weird issue is where I reserve vm-memory

    vm-memory@40000000 {
        reg = <0x0 0x40000000 0x0 0x50000000>;
        no-map;
    };

The above definition works fine and I can run 2 VMs one with 1GiB and the other with 0.25GiB of memory.

Increasing the vm-memory (without changing any of the VM attributes also causes the system to not boot successfully.

For example, here I want to reserve 5GiB leaving 2GiB (should be 3 if the 1st problem is fixed!) available for seL4.

    vm-memory@40000000 {
        reg = <0x0 0x40000000 0x1 0x40000000>;
        no-map;
    };

Bit baffled at the moment and trying to figure out what might be wrong but hoping somebody out there may provide that bit of knowledge that fixes things.

Thanks,
Zippy

2

For the 8GB problem, try the seL4 head version from git and see if it persist.

For the VM reserved memory, there might be some assumption somewhere in user space that the region is covered with one untyped memory. If so, the region must be power-of-two sized and aligned. Alternatively, it may get fragmented into more untyped caps than the sw can deal with.