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.
________________________________________
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
