bootstrap: check and log allocation failures#107
Merged
Indanz merged 2 commits intoseL4:masterfrom Jan 27, 2026
Merged
Conversation
midnightveil
force-pushed
the
julia/bootstrap-errors
branch
from
7172291 to
5950bcb
Compare
Indanz
reviewed
Jan 15, 2026
midnightveil
force-pushed
the
julia/bootstrap-errors
branch
from
5950bcb to
106f12a
Compare
These functions are dependencies of the init_allocator() from libsel4benchsupport. If a thread is spawned with a set of UTs where either there is not enough to bootstrap the thread, or if they are all too small (e.g. < 12 bits when the default CNode size LibSel4UtilsCSpaceSizeBits defaults to 12 + 5), then the thread would proceed to fault on a data read on a region of virtual memory that didn't get allocated. Instead, return an error and log a reason (for the CNode case). Signed-off-by: Julia Vassiliki <[email protected]>
Signed-off-by: Julia Vassiliki <[email protected]>
midnightveil
force-pushed
the
julia/bootstrap-errors
branch
from
106f12a to
e95835f
Compare
Indanz
approved these changes
Jan 27, 2026
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
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.
These functions are dependencies of the init_allocator() from libsel4benchsupport. If a thread is spawned with a set of UTs where either there is not enough to bootstrap the thread, or if they are all too small (e.g. < 12 bits when the default CNode size LibSel4UtilsCSpaceSizeBits defaults to 12 + 5), then the thread would proceed to fault on a data read on a region of virtual memory that didn't get allocated.
Instead, return an error and log a reason (for the CNode case).