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
_______________________________________________
Devel mailing list -- [email protected]
To unsubscribe send an email to [email protected]
