mcs: Add sporadic flag to SchedControl_Configure

This adds a flags parameter to SchedControl_Configure to enable
configuration of a sporadic SC.

This also allows flags to be added in the future as needed without
breaking the API.

This allows the user to configure an SC either to be constrained as a
sporadic task where accumulated time is only delayed to when a task has
become runnable (implementing the sporadic server algorithm) or
whenever the task becomes the current executing task (implementing the
sliding-window constraint as in constant-bandwidth servers).

This can be used to prevent non-realtime tasks from exceeding bandwidth
under any circumstances, even in an over-committed configuration, whilst
also allowing work-conserving tasks to be configured in the same system.

To implement sporadic servers, we need to ensure that the suspension of
a task cannot be used as a mechanism to amplify budget of a task by
granting that task access to effectively multiple periods worth of
replenishments within a single period.

To align the implementation of SCs with the model of sporadic servers we
must delay available time until the release of a task. Within seL4, a
release would be any time where an SC changes from not being associated
with a Running, RunningVM, or Restart thread to one that is.

This can occur when an SC is bound to a new thread in such a state or
when a thread changes to such a state from any non-running states.

Critically, replenishments should not be delayed at the point when an SC
becomes the current SC (as was the case prior to this commit). This has
the effect of enforcing a continuous, constant bandwidth which is a
restriction that is incompatible with standard scheduling logic.

Accounting for this requires inserting a new refill_unblock_check
call whenever a sporadic SC is unblocked and removing the
refill_unblock_check call from when said SC is scheduled.

Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

CHANGES

@@ -22,10 +22,15 @@ description indicates whether it is SOURCE-COMPATIBLE, BINARY-COMPATIBLE, or BRE
 Further information about [seL4 releases](https://docs.sel4.systems/sel4_release/) is available.
 
 ---
-Upcoming release: BINARY COMPATIBLE
+Upcoming release: BREAKING
 
 ## Changes
 
+* Scheduling contexts can be configured as constant-bandwidth or sporadic server
+  - Constant bandwidth observes a continuous constant bandwidth of budget/period
+  - Sporadic server behaves as described by Sprunt et. al.
+  - In an overcommitted system, sporadic preserves accumulated time
+
 
 ## Upgrade Notes
 ---

include/kernel/sporadic.h

@@ -144,6 +144,25 @@ static inline bool_t sc_released(sched_context_t *sc)
     }
 }
 
+/*
+ * Return true if a SC's available refills should be delayed at the
+ * point the associated thread becomes runnable (sporadic server).
+ */
+static inline bool_t sc_sporadic(sched_context_t *sc)
+{
+    return sc != NULL && sc->scSporadic;
+}
+
+/*
+ * Return true if a SC's available refills should be delayed at the
+ * point the associated thread becomes the current thread (constant
+ * bandwidth).
+ */
+static inline bool_t sc_constant_bandwidth(sched_context_t *sc)
+{
+    return !sc->scSporadic;
+}
+
 /* Create a new refill in a non-active sc */
 #ifdef ENABLE_SMP_SUPPORT
 void refill_new(sched_context_t *sc, word_t max_refills, ticks_t budget, ticks_t period, word_t core);

include/object/structures.h

@@ -373,6 +373,10 @@ struct sched_context {
     word_t scRefillHead;
     /* Index of the tail of the refill circular buffer */
     word_t scRefillTail;
+
+    /* Whether to apply constant-bandwidth/sliding-window constraint
+     * rather than only sporadic server constraints */
+    bool_t scSporadic;
 };
 
 struct reply {

libsel4/include/interfaces/sel4.xml

@@ -644,7 +644,7 @@
 
     <interface name="seL4_SchedControl">
 
-        <method id="SchedControlConfigure" name="Configure" manual_name="Configure" manual_label="schedcontrol_configure" condition="defined(CONFIG_KERNEL_MCS)">
+        <method id="SchedControlConfigureFlags" name="ConfigureFlags" manual_name="ConfigureFlags" manual_label="schedcontrol_configureflags" condition="defined(CONFIG_KERNEL_MCS)">
             <brief>
                 Set the parameters of a scheduling context by invoking the scheduling control capability. If the scheduling context is bound to a currently running thread, the parameters will take effect immediately: that is the current budget will be increased or reduced by the difference between the new and previous budget and the replenishment time will be updated according to any difference in the period. This can result in active threads being post-poned or released depending on the nature of the parameter change and the state of the thread. Additionally, if the scheduling context was previously empty (no budget) but bound to a runnable thread, this can result in a thread running for the first time since it now has access to CPU time. This call will return seL4 Invalid Argument if the parameters are too small (smaller than the kernel WCET for this platform) or too large (will overflow the timer).
             </brief>
@@ -662,6 +662,8 @@
                 description="Number of extra sporadic replenishments this scheduling context should use. Ignored for round-robin threads."/>
             <param dir="in" name="badge" type="seL4_Word"
                 description="Identifier for this scheduling context. Delivered to timeout exception handler. Can be used to determine which scheduling context triggered the timeout." />
+            <param dir="in" name="flags" type="seL4_Word"
+                description="Bitwise OR'd set of seL4_SchedContextFlag." />
         </method>
 
     </interface>

libsel4/include/sel4/constants.h

@@ -93,6 +93,14 @@ static inline seL4_Word seL4_MaxExtraRefills(seL4_Word size)
     return (LIBSEL4_BIT(size) -  seL4_CoreSchedContextBytes) / seL4_RefillSizeBytes;
 }
 #endif /* !__ASSEMBLER__ */
+
+/* Flags to be used with seL4_SchedControl_ConfigureFlags */
+typedef enum {
+    seL4_SchedContext_NoFlag = 0x0,
+    seL4_SchedContext_Sporadic = 0x1,
+    SEL4_FORCE_LONG_ENUM(seL4_SchedContextFlag),
+} seL4_SchedContextFlag;
+
 #endif /* CONFIG_KERNEL_MCS */
 
 #ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC

libsel4/include/sel4/sel4.h

@@ -14,6 +14,7 @@
 
 #include <sel4/invocation.h>
 #include <interfaces/sel4_client.h>
+#include <sel4/virtual_client.h>
 
 #include <sel4/bootinfo.h>
 #include <sel4/faults.h>

libsel4/include/sel4/virtual_client.h

@@ -0,0 +1,27 @@
+/*
+ * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#pragma once
+#include <autoconf.h>
+#include <sel4/types.h>
+#include <sel4/macros.h>
+#include <sel4/invocation.h>
+#include <sel4/constants.h>
+#include <interfaces/sel4_client.h>
+
+/*
+ * This file specifies virtual implementations of older invocations
+ * that can be aliased directly to new invocations.
+ */
+
+#ifdef CONFIG_KERNEL_MCS
+LIBSEL4_INLINE seL4_Error seL4_SchedControl_Configure(seL4_SchedControl _service, seL4_SchedContext schedcontext,
+                                                      seL4_Time budget, seL4_Time period, seL4_Word extra_refills, seL4_Word badge)
+{
+    return seL4_SchedControl_ConfigureFlags(_service, schedcontext, budget, period, extra_refills, badge,
+                                            seL4_SchedContext_NoFlag);
+}
+#endif

manual/parts/threads.tex

@@ -200,8 +200,15 @@ invoke the appropriate \obj{SchedControl} capability, which provides access to C
 on a single node.  A scheduling control cap for each node is provided to the initial task at run
 time.  Threads run on the node that their scheduling context is configured for.  Scheduling context
 parameters can then be set and updated using
-\apifunc{seL4\_SchedControl\_Configure}{schedcontrol_configure}, which allows the budget and period
-to be specified.
+\apifunc{seL4\_SchedControl\_ConfigureFlags}{schedcontrol_configureflags}, which allows the budget and period
+to be specified along with a bitwise OR'd set of the following flags.
+
+\begin{description}
+
+\item[seL4\_SchedContext\_Sporadic]: constrain the execution time only according to the
+sporadic server algorithm rather than to a continuous constant bandwidth.
+
+\end{description}
 
 The kernel does not conduct any schedulability tests, as task admission is left to user-level policy
 and can be conducted online or offline, statically or dynamically or not at all.

src/kernel/thread.c

@@ -91,6 +91,10 @@ void restart(tcb_t *target)
         cancelIPC(target);
 #ifdef CONFIG_KERNEL_MCS
         setThreadState(target, ThreadState_Restart);
+        if (sc_sporadic(target->tcbSchedContext) && sc_active(target->tcbSchedContext)
+            && target->tcbSchedContext != NODE_STATE(ksCurSC)) {
+            refill_unblock_check(target->tcbSchedContext);
+        }
         schedContext_resume(target->tcbSchedContext);
         if (isSchedulable(target)) {
             possibleSwitchTo(target);
@@ -137,6 +141,11 @@ void doReplyTransfer(tcb_t *sender, tcb_t *receiver, cte_t *slot, bool_t grant)
     reply_remove(reply, receiver);
     assert(thread_state_get_replyObject(receiver->tcbState) == REPLY_REF(0));
     assert(reply->replyTCB == NULL);
+
+    if (sc_sporadic(receiver->tcbSchedContext) && sc_active(receiver->tcbSchedContext)
+        && receiver->tcbSchedContext != NODE_STATE_ON_CORE(ksCurSC, receiver->tcbSchedContext->scCore)) {
+        refill_unblock_check(receiver->tcbSchedContext);
+    }
 #else
     assert(thread_state_get_tsType(receiver->tcbState) ==
            ThreadState_BlockedOnReply);
@@ -313,7 +322,9 @@ static void switchSchedContext(void)
 {
     if (unlikely(NODE_STATE(ksCurSC) != NODE_STATE(ksCurThread)->tcbSchedContext) && NODE_STATE(ksCurSC)->scRefillMax) {
         NODE_STATE(ksReprogram) = true;
-        refill_unblock_check(NODE_STATE(ksCurThread->tcbSchedContext));
+        if (sc_constant_bandwidth(NODE_STATE(ksCurThread)->tcbSchedContext)) {
+            refill_unblock_check(NODE_STATE(ksCurThread)->tcbSchedContext);
+        }
 
         assert(refill_ready(NODE_STATE(ksCurThread->tcbSchedContext)));
         assert(refill_sufficient(NODE_STATE(ksCurThread->tcbSchedContext), 0));

src/object/endpoint.c

@@ -103,6 +103,9 @@ void sendIPC(bool_t blocking, bool_t do_call, word_t badge,
         assert(dest->tcbSchedContext == NULL || refill_sufficient(dest->tcbSchedContext, 0));
         assert(dest->tcbSchedContext == NULL || refill_ready(dest->tcbSchedContext));
         setThreadState(dest, ThreadState_Running);
+        if (sc_sporadic(dest->tcbSchedContext) && dest->tcbSchedContext != NODE_STATE(ksCurSC)) {
+            refill_unblock_check(dest->tcbSchedContext);
+        }
         possibleSwitchTo(dest);
 #else
         bool_t replyCanGrant = thread_state_ptr_get_blockingIPCCanGrant(&dest->tcbState);;
@@ -233,6 +236,11 @@ void receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking)
             do_call = thread_state_ptr_get_blockingIPCIsCall(&sender->tcbState);
 
 #ifdef CONFIG_KERNEL_MCS
+            if (sc_sporadic(sender->tcbSchedContext)) {
+                assert(sender->tcbSchedContext != NODE_STATE(ksCurSC));
+                refill_unblock_check(sender->tcbSchedContext);
+            }
+
             if (do_call ||
                 seL4_Fault_get_seL4_FaultType(sender->tcbFault) != seL4_Fault_NullFault) {
                 if ((canGrant || canGrantReply) && replyPtr != NULL) {
@@ -385,6 +393,10 @@ void cancelAllIPC(endpoint_t *epptr)
             }
             if (seL4_Fault_get_seL4_FaultType(thread->tcbFault) == seL4_Fault_NullFault) {
                 setThreadState(thread, ThreadState_Restart);
+                if (sc_sporadic(thread->tcbSchedContext)) {
+                    assert(thread->tcbSchedContext != NODE_STATE(ksCurSC));
+                    refill_unblock_check(thread->tcbSchedContext);
+                }
                 possibleSwitchTo(thread);
             } else {
                 setThreadState(thread, ThreadState_Inactive);
@@ -430,6 +442,10 @@ void cancelBadgedSends(endpoint_t *epptr, word_t badge)
                 if (seL4_Fault_get_seL4_FaultType(thread->tcbFault) ==
                     seL4_Fault_NullFault) {
                     setThreadState(thread, ThreadState_Restart);
+                    if (sc_sporadic(thread->tcbSchedContext)) {
+                        assert(thread->tcbSchedContext != NODE_STATE(ksCurSC));
+                        refill_unblock_check(thread->tcbSchedContext);
+                    }
                     possibleSwitchTo(thread);
                 } else {
                     setThreadState(thread, ThreadState_Inactive);

src/object/notification.c

@@ -80,6 +80,12 @@ void sendSignal(notification_t *ntfnPtr, word_t badge)
                 MCS_DO_IF_SC(tcb, ntfnPtr, {
                     possibleSwitchTo(tcb);
                 })
+#ifdef CONFIG_KERNEL_MCS
+                if (sc_sporadic(tcb->tcbSchedContext) && sc_active(tcb->tcbSchedContext)) {
+                    assert(tcb->tcbSchedContext != NODE_STATE(ksCurSC));
+                    refill_unblock_check(tcb->tcbSchedContext);
+                }
+#endif
 #ifdef CONFIG_VTX
             } else if (thread_state_ptr_get_tsType(&tcb->tcbState) == ThreadState_RunningVM) {
 #ifdef ENABLE_SMP_SUPPORT
@@ -95,6 +101,16 @@ void sendSignal(notification_t *ntfnPtr, word_t badge)
                     MCS_DO_IF_SC(tcb, ntfnPtr, {
                         possibleSwitchTo(tcb);
                     })
+#ifdef CONFIG_KERNEL_MCS
+                    if (tcb->tcbSchedContext != NULL && sc_active(tcb->tcbSchedContext)) {
+                        sched_context_t *sc = SC_PTR(notification_ptr_get_ntfnSchedContext(ntfnPtr));
+                        if (tcb->tcbSchedContext == sc && sc_sporadic(sc)) {
+                            /* Only unblock if the SC was donated from the
+                             * notification */
+                            refill_unblock_check(tcb->tcbSchedContext);
+                        }
+                    }
+#endif
                 }
 #endif /* CONFIG_VTX */
             } else {
@@ -136,6 +152,13 @@ void sendSignal(notification_t *ntfnPtr, word_t badge)
         MCS_DO_IF_SC(dest, ntfnPtr, {
             possibleSwitchTo(dest);
         })
+
+#ifdef CONFIG_KERNEL_MCS
+        if (sc_sporadic(dest->tcbSchedContext) && sc_active(dest->tcbSchedContext)) {
+            assert(dest->tcbSchedContext != NODE_STATE(ksCurSC));
+            refill_unblock_check(dest->tcbSchedContext);
+        }
+#endif
         break;
     }
 
@@ -193,6 +216,11 @@ void receiveSignal(tcb_t *thread, cap_t cap, bool_t isBlocking)
         notification_ptr_set_state(ntfnPtr, NtfnState_Idle);
 #ifdef CONFIG_KERNEL_MCS
         maybeDonateSchedContext(thread, ntfnPtr);
+        // If the SC has been donated to the current thread (in a reply_recv, send_recv scenario) then
+        // we may need to perform refill_unblock_check if the SC is becoming activated.
+        if (thread->tcbSchedContext != NODE_STATE(ksCurSC) &&  sc_sporadic(thread->tcbSchedContext) ) {
+            refill_unblock_check(thread->tcbSchedContext);
+        }
 #endif
         break;
     }
@@ -211,6 +239,10 @@ void cancelAllSignals(notification_t *ntfnPtr)
         for (; thread; thread = thread->tcbEPNext) {
             setThreadState(thread, ThreadState_Restart);
 #ifdef CONFIG_KERNEL_MCS
+            if (sc_sporadic(thread->tcbSchedContext)) {
+                assert(thread->tcbSchedContext != NODE_STATE(ksCurSC));
+                refill_unblock_check(thread->tcbSchedContext);
+            }
             possibleSwitchTo(thread);
 #else
             SCHED_ENQUEUE(thread);
@@ -251,6 +283,14 @@ void completeSignal(notification_t *ntfnPtr, tcb_t *tcb)
         notification_ptr_set_state(ntfnPtr, NtfnState_Idle);
 #ifdef CONFIG_KERNEL_MCS
         maybeDonateSchedContext(tcb, ntfnPtr);
+        if (sc_sporadic(tcb->tcbSchedContext) && sc_active(tcb->tcbSchedContext)) {
+            sched_context_t *sc = SC_PTR(notification_ptr_get_ntfnSchedContext(ntfnPtr));
+            if (tcb->tcbSchedContext == sc) {
+                /* Only unblock if the SC was donated from the
+                 * notification */
+                refill_unblock_check(tcb->tcbSchedContext);
+            }
+        }
 #endif
     } else {
         fail("tried to complete signal with inactive notification object");

src/object/schedcontext.c

@@ -286,6 +286,9 @@ void schedContext_bindTCB(sched_context_t *sc, tcb_t *tcb)
 
     SMP_COND_STATEMENT(migrateTCB(tcb, sc->scCore));
 
+    if (sc_sporadic(sc) && sc_active(sc)) {
+        refill_unblock_check(sc);
+    }
     schedContext_resume(sc);
     if (isSchedulable(tcb)) {
         SCHED_ENQUEUE(tcb);

src/object/schedcontrol.c

@@ -10,8 +10,8 @@
 #include <object/schedcontrol.h>
 #include <kernel/sporadic.h>
 
-static exception_t invokeSchedControl_Configure(sched_context_t *target, word_t core, ticks_t budget,
-                                                ticks_t period, word_t max_refills, word_t badge)
+static exception_t invokeSchedControl_ConfigureFlags(sched_context_t *target, word_t core, ticks_t budget,
+                                                     ticks_t period, word_t max_refills, word_t badge, word_t flags)
 {
 
     target->scBadge = badge;
@@ -42,6 +42,8 @@ static exception_t invokeSchedControl_Configure(sched_context_t *target, word_t
         }
     }
 
+    target->scSporadic = (flags & seL4_SchedContext_Sporadic) != 0;
+
     if (budget == period) {
         /* this is a cool hack: for round robin, we set the
          * period to 0, which means that the budget will always be ready to be refilled
@@ -84,16 +86,16 @@ static exception_t invokeSchedControl_Configure(sched_context_t *target, word_t
     return EXCEPTION_NONE;
 }
 
-static exception_t decodeSchedControl_Configure(word_t length, cap_t cap, word_t *buffer)
+static exception_t decodeSchedControl_ConfigureFlags(word_t length, cap_t cap, word_t *buffer)
 {
     if (current_extra_caps.excaprefs[0] == NULL) {
-        userError("SchedControl_Configure: Truncated message.");
+        userError("SchedControl_ConfigureFlags: Truncated message.");
         current_syscall_error.type = seL4_TruncatedMessage;
         return EXCEPTION_SYSCALL_ERROR;
     }
 
     if (length < (TIME_ARG_SIZE * 2) + 2) {
-        userError("SchedControl_configure: truncated message.");
+        userError("SchedControl_configureFlags: truncated message.");
         current_syscall_error.type = seL4_TruncatedMessage;
         return EXCEPTION_SYSCALL_ERROR;
     }
@@ -104,17 +106,18 @@ static exception_t decodeSchedControl_Configure(word_t length, cap_t cap, word_t
     ticks_t period_ticks = usToTicks(period_us);
     word_t extra_refills = getSyscallArg(TIME_ARG_SIZE * 2, buffer);
     word_t badge = getSyscallArg(TIME_ARG_SIZE * 2 + 1, buffer);
+    word_t flags = getSyscallArg(TIME_ARG_SIZE * 2 + 2, buffer);
 
     cap_t targetCap = current_extra_caps.excaprefs[0]->cap;
     if (unlikely(cap_get_capType(targetCap) != cap_sched_context_cap)) {
-        userError("SchedControl_Configure: target cap not a scheduling context cap");
+        userError("SchedControl_ConfigureFlags: target cap not a scheduling context cap");
         current_syscall_error.type = seL4_InvalidCapability;
         current_syscall_error.invalidCapNumber = 1;
         return EXCEPTION_SYSCALL_ERROR;
     }
 
     if (budget_us > MAX_BUDGET_US || budget_ticks < MIN_BUDGET) {
-        userError("SchedControl_Configure: budget out of range.");
+        userError("SchedControl_ConfigureFlags: budget out of range.");
         current_syscall_error.type = seL4_RangeError;
         current_syscall_error.rangeErrorMin = MIN_BUDGET_US;
         current_syscall_error.rangeErrorMax = MAX_BUDGET_US;
@@ -122,7 +125,7 @@ static exception_t decodeSchedControl_Configure(word_t length, cap_t cap, word_t
     }
 
     if (period_us > MAX_BUDGET_US || period_ticks < MIN_BUDGET) {
-        userError("SchedControl_Configure: period out of range.");
+        userError("SchedControl_ConfigureFlags: period out of range.");
         current_syscall_error.type = seL4_RangeError;
         current_syscall_error.rangeErrorMin = MIN_BUDGET_US;
         current_syscall_error.rangeErrorMax = MAX_BUDGET_US;
@@ -130,7 +133,7 @@ static exception_t decodeSchedControl_Configure(word_t length, cap_t cap, word_t
     }
 
     if (budget_ticks > period_ticks) {
-        userError("SchedControl_Configure: budget must be <= period");
+        userError("SchedControl_ConfigureFlags: budget must be <= period");
         current_syscall_error.type = seL4_RangeError;
         current_syscall_error.rangeErrorMin = MIN_BUDGET_US;
         current_syscall_error.rangeErrorMax = period_us;
@@ -148,19 +151,20 @@ static exception_t decodeSchedControl_Configure(word_t length, cap_t cap, word_t
     }
 
     setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
-    return invokeSchedControl_Configure(SC_PTR(cap_sched_context_cap_get_capSCPtr(targetCap)),
-                                        cap_sched_control_cap_get_core(cap),
-                                        budget_ticks,
-                                        period_ticks,
-                                        extra_refills + MIN_REFILLS,
-                                        badge);
+    return invokeSchedControl_ConfigureFlags(SC_PTR(cap_sched_context_cap_get_capSCPtr(targetCap)),
+                                             cap_sched_control_cap_get_core(cap),
+                                             budget_ticks,
+                                             period_ticks,
+                                             extra_refills + MIN_REFILLS,
+                                             badge,
+                                             flags);
 }
 
 exception_t decodeSchedControlInvocation(word_t label, cap_t cap, word_t length, word_t *buffer)
 {
     switch (label) {
-    case SchedControlConfigure:
-        return  decodeSchedControl_Configure(length, cap, buffer);
+    case SchedControlConfigureFlags:
+        return  decodeSchedControl_ConfigureFlags(length, cap, buffer);
     default:
         userError("SchedControl invocation: Illegal operation attempted.");
         current_syscall_error.type = seL4_IllegalOperation;