infer_cpu_gic_id now reads cpu id from GICD_TYPER register

[IkerGalardi]

Signed-off-by: IkerGalardi contacto.ikergalardi@gmail.com

Before, the current cpu gic id was guessed from target registers, but as it can be read in the documentation, the interrupt controller distributor has a register containing this information.

Inside the register GICD_TYPER (ic_type distributor struct) bits [5:7] represent the cpu id. This reimplementation of the function infer_cpu_gic_id simply reads that register and returns the information from there.

[lsf37]

It's Ok to ignore the Link test failure, they moved, and we'll fix them separately. @wom-bat would it make sense to set up a redirect on the website?

In any case, I'll start the larger regression test here:
@ssrg-bamboo test

And I'll also start a proof run for checking if the proofs still work (it looks like they should).

[ssrg-bamboo]

Hello, I'm a bot! I'll bring this PR into Trustworthy Systems and run some tests

[yyshen]

It looks like the code is trying to get the CPUNumber field from the ic_type, so it should be right shift by 5. It looks to me that the function is trying to infer the gic id, not the total number of implemented CPU interfaces.

[kent-mcleod]

Yea, the purpose of infer_cpu_gic_id is to handle the case where the CPU ID in the GIC-V2 context is not equal to the CPU ID that seL4 assigns to the node. An example where this is an issue is for the TX2 where the first A57 core has an seL4 ID of 0 but a GIC ID of 2 or 4 IIRC. Back when this function was written, the only way for a core to figure out what it's GIC target ID was was to read the read-only target value of some per-processor-interrupts. I'm not sure if this is still the only way, but I'm not aware of a better one yet.

It also seems that setIRQTarget doesn't correctly translate the Core ID to the GIC CPU target...

[yyshen]

On TX2, A57 quad-core cluster is the second cluster with cluster Id 1, and the dual-core Denver2 cluster is the first cluster with cluster id 0. However, the bootstrapping core is from the A57 cluster, and thus we have an non-zero GIC ID. We could read the mpidr_el1 to find out which cluster a core is in as well as the core id in the cluster. From there, I think we can infer the id for gic.

[kent-mcleod]

I researched this at the time, and it wasn't guaranteed that the GIC CPU ID could be estimated like that. At least the gicV3 uses the same ID I think.

[yyshen]

TX2 is an interesting mix, it uses aarch64 but with a gic-v2 controller. For giv-v2 controller, 8 cores are supported, and when sending the IPIs, the cluster ID and core ID need to be translated to 0-7 bits (one bit for each core) in the sgi_control. GIC-v3 supports more cores, so the cluster id and core ID are used when sending IPIs. So we could use the mpidr_el1 value (assuming is not changed by a hypervisor), as the target ID (for instance, the rk3399 GIC3 fix for two clusters). Well, that is a bit off the topic.

[kent-mcleod]

@IkerGalardi, thanks for proposing these changes. It appears that the GICD_TYPER (ic_type) field that you are referring to holds the number of CPU IDs that the implementation supports, and not the unique ID for each CPU. Do you have any more information about this?

[IkerGalardi]

I'm sorry I miss understood what that field meant. Apparently the GICv2 architecture specification doesn't give any direct way of querying the CPU ID, which is a bit sad.

Apart from the discussion, can I ask you how it was inferred with target registers? I don't really see where the target registers have any information about the processor accessing the registers.

Should I close the PR or should it be done by you?

[yyshen]

Hi @IkerGalardi I will close the PR. Thanks for the efforts.

[kent-mcleod]

Apart from the discussion, can I ask you how it was inferred with target registers? I don't really see where the target registers have any information about the processor accessing the registers.

@IkerGalardi, The early target registers (corresponding to IRQs 0-31) are expected to be read-only as they refer to interrupts that are per-processor and cannot be redirected to different processors as they essentially come from within the processor. Each processor reads a different value from the same memory address for those registers. So the first processor may read a target value of BIT(0) and the second processor may read a target value of BIT(1).