Hi all,
I work on getting seL4 virtualization on Raspberry Pi 4 and I had to add few modifications to get the rpi4 in 64bit compiling, booting and passing the official test suite project.
Good new, it’s working, but I needed to relax a restriction (among other thing) in the parsing of dtb file (memory mapping) which seems stricter than necessary.
Explanation: In order to get closer to the final dtb, I retrieved the dynamic dtb from the Linux boot process and used it to get the sel4test test binary on rpi4 with 64bit.
Is there a reason for keeping strictly non overlapping memory region in the dtb mem region parsing?
(platform_sift.py l.84)
Second question, would it be interesting for the community to publish the cmake modification we’ve done to get rpi4 running?
Do you have an example test case for what you mean? Two regions that share a memory address shouldn’t be allowed, but two regions that are adjacent should be allowed. The regions described by the YAML file are what the kernel will create untypeds for. Any kernel objects that were overlapping would be a serious error so these regions need to be distinct. However if you are talking about a situation where a region starts at the same address as another ends and platform_sift.py rejects it then this could be an issue with the script.
By test case I mean something like the following YAML file that would be an input to the script:
I had this error when using the rpi4 dtb provided by the gpu at boot time. It presents the same configuration as in your example, where the end of a non device memory region is the starting point of the next non device memory (split for 64bit addressing space with dtb addresses in 32bits).
As a consequence, I had to accept this special case in platform_sift.py.
I think the issue is the tool that generates platform_gen.yaml should be merging the adjacent region node but isn’t. The separate regions mean that the kernel will treat the regions as separate and not create an untyped object that crosses the boundary. This could create a lot of fragmentation if the boundary has low alignment. We should likely modify the generation scripts to merge this regions in this case, and leave platform_sift to reject memory regions that are adjacent.
I also have this very same issue with imx8Mplus board which presents the following mapping.
In this case, the end is misleadingly shared between device and memory region.
devices:
end: 0x38800000
start: 0x0
end: 0x38880000
start: 0x38810000
end: 0x40000000
start: 0x38940000
end: 0xfffffff000
start: 0x1c0000000
memory:
end: 0x100000000
start: 0x40000000
end: 0x1c0000000
start: 0x100000000
I don’t get a clear view of the root cause of this issue. Is it due to a misinterpretation of FDT memory mapping or is it due to improper R1(end)==R2(start) check instead to use of a safer R1(end-1)==R2(start) check?
I can’t see where the end is shared with the two regions that you are referring to. These regions should be not end inclusive (ie [start, end)). Another way of representing them would be start and size where size is end - start. From looking at your examples, none of the regions are overlapping, but some memory regions could be merged (which is what your PR is addressing: Merge memory regions before checking for reserved areas by bvirfollet · Pull Request #350 · seL4/seL4 · GitHub).