Hi Kent, Thanks for the help! I think I have most of the additions required to get the RPi4 running, however I am falling over at what I hope is the last hurdle. I have the build going to the point that the elfloader tool attempts to map the image to a memory region, however I do not currently have this implemented in the overlay-rpi4.dts, so I get the following: FAILED: elfloader/gen_headers/image_start_addr.h cd /host/build/rpi4/elfloader && sh -c "/host/tools/seL4/elfloader-tool/../cmake-tool/helpers/shoehorn.py /host/build/rpi4/kernel/gen_headers/plat/machine/platform_gen.yaml /host/build/rpi4/elfloader/archive.o > /host/build/rpi4/elfloader/gen_headers//image_start_addr.h" shoehorn: fatal error: ELF-loader image "/host/build/rpi4/elfloader/archive.o" of size 0x2c29548 does not fit within any memory region described in "{'devices': [{'end': 4286844928, 'start': 0}, {'end': 4286857216, 'start': 4286853120}, {'end': 17592186040320, 'start': 4286861312}], 'memory': []}" I think that it makes sense for the base DTS not to know exactly what the RAM configuration is, as this is configurable on the PI, and so it needs to be told what the values actually are (at least this is my understanding). I have attempted to add a memory device to the overlay, but think I may be misunderstanding what information I need to implement here: / { chosen { seL4,elfloader-devices = "serial1"; seL4,kernel-devices = "serial1", &{/soc/gic400@40041000}, &{/timer}; }; memory@0 { /* This is configurable in the Pi's config.txt, but we use 128MiB of RAM by default. */ reg = <0x00 0x00000000 0x00 0x08000000>; }; }; To my knowledge, this should result in the build system being told that there is RAM located at Physical Memory Address 0x00... which is 0x08000000 (128MiB) bits in size. (The thought has dawned on me that this may not be large enough for the kernel + VM, however setting this to the full 1G or 512M just yields the same error...) This now results in an error in the init-build.sh script: Traceback (most recent call last): File "/host/kernel/tools/hardware_gen.py", line 94, in <module> main(args) File "/host/kernel/tools/hardware_gen.py", line 65, in main OUTPUTS[t].run(parsed_dt, hardware, cfg, args) File "/host/kernel/tools/hardware/outputs/c_header.py", line 176, in run physical_memory, reserved, physBase = memory.get_physical_memory(tree, config) File "/host/kernel/tools/hardware/utils/memory.py", line 95, in get_physical_memory regions = get_memory_regions(tree) File "/host/kernel/tools/hardware/utils/memory.py", line 30, in get_memory_regions tree.visit(visitor) File "/host/kernel/tools/hardware/fdt.py", line 113, in visit return self.wrapped_root.visit(visitor) File "/host/kernel/tools/hardware/device.py", line 148, in visit ret += child.visit(visitor) File "/host/kernel/tools/hardware/device.py", line 144, in visit ret = [visitor(self)] File "/host/kernel/tools/hardware/utils/memory.py", line 29, in visitor regions.update(node.get_regions()) File "/host/kernel/tools/hardware/device.py", line 113, in get_regions for r in Utils.intarray_iter(prop, sizes): File "/host/kernel/tools/hardware/device.py", line 229, in intarray_iter res.append(Utils.make_number(sizes[i], array)) File "/host/kernel/tools/hardware/device.py", line 221, in make_number ret |= array.pop(0) IndexError: pop from empty list After looking through the python scripts, this seems to result from the Utils.intarray_iter generator not generating any memory regions? I think... I have read all the documentation I can find on this, and just don't think I quite understand what's wrong here. If you have any insight (I hope I've provided enough information) into what I've got wrong here, I would be grateful! Thanks, Ben Turner ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________