diff --git a/CHANGES b/CHANGES index bd3e82eb4..a0a479cb6 100644 --- a/CHANGES +++ b/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 --- diff --git a/include/kernel/sporadic.h b/include/kernel/sporadic.h index 285e90891..401f41051 100644 --- a/include/kernel/sporadic.h +++ b/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); diff --git a/include/object/structures.h b/include/object/structures.h index ca5c5fa56..787a0470a 100644 --- a/include/object/structures.h +++ b/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 { diff --git a/libsel4/include/interfaces/sel4.xml b/libsel4/include/interfaces/sel4.xml index 6392b2869..66844118d 100644 --- a/libsel4/include/interfaces/sel4.xml +++ b/libsel4/include/interfaces/sel4.xml @@ -644,7 +644,7 @@ - + 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). @@ -662,6 +662,8 @@ description="Number of extra sporadic replenishments this scheduling context should use. Ignored for round-robin threads."/> + diff --git a/libsel4/include/sel4/constants.h b/libsel4/include/sel4/constants.h index f5fe8cc9e..6bb3afa25 100644 --- a/libsel4/include/sel4/constants.h +++ b/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 diff --git a/libsel4/include/sel4/sel4.h b/libsel4/include/sel4/sel4.h index 710fb7af3..b8482bb3c 100644 --- a/libsel4/include/sel4/sel4.h +++ b/libsel4/include/sel4/sel4.h @@ -14,6 +14,7 @@ #include #include +#include #include #include diff --git a/libsel4/include/sel4/virtual_client.h b/libsel4/include/sel4/virtual_client.h new file mode 100644 index 000000000..ed41dada0 --- /dev/null +++ b/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 +#include +#include +#include +#include +#include + +/* + * 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 diff --git a/manual/parts/threads.tex b/manual/parts/threads.tex index bd391ee32..2142e8208 100644 --- a/manual/parts/threads.tex +++ b/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. diff --git a/src/kernel/thread.c b/src/kernel/thread.c index 029973eb4..f546fac3a 100644 --- a/src/kernel/thread.c +++ b/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)); diff --git a/src/object/endpoint.c b/src/object/endpoint.c index 10fe8c9ec..76bd6c8e3 100644 --- a/src/object/endpoint.c +++ b/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); diff --git a/src/object/notification.c b/src/object/notification.c index 0aef25ec0..3fc685186 100644 --- a/src/object/notification.c +++ b/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"); diff --git a/src/object/schedcontext.c b/src/object/schedcontext.c index 47e09a907..d935dbf6c 100644 --- a/src/object/schedcontext.c +++ b/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); diff --git a/src/object/schedcontrol.c b/src/object/schedcontrol.c index e9c94777e..80122339c 100644 --- a/src/object/schedcontrol.c +++ b/src/object/schedcontrol.c @@ -10,8 +10,8 @@ #include #include -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;