Added support for endpoint thresholds and budget limits by Yermin9 · Pull Request #6 · Yermin9/seL4

Yermin9 · 2023-04-03T10:07:57Z

No description provided.

Indanz · 2023-11-16T12:17:17Z

Please split the one commit into multiple ones: One for threshold, one for limit, and another one for the new system calls. That makes reviewing a lot easier. The current code needs some cleaning up.

For the threshold check the main costs seems to be updateTimestamp. But if that is done before taking the kernel lock anyway for other reasons, the extra overhead for this feature will be minimal. See discussion of seL4#844. But it depends on what time model MCS is going to use.

I think the fastpath shouldn't use the expensive available_budget_check() call, but only look at the current refill, same as round-robin does.

Yermin9 · 2024-01-26T00:22:46Z

My apologies for taking a while, but I've now split this up into separate commits for Thresholds, Budget Limits and the new System call.

Indanz · 2024-01-26T10:41:23Z

 void receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking, cap_t replyCPtr);
 void reorderEP(endpoint_t *epptr, tcb_t *thread);
+
+void setThreshold(endpoint_t * epptr, time_t threshold, bool_t budgetLimit);


budgetLimit should be part of the other commit.

Indanz · 2024-01-26T10:42:08Z

 void replyFromKernel_error(tcb_t *thread);
-void replyFromKernel_success_empty(tcb_t *thread);
-
+void replyFromKernel_success_empty(tcb_t *thread);


Please avoid unnecessary whitespace changes like these.

Indanz · 2024-01-26T10:45:32Z

            </error>
        </method>
+
+        <method id="EndpointSetThreshold" name="Endpoint_SetThreshold" manual_name="Endpoint Set Threshold" manual_label="cnode__endpoint_setThreshold">


This should be an endpoint operation, not a cnode operation, that just overly complicates the API for no reason.

Actually, the reason it is implemented as a CNode operation is probably because any invocation on an endpoint is treated as an IPC call, not a syscall.

With that limitation in mind, I think we should make it a reply object property and invocation instead.

Reply objects have the same problem as endpoints, all invocations are treated as replies to an IPC call.

With the current kernel syscall+method decoding mess, there is no clean way to add endpoint, reply or notification methods.

As you stated, I think I made it a Cnode operation because all endpoint operations are treated as IPC calls.

With the limitations on reply objects as well, what do you suggest?

Indanz · 2024-01-26T10:55:32Z

+        /* Perform addition, checking for overflow as we go */
+        if (unlikely(getMaxTicksToUs() - NODE_STATE(ksConsumed) < threshold)) {


This overflow should be impossible by design, ksConsumed > getMaxTicksToUs() should be impossible.

Indanz · 2024-01-26T11:06:25Z

+
+#ifdef CONFIG_KERNEL_MCS
+void setThreshold(endpoint_t * epptr, time_t threshold, bool_t budgetLimit) {
+    /* Add the kernel WCET to the passed threshold value, unless we were passed 0*/


The comment is in the wrong place, but why add WCET? A fastpath invocation should take nowhere near WCET time.

I'd assure that the threshold is at least WCET instead. Users need to measure the call time to tweak this setting anyway, don't make it harder by changing the value randomly.

Indanz · 2024-01-26T11:11:25Z

+                commitTime();
+
+                /* Yield and wait for sufficient budget */
+                if(!merge_until_budget(NODE_STATE(ksCurThread)->tcbSchedContext,endpoint_ptr_get_epThreshold(ep_ptr) + 2u * getKernelWcetTicks())) {


Don't add WCET everywhere please. The threshold value should be twice WCET already.

Please write a test for sel4test that checks that the budget works as expected and use that to test your implementation. E.g. configure a task with a certain budget/period and check if IPC calls fail and succeed when they should.

Indanz · 2024-01-26T11:44:39Z

+    /* The EXCEPTION_NONE_THRESHOLD_RESTART check is necessary,
+     * because for IPC threshold behaviour, we actually do want to set ThreadState_Restart
+     */
    if (unlikely(
-            thread_state_get_tsType(thread->tcbState) == ThreadState_Restart)) {
+            thread_state_get_tsType(thread->tcbState) == ThreadState_Restart
+                && status != EXCEPTION_NONE_THRESHOLD_RESTART
+            )) {


The original code was already obtuse, but with this change it gets even harder to understand what's happening.

It would make more sense if the code that sets the task to ThreadState_Restart would set it to ThreadState_Running instead if that's what's wanted (and also call replyFromKernel_success_empty()). Then this code can be removed altogether.

Indanz · 2024-01-26T11:51:08Z

My apologies for taking a while, but I've now split this up into separate commits for Thresholds, Budget Limits and the new System call.

No problem and thanks.

I recommend focussing on the threshold feature first and leaving the others for now, or have them in a separate PR to ease review. At least I'm ignoring the limit and new syscall features, because I don't agree with them.

Yermin9 · 2025-07-29T10:13:55Z

I should have the time now to follow this through.
I've started by rebasing onto master, discarded the budgetLimit commits and removed any stray budgetLimit references.

Indanz · 2025-07-29T10:36:14Z

I should have the time now to follow this through. I've started by rebasing onto master, discarded the budgetLimit commits and removed any stray budgetLimit references.

I'm working on a simplified version at the moment, so don't spend too much time on it. Should have something up this week. Trying to keep the good bits of your commits though and would greatly appreciate your feedback. There's probably a reason for everything you did, which I don't know, so I might be oversimplifying things too much.

As you stated, I think I made it a Cnode operation because all endpoint operations are treated as IPC calls.
With the limitations on reply objects as well, what do you suggest?

If people didn't spend decades verifying the current code, I'd suggest to cleanup the syscall/invocation decoding code to something less messy and horrible. Then there would be no assumptions on which objects which syscalls are done, and adding a new invocation would be easy without slowing down everything else.

As it is, I think I prefer either an endpoint or Reply invocation that requires both an endpoint and Reply cap. Then we can use the permissions on the reply cap to limit this call, as you would need something like read permission for the endpoint and write for the reply. Wherever I put it, it will slow down everything, but hopefully it can be limited to one extra if-check in a slow path somewhere.

The other gnarl is how to bypass handleInvocation's trailing code messing things up.

Indanz · 2025-07-30T15:33:53Z

WIP can be found at: Indanz#2

Early version, haven't compiled it yet. I went for making it a reply invocation as I can do a quick check on the call argument, limiting the damage. This check can be avoided altogether for the fastpath, as the fastpath only handles endpoint calls and ReplyRecv syscalls.

I fixed some other problems by improving the mainline kernel, not sure if that's being too optimistic.

Yermin9 force-pushed the threshold_rfc branch from f9f34c0 to 2e604cd Compare January 26, 2024 00:22

Indanz reviewed Jan 26, 2024

View reviewed changes

Mitchell Johnston added 2 commits July 29, 2025 20:08

Implemented Threshold support

103e08a

fixup: Remove stray budgetLimit references

c2567f5

Yermin9 force-pushed the threshold_rfc branch from 2e604cd to c2567f5 Compare July 29, 2025 10:10

Indanz mentioned this pull request Jul 30, 2025

Endpoint Budget Threshold Indanz/seL4#2

Draft

		/* Perform addition, checking for overflow as we go */
		if (unlikely(getMaxTicksToUs() - NODE_STATE(ksConsumed) < threshold)) {

Conversation

Yermin9 commented Apr 3, 2023

Uh oh!

Indanz commented Nov 16, 2023

Uh oh!

Yermin9 commented Jan 26, 2024

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Indanz Jul 28, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Indanz commented Jan 26, 2024

Uh oh!

Yermin9 commented Jul 29, 2025

Uh oh!

Indanz commented Jul 29, 2025

Uh oh!

Indanz commented Jul 30, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Indanz Jul 28, 2025 •

edited

Loading