Adding Platform Support: CAmkES-ARM-VM: VM_Minimal: Raspberry Pi 3b
Hi, I have been attempting to add support for the Raspberry Pi 3 b platform so that I can run the vm_minimal application on it. The platform supports ARM_HYP, so I believe it should be possible to get this working. I have reached to point where ninja errors on an implicit declaration for `set_gic_vcpu_ctrl_hcr`. From what I understand, this is to do with the ARM Generic Interrupt Controller, however the RPi3b doesn't have a GIC, it has a `bcm2836-armctrl-ic`. This occurs because the file vcpu.h defines an inline function that calls this function, however as the RPi3b doesn't have a GIC, neither the gic_v2.h or gic_v3.h files are provided in the build environment, and hence the build fails. I am unsure what this means in terms of implementation. What needs to be added or changed to get this compiling for the RPi3b? Thanks in advance 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. ________________________________________
Hi Ben, When configured as a hypervisor, seL4 uses the hardware interrupt virtualization support of GICv2 (GIC-400) and GICv3 (GIC-500). More work is needed for SoCs without such hardware support. BTW, it looks like Raspberry Pi4 (bcm2711) has a GIC-400 controller. Would you consider the new version? Regards, Yanyan On Thu, 2020-02-13 at 09:15 +0000, Turner, Ben wrote:
Hi,
I have been attempting to add support for the Raspberry Pi 3 b platform so that I can run the vm_minimal application on it. The platform supports ARM_HYP, so I believe it should be possible to get this working.
I have reached to point where ninja errors on an implicit declaration for `set_gic_vcpu_ctrl_hcr`. From what I understand, this is to do with the ARM Generic Interrupt Controller, however the RPi3b doesn't have a GIC, it has a `bcm2836-armctrl-ic`. This occurs because the file vcpu.h defines an inline function that calls this function, however as the RPi3b doesn't have a GIC, neither the gic_v2.h or gic_v3.h files are provided in the build environment, and hence the build fails.
I am unsure what this means in terms of implementation. What needs to be added or changed to get this compiling for the RPi3b?
Thanks in advance
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
Hi Yanyan,
Thanks for your reply.
That is a very good point! I think it may well be easier to add the other board support parts for the RPi4 to the build system, rather than figuring out what needs to be done for the RPi3 interrupt controller…
Thanks for the suggestion, I’ll be sure to let you know how I get on.
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.
________________________________________
From: Shen, Yanyan (Data61, Kensington NSW)
Hi,
I have been attempting to add support for the Raspberry Pi 3 b platform so that I can run the vm_minimal application on it. The platform supports ARM_HYP, so I believe it should be possible to get this working.
I have reached to point where ninja errors on an implicit declaration for `set_gic_vcpu_ctrl_hcr`. From what I understand, this is to do with the ARM Generic Interrupt Controller, however the RPi3b doesn't have a GIC, it has a `bcm2836-armctrl-ic`. This occurs because the file vcpu.h defines an inline function that calls this function, however as the RPi3b doesn't have a GIC, neither the gic_v2.h or gic_v3.h files are provided in the build environment, and hence the build fails.
I am unsure what this means in terms of implementation. What needs to be added or changed to get this compiling for the RPi3b?
Thanks in advance
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.ukhttp://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.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/develhttps://sel4.systems/lists/listinfo/devel
Hi,
I think I am most of the way through adding RPi4 support to the required projects, however I have stumbled upon an issue.
In the `kernel/src/plat/<plat>/config.cmake` files there is a `declare_default_headers` section. Where does the information for these values come from? I have searched the ARM CortexA72 TRM and looked for the BCM2711 specification document, but haven’t had much luck…
Where can I find out the correct values for the following question marks:
declare_default_headers(
TIMER_FREQUENCY ????????llu
MAX_IRQ ???
NUM_PPI 32 <
Hi,
I have been attempting to add support for the Raspberry Pi 3 b platform so that I can run the vm_minimal application on it. The platform supports ARM_HYP, so I believe it should be possible to get this working.
I have reached to point where ninja errors on an implicit declaration for `set_gic_vcpu_ctrl_hcr`. From what I understand, this is to do with the ARM Generic Interrupt Controller, however the RPi3b doesn't have a GIC, it has a `bcm2836-armctrl-ic`. This occurs because the file vcpu.h defines an inline function that calls this function, however as the RPi3b doesn't have a GIC, neither the gic_v2.h or gic_v3.h files are provided in the build environment, and hence the build fails.
I am unsure what this means in terms of implementation. What needs to be added or changed to get this compiling for the RPi3b?
Thanks in advance
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.ukhttp://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.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/develhttps://sel4.systems/lists/listinfo/devel
Hi Ben,
Glad to hear that!
I assume you can still boot Linux on the board? If so, searching the Linux boot log (dmesg) should help to find the TIMER_FREQUENCY and MAX_IRQ values.
Setting NUM_PPI to 32 is right.
The remaining parameters, KERNEL_WCET, CLK_MAGIC, and CLK_SHIFT, are related to the MCS config option. I copied Curtis and Kent who might help on these values.
Regards,
Yanyan
From: "Turner, Ben"
Hi,
I have been attempting to add support for the Raspberry Pi 3 b platform so that I can run the vm_minimal application on it. The platform supports ARM_HYP, so I believe it should be possible to get this working.
I have reached to point where ninja errors on an implicit declaration for `set_gic_vcpu_ctrl_hcr`. From what I understand, this is to do with the ARM Generic Interrupt Controller, however the RPi3b doesn't have a GIC, it has a `bcm2836-armctrl-ic`. This occurs because the file vcpu.h defines an inline function that calls this function, however as the RPi3b doesn't have a GIC, neither the gic_v2.h or gic_v3.h files are provided in the build environment, and hence the build fails.
I am unsure what this means in terms of implementation. What needs to be added or changed to get this compiling for the RPi3b?
Thanks in advance
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.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Hi Shen,
Thanks for the advice. I may have found the TIMER_FREQUENCY (although I’m not certain) – the boot log has an entry:
arch_timer: cp15 timer(s) running at 54.00MHz
This is the only possibly relevant timer reference I can find?
I haven’t had any luck with the MAX_IRQ value though. The only value in the boot log that could relate is:
NR_IRQS: 16, nr_irqs: 16, preallocated irqs: 16
But 16 seems way lower than I would expect… The value for the RPi3, for example, is 127!
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.
________________________________________
From: Shen, Yanyan (Data61, Kensington NSW)
Hi,
I have been attempting to add support for the Raspberry Pi 3 b platform so that I can run the vm_minimal application on it. The platform supports ARM_HYP, so I believe it should be possible to get this working.
I have reached to point where ninja errors on an implicit declaration for `set_gic_vcpu_ctrl_hcr`. From what I understand, this is to do with the ARM Generic Interrupt Controller, however the RPi3b doesn't have a GIC, it has a `bcm2836-armctrl-ic`. This occurs because the file vcpu.h defines an inline function that calls this function, however as the RPi3b doesn't have a GIC, neither the gic_v2.h or gic_v3.h files are provided in the build environment, and hence the build fails.
I am unsure what this means in terms of implementation. What needs to be added or changed to get this compiling for the RPi3b?
Thanks in advance
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.ukhttp://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.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/develhttps://sel4.systems/lists/listinfo/devel
Hi Ben,
You could also read the register CNTFRQ_EL0 [https://developer.arm.com/docs/ddi0595/b/aarch64-system-registers/cntfrq_el0] to double check the value.
As to the max IRQ, you can read it from the GICD_TYPER [https://developer.arm.com/docs/ihi0048/b/arm-generic-interrupt-controller-ar...]. The ITLinesNumber field indicates the maximum number of interrupts supported by the GIC.
Hope that will help.
Regards,
Yanyan
From: "Turner, Ben"
Hi Shen,
I have managed to confirm that the frequency is 54MHz and the MAX_IRQ is 127.
Still no luck finding much on KERNEL_WCET, CLK_MAGIC or CLK_SHIFT so far. I’ll keep digging but any other tips you can throw my way would be appreciated!
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.
________________________________________
From: Shen, Yanyan (Data61, Kensington NSW)
Hi Ben,
There is a tool in kernel/tools called reciprocal.py. It calculates CLK_MAGIC and CLK_SHIFT from an input frequency like so:
```
./reciprocal.py --divisor 54000000
magic number is: 5337599559, shift amount is 58
```
With an input frequency of 31250000 CLK_MAGIC=5337599559, CLK_SHIFT=58.
KERNEL_WCET is the worst case execution time of a path through the kernel in microseconds. Without an actual measurement, most platforms configure this to 10us.
________________________________
From: Turner, Ben
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. ________________________________________
participants (3)
-
Mcleod, Kent (Data61, Kensington NSW) -
Shen, Yanyan (Data61, Kensington NSW) -
Turner, Ben