Endpoint Budget Threshold #2
Draft
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
Indanz
force-pushed
the
threshold
branch
2 times, most recently
from
dc812ca to
5ff7fae
Compare
There is no reason to check for pending interrupts after failed or preempted system calls. All it does is save a bit of time avoiding exiting and entering the kernel when preempting long-running kernel operations. The slowdown for such operations after this change is a factor of: (kernel exit + entry time) / WCET But making the code more complicated and slowing down all syscalls to speed up a corner case is not a good trade off. There is no reason for mcsPreemptionPoint to do basic timekeeping, normal kernel operation is sufficient if we don't try to bypass kernel exit/entry. Signed-off-by: Indan Zupancic <indan@nul.nu>
Otherwise all caller of endTimeslice will need to do it themselves. Signed-off-by: Indan Zupancic <indan@nul.nu>
Signed-off-by: Indan Zupancic <indan@nul.nu>
Indanz
force-pushed
the
threshold
branch
2 times, most recently
from
b0cf453 to
ff3a46d
Compare
Issues that make the implementation complicated: - We want the task to be restarted when ThreadState_Restart, but current code assumes that means something else. Commit 8ae457a is one possible work-around and something I think we want anyway. Another solution would be to clean up the threadstate code so that ThreadState_Restart will be honoured. Whatever is done, it will cause changes to the current code and add verification work. - There is no way to do endpoint invocations. Current work-around is to make it a reply invocation at the cost of one extra if-check in the reply handling slow path. An alternative is to make it a CNode operation like Yermin9 did, but that's even uglier of a solution, as it requires too much permissions. Now if a server can receive on the endpoint, it can also set the budget threshold, which makes sense considering the server has to be trusted to reply eventually. - The bitfield generator can't deal with fields spread over multiple words, forcing us to split the field into a high and a low one. Solution would be to fix the generator to support this, but I don't know how to do that for the generated proofs. Only 64-bit has this problem, but to reduce differences between 32 and 64-bits the code is the same. TODO: - Check details (exact behaviour on block, !canDonate etc.) - Write sel4test tests. Signed-off-by: Indan Zupancic <indan@nul.nu>
Owner
Author
|
Small correction for commit 8ae457a: The slowdown for such operations after this change is a factor of: (schedule + kernel exit + entry time) / WCET That is, the kernel also does a schedule call for each iteration, which currently is skipped. |
Indanz
commented
Dec 2, 2025
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Work in progress, cleaner implementation of the work done by @Yermin9. See
Issues that make the implementation complicated:
We want the task to be restarted when ThreadState_Restart, but
current code assumes that means something else. Commit 8ae457a
is one possible work-around and something I think we want anyway.
Another solution would be to clean up the threadstate code so that
ThreadState_Restart will be honoured. Whatever is done, it will
cause changes to the current code and add verification work.
There is no way to do endpoint invocations. Current work-around
is to make it a reply invocation at the cost of one extra if-check
in the reply handling slow path. An alternative is to make it a
CNode operation like Yermin9 did, but that's even uglier of a
solution, as it requires too much permissions. Now if a server
can receive on the endpoint, it can also set the budget threshold,
which makes sense considering the server has to be trusted to reply
eventually.
The bitfield generator can't deal with fields spread over multiple
words, forcing us to split the field into a high and a low one.
Solution would be to fix the generator to support this, but I
don't know how to do that for the generated proofs. Only 64-bit
has this problem, but to reduce differences between 32 and 64-bits
the code is the same.
TODO: