For ARM platforms, the hardware provides access to the MPIDR ("Multiprocessor 
Identification Register") [1],
which, amongst other things, provides access to 2 (or 3, for AArch64) affinity 
levels: Aff0, Aff1, Aff2, and possibly
Aff3. However, seL4 instead seems to gather the CPU index from a loader-set 
`tpidr_el1`.

    /* tpidr_el1 has the logic ID of the core, starting from 0 */
    mrs     x6, tpidr_el1
    /* Set the sp for each core assuming linear indices */
    ldr     x5, =BIT(CONFIG_KERNEL_STACK_BITS)
    mul     x5, x5, x6

This is then overwritten later. with the kernel stack address. Is there any 
reasoning for why it was done this way?

The elfloader [3] then has read the MPIDR and converted it to TPIDR_EL1 for the 
kernel, and
it uses a generated table to map the MPIDR IDs to "logical core IDs" [4]. Here 
is the boot log for the TX2,
which does use non-contiguous Aff0 IDs.

    Boot cpu id = 0x100, index=2
    Core 257 is up with logic id 1
    Core 258 is up with logic id 2
    Core 259 is up with logic id 3
    Enabling MMU and paging

Of note here is 2 things:

1. That the ARM PSCI specification [5], for "target_cpu" when calling PSCI_ON 
or OFF methods
   (such as done in the elfloader) expects a MPIDR-like ID (I say "like" 
because it is with the "U"
    and "MT" bits masked out). In its current state, the seL4_BootInfo provided 
ID is instead the
    logical ID, which means that there's no way to see the value of MPIDR from 
userspace.

2. The GICv3 uses MPIDR affinity values when sending IPIs, and so the kernel 
does actually
    maintain a "mpidr_map" which wouldn't be necessary if everything talked in 
terms of
    MPIDRs. (It would still be required for other reasons on SMP as opposed to 
multikernel,
    though).

        BOOT_CODE void cpu_initLocalIRQController(void)
        {
            word_t mpidr = 0;
            SYSTEM_READ_WORD(MPIDR, mpidr);

            mpidr_map[CURRENT_CPU_INDEX()] = mpidr;
            active_irq[CURRENT_CPU_INDEX()] = IRQ_NONE;

            gicr_init();
            cpu_iface_init();
        }


In the spirit of being a minimal hardware abstraction, I feel that it makes 
more sense for the kernel's APIs
to be in terms of MPIDRs [6], but that it would probably be a breaking change. 
Internally, aside from this,
it makes *more* sense for the kernel to think in terms of MPIDRs for the core 
values, rather than a "logical core ID".

Some context for how this is represented in the device trees:
In the device tree documentation 
'Documentation/devicetree/bindings/arm/cpus.yaml' [2] the `<reg>`
field of the cpus node tells the values of each of the CPU nodes; mapping the 
affinities (possibly non-contiguous)
to a contiguous CPU index could be done with a build-time lookup table. For 
example,
here is the first part of the OdroidC4 device tree, which tells us that node 0 
is Aff0=0, Aff1=0.

        cpus {
                #address-cells = <0x02>;
                #size-cells = <0x00>;
                cpu@0 {
                        device_type = "cpu";
                        reg = <0x00 0x00>;
                };
                /* etc */
        }

[1]: https://arm.jonpalmisc.com/latest_sysreg/AArch64-mpidr_el1
[2] https://www.kernel.org/doc/Documentation/devicetree/bindings/arm/cpus.yaml
[3]: 
https://github.com/seL4/seL4_tools/blob/26f94df7e97a04f8ee49c1e94a0aa12036581f71/elfloader-tool/src/arch-arm/64/cpuid.c#L13-L18
[4]: 
https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/arch-arm/smp_boot.c#L71-L129
[5]: https://documentation-service.arm.com/static/6703a8b8d7e4b739d817e10d
[6]: So, the SMP affinity APIs, and BootInfo->nodeID field.

Julia

This email and any files transmitted with it may contain confidential 
information. If you believe you have received this email or any of its contents 
in error, please notify me immediately by return email and destroy this email. 
Do not use, disseminate, forward, print or copy any contents of an email 
received in error.

_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

Reply via email to