seL4/libsel4/include/sel4/constants.h
Curtis Millar afbea15710 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>
2021-04-14 15:24:40 +10:00

109 lines
2.9 KiB
C

/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <autoconf.h>
#include <sel4/macros.h>
#ifndef __ASSEMBLER__
#ifdef CONFIG_HARDWARE_DEBUG_API
/* API arg values for breakpoint API, "type" arguments. */
typedef enum {
seL4_DataBreakpoint = 0,
seL4_InstructionBreakpoint,
seL4_SingleStep,
seL4_SoftwareBreakRequest,
SEL4_FORCE_LONG_ENUM(seL4_BreakpointType)
} seL4_BreakpointType;
/* API arg values for breakpoint API, "access" arguments. */
typedef enum {
seL4_BreakOnRead = 0,
seL4_BreakOnWrite,
seL4_BreakOnReadWrite,
seL4_MaxBreakpointAccess,
SEL4_FORCE_LONG_ENUM(seL4_BreakpointAccess)
} seL4_BreakpointAccess;
/* Format of a debug-exception message. */
typedef enum {
seL4_DebugException_FaultIP,
seL4_DebugException_ExceptionReason,
seL4_DebugException_TriggerAddress,
seL4_DebugException_BreakpointNumber,
seL4_DebugException_Length,
SEL4_FORCE_LONG_ENUM(seL4_DebugException_Msg)
} seL4_DebugException_Msg;
#endif
enum priorityConstants {
seL4_InvalidPrio = -1,
seL4_MinPrio = 0,
seL4_MaxPrio = CONFIG_NUM_PRIORITIES - 1
};
/* seL4_MessageInfo_t defined in api/shared_types.bf */
enum seL4_MsgLimits {
seL4_MsgLengthBits = 7,
seL4_MsgExtraCapBits = 2
};
enum {
seL4_MsgMaxLength = 120,
};
#define seL4_MsgMaxExtraCaps (LIBSEL4_BIT(seL4_MsgExtraCapBits)-1)
/* seL4_CapRights_t defined in shared_types_*.bf */
#define seL4_CapRightsBits 4
typedef enum {
seL4_NoFailure = 0,
seL4_InvalidRoot,
seL4_MissingCapability,
seL4_DepthMismatch,
seL4_GuardMismatch,
SEL4_FORCE_LONG_ENUM(seL4_LookupFailureType),
} seL4_LookupFailureType;
#endif /* !__ASSEMBLER__ */
#ifdef CONFIG_KERNEL_MCS
/* Minimum size of a scheduling context (2^{n} bytes) */
#define seL4_MinSchedContextBits 8
#ifndef __ASSEMBLER__
/* the size of a scheduling context, excluding extra refills */
#define seL4_CoreSchedContextBytes (10 * sizeof(seL4_Word) + (6 * 8))
/* the size of a single extra refill */
#define seL4_RefillSizeBytes (2 * 8)
/*
* @brief Calculate the max extra refills a scheduling context can contain for a specific size.
*
* @param size of the schedulding context. Must be >= seL4_MinSchedContextBits
* @return the max number of extra refills that can be passed to seL4_SchedControl_Configure for
* this scheduling context
*/
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
#define DEBUG_MESSAGE_START 6
#define DEBUG_MESSAGE_MAXLEN 50
#endif