[Elfloader] Memory mapping boundaries

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?

Pull Requests on GitHub are always appreciated!

1 Like

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:

devices:
- end: 0x8000000
  start: 0x0
- end: 0x8010000
  start: 0x8001000
- end: 0x40000000
  start: 0x8011000
- end: 0xfffff000
  start: 0x80000000
memory:
- end: 0x80000000
  start: 0x40000000

Hi Kent,

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.

Hi Kent,

The yaml file causing this error is:
devices:

  • end: 0x40000000
    start: 0x3b400000
  • end: 0xff800000
    start: 0xfc000000
  • end: 0xff841000
    start: 0xff801000
  • end: 0xff844000
    start: 0xff843000
  • end: 0x100000000
    start: 0xff845000
  • end: 0xffffffff000
    start: 0x200000000
    memory:
  • end: 0x3b400000
    start: 0x0
  • end: 0xfc000000
    start: 0x40000000
  • end: 0x180000000
    start: 0x100000000
  • end: 0x200000000
    start: 0x180000000

If I understand well, get_memory_regions in memory.py is the best place to merge memory regions before checking for reserved ones. Do you agree?

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: https://github.com/seL4/seL4/pull/350).

I think your PR is appropriate. Thanks!