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