Kernel use of MPIDR_EL1 register on ARM
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/26f94df7e97a04f8ee49c1e94a0aa1203658... [4]: https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/arch-arm/s... [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.
On Mon, Sep 8, 2025 at 1:36 PM Julia Vassiliki via Devel <devel@sel4.systems> wrote:
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".
Which kernel APIs are you thinking of? The boot api does need to provide a logical id to each hw thread when calling into the kernel so that the right code path can be taken. This wouldn't be possible with using MPIDR values because the kernel may not be running on the lowest mpdir core or there may be multiple isolated kernel instances running. Reading MPIDR from user level could be supported with the addition of a cap for mediating the system register access.
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/26f94df7e97a04f8ee49c1e94a0aa1203658... [4]: https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/arch-arm/s... [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
Which kernel APIs are you thinking of? The boot api does need to provide a logical id to each hw thread when calling into the kernel so that the right code path can be taken. This wouldn't be possible with using MPIDR values because the kernel may not be running on the lowest mpdir core or there may be multiple isolated kernel instances running.
I'm mostly talking about the interface between the elfloader and the kernel here, with some additional notes regarding BootInfo->NodeID and SGI APIs (as well as PSCI as enabled by an SMC caps). And yes, obviously, the lowest MPIDR may not be the "boot core". What I'm asking is why is the loader responsible for making up these "logical core IDs" when they don't really simplify anything; and it adds complexity as every layer needs to know the value of the core ID -> MPIDR mapping. Even if this is needed (which the opposite direction is, internally, in parts at the very least for storing dense arrays in the scheduling queues - though perfect hash functions are almost certainly doable), it's not needed to expose this at every layer. What I'm trying to say, in all, is that I don't see the *point*. The only information that the loader needs to tell seL4 is which core is the "primary" (i.e. core 0); in the case of multikernel this becomes fuzzy anyhow; (is everyone really core 0?) --- What I'm asking, anyway, is if there was justification from the time, that anyone remembers. i.e. some reason I'm missing for why this was done in the loader as opposed to handles within the kernel, with the kernel reading this register. Whether or not the kernel pretends to userland that the cores are contiguously indexed is related, but not the same as why the kernel boot API was done this way. Julia ________________________________ From: Kent Mcleod <kent.mcleod72@gmail.com> Sent: Tuesday, September 9, 2025 10:18:42 AM To: Julia Vassiliki <julia.vassiliki@unsw.edu.au> Cc: devel@sel4.systems <devel@sel4.systems> Subject: Re: [seL4] Kernel use of MPIDR_EL1 register on ARM [You don't often get email from kent.mcleod72@gmail.com. Learn why this is important at https://aka.ms/LearnAboutSenderIdentification ] On Mon, Sep 8, 2025 at 1:36 PM Julia Vassiliki via Devel <devel@sel4.systems> wrote:
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".
Which kernel APIs are you thinking of? The boot api does need to provide a logical id to each hw thread when calling into the kernel so that the right code path can be taken. This wouldn't be possible with using MPIDR values because the kernel may not be running on the lowest mpdir core or there may be multiple isolated kernel instances running. Reading MPIDR from user level could be supported with the addition of a cap for mediating the system register access.
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/26f94df7e97a04f8ee49c1e94a0aa1203658... [4]: https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/arch-arm/s... [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
Hello Julia, For context, this only applies to the SMP version of seL4. On 2025-09-09 01:42, Julia Vassiliki via Devel wrote:
And yes, obviously, the lowest MPIDR may not be the "boot core". What I'm asking is why is the loader responsible for making up these "logical core IDs" when they don't really simplify anything; and it adds complexity as every layer needs to know the value of the core ID -> MPIDR mapping.
There is no need for the loader to assign logical core IDs, that's just how it's implemented currently. The Elfloader construction as it is adds more complexity than it solves for all kind of things, that's why I plan on making seL4 self-booting on Arm and RISC-V too.
Even if this is needed (which the opposite direction is, internally, in parts at the very least for storing dense arrays in the scheduling queues - though perfect hash functions are almost certainly doable), it's not needed to expose this at every layer.
For sane platforms, core ID == MPIDR. For some others, there can be a fixed transformation. Not sure all remaining cases can be solved with a perfect hash.
What I'm trying to say, in all, is that I don't see the *point*. The only information that the loader needs to tell seL4 is which core is the "primary" (i.e. core 0); in the case of multikernel this becomes fuzzy anyhow; (is everyone really core 0?)
There is no need for the loader to tell seL4 which core is the primary one either, again, that's just an implementation choice currently made. RISC-V especially made it unnecessarily complicated by trying to switch boot to the CONFIG_FIRST_HART_ID core in the loader instead of just continuing on the current one.
What I'm asking, anyway, is if there was justification from the time, that anyone remembers. i.e. some reason I'm missing for why this was done in the loader as opposed to handles within the kernel, with the kernel reading this register.
Because you can't infer the logical core ID from MPIDR, you need some policy decision. It's not much, but it's still there. RISC-V has the same problem with hart-IDs, where some platforms reserve hart ID 0 as a supervisor core and hart IDs may be non-sequential according to the RSIC-V standard (only hart ID 0 is always defined). Why a new platform would add this insanity is beyond me, but we have to deal with it.
Whether or not the kernel pretends to userland that the cores are contiguously indexed is related, but not the same as why the kernel boot API was done this way.
As you noted, logical core IDs are needed for efficiently looking up core-local data. For user space the API is also much friendlier, as the code can be more portable. As the kernel does everything by logical core ID, and MPIDR is only used for sending IPIs, it is not so strange that it ended up as it currently is. Whether Multikernel will use logical core IDs or not is an open question. It probably won't be needed. Greetings, Indan
participants (3)
-
Indan Zupancic -
Julia Vassiliki -
Kent Mcleod