Add SMP support for ARM/RISC-V #353
Open
+1,035
−150
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Contributor
Author
|
Ping @Indanz as you had comments on the previous iteration of this code in the smp branch. This has followed your pieces of advice. |
midnightveil
commented
Nov 11, 2025
| _start: | ||
|
|
||
| mrs x0, mpidr_el1 | ||
| and x0, x0,#0xFF // Check processor id |
Contributor
Author
There was a problem hiding this comment.
I'll add a quick note on why this was removed: this is wrong, as we are not guaranteed that the CPU we are booting on will have the Aff0 value of the MPIDR_EL1 to be 0. Nor do we expect that this part of the code should run on multiple cores. This dates back the initial public release of seL4CP.
midnightveil
force-pushed
the
julia/smp
branch
2 times, most recently
from
9d7020c to
9e6c71b
Compare
Indanz
reviewed
Nov 11, 2025
Ivan-Velickovic
changed the title
Ivan-Velickovic
force-pushed
the
julia/smp
branch
from
9e6c71b to
1653563
Compare
midnightveil
force-pushed
the
julia/smp
branch
from
1653563 to
6ebec68
Compare
Ivan-Velickovic
force-pushed
the
julia/smp
branch
from
0606a19 to
f004681
Compare
Comment on lines
106
to
103
| j spin_hart /* Spin any hart that isn't FIRST_HART_ID since we only support single-core right now. */ | ||
| li a7, SBI_HSM_BASE_EID | ||
| li a6, 0x1 | ||
| ecall |
Collaborator
There was a problem hiding this comment.
Need to clean this up and explain what's going on.
Collaborator
|
Once we finish the code changes we'll need to update a couple sections on the manual (e.g the list/description of Microkit configs and the QEMU sections on how to boot with multiple cores). We'll also need to adjust the porting platform support section for the SMP related changes. |
Ivan-Velickovic
force-pushed
the
julia/smp
branch
from
0f742e1 to
f3e8b6d
Compare
midnightveil
force-pushed
the
julia/smp
branch
from
0d686ad to
8b2ea2d
Compare
Signed-off-by: Julia Vassiliki <[email protected]>
this fixes real hardware Signed-off-by: Julia Vassiliki <[email protected]>
Signed-off-by: Julia Vassiliki <[email protected]>
Signed-off-by: Julia Vassiliki <[email protected]>
Signed-off-by: Julia Vassiliki <[email protected]>
Signed-off-by: Ivan Velickovic <[email protected]>
Signed-off-by: Ivan Velickovic <[email protected]>
Signed-off-by: Ivan Velickovic <[email protected]>
Signed-off-by: Ivan Velickovic <[email protected]>
Signed-off-by: Ivan Velickovic <[email protected]>
Signed-off-by: Ivan Velickovic <[email protected]>
Signed-off-by: Ivan Velickovic <[email protected]>
Signed-off-by: Ivan Velickovic <[email protected]>
Signed-off-by: Ivan Velickovic <[email protected]>
Signed-off-by: Julia Vassiliki <[email protected]>
This means that the board names are the same, but we build extra configurations of the boards with different kernel configurations for SMP support. This is cleaner, as we were finding that renaming the boards was broken a lot of our build systems code which needed to be duplicate for new boards. I'm not entirely convinced this is the best possible solution, but it is the nicest we can think of. Signed-off-by: Julia Vassiliki <[email protected]>
Signed-off-by: Julia Vassiliki <[email protected]>
Signed-off-by: Julia Vassiliki <[email protected]>
(instead of horribly violating it) Signed-off-by: Julia Vassiliki <[email protected]>
Signed-off-by: Julia Vassiliki <[email protected]>
Signed-off-by: Julia Vassiliki <[email protected]>
Signed-off-by: Julia Vassiliki <[email protected]>
Signed-off-by: Julia Vassiliki <[email protected]>
Signed-off-by: Julia Vassiliki <[email protected]>
To make it clearer what its purpose is. Signed-off-by: Julia Vassiliki <[email protected]>
Signed-off-by: Julia Vassiliki <[email protected]>
midnightveil
force-pushed
the
julia/smp
branch
from
8b2ea2d to
ff974cb
Compare
Contributor
Author
|
This is blocked on seL4/seL4#1563 |
Signed-off-by: Julia Vassiliki <[email protected]>
Signed-off-by: Julia Vassiliki <[email protected]>
Signed-off-by: Julia Vassiliki <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds support for SMP builds of the kernel on AArch64.
We have a
psci_target_cpus[]array, currently hardcoded, for the IDs of the cores to boot. This should match the values specified in the device tree /cpu@0/ node's<reg>field. Note that due to quirks of various platforms (e.g. OdroidC4), these do not (but can) match theMPIDRvalues that hardware reports, so we maintain a different table of their MPIDR values.There a few TODOs scattered throughout this code.