Adding rockpro64 to sel4cp hello world example

New to seL4
1

I am attempting to build the @ivanvelickovic fork of the sel4cp hello world example for the rockpro64 board. I saw that the board is supported by sel4 and had platform files included in the seL4 repo. I successfully ran sel4test on the board. My attempt to add board support to the sel4cp repo has so far not been successful. Here is the commit:

I copied the example files for the qemu_virt_arm which looked suitably generic so they didn’t need modification. I added the board to build_sdk with the correct loader address and KernelPlatform. Building the SDK goes fine. Then when I attempt to build the example I get this error:

Traceback (most recent call last):
  File "/usr/lib/python3.9/runpy.py", line 197, in _run_module_as_main
    return _run_code(code, main_globals, None,
  File "/usr/lib/python3.9/runpy.py", line 87, in _run_code
    exec(code, run_globals)
  File "/host/sel4cp/tool/sel4coreplat/__main__.py", line 2113, in <module>
    exit(main())
  File "/host/sel4cp/tool/sel4coreplat/__main__.py", line 2097, in main
    loader = Loader(
  File "/host/sel4cp/tool/sel4coreplat/loader.py", line 230, in __init__
    _check_non_overlapping(all_regions)
  File "/host/sel4cp/tool/sel4coreplat/loader.py", line 89, in _check_non_overlapping
    raise Exception(f"Overlapping regions: [0x{base:x}..0x{end:x}] overlaps [0x{b:x}..0x{e:x}]")
Exception: Overlapping regions: [0x10000000..0x1000a100] overlaps [0x10000000..0x10243000]

I think I modified the loader.c to have correct values for the rockpro64 but perhaps I missed something. Hints on what I still need to modify or where I have gone wrong are appreciated.

2

This comment in the code attempts to explain why the assert is needed and what is going on:

        # In addition to checking that provided regions (e.g initial task
        # and PD ELFs) do not overlap, we must make sure they do not overlap
        # with the loader itself, as that would (and has) lead to corruption of
        # the loader when copying regions to their respective locations.
        all_regions = list(self._regions)
        all_regions.append((loader_segment.virt_addr, self._image))
        _check_non_overlapping(all_regions)

The easiest fix is to change the loader_link_address to a higher memory address (e.g 0x20000000).

A long term fix would have a relocatable loader or different allocation strategy in seL4CP such that this assert is never expected to go off. This long term fix is something that will come later when the development changes become more mature and upstreamed to the mainline.

3

I am on Mattermost (@ivanv) should have any further direct questions!