RTOS/seL4
1
0
Fork 0
forked from Imagelibrary/seL4
Code Pull Requests Activity

Rename MAX_BUDGET to MAX_PERIOD

Browse Source 
As this variable bounds both the period and the budget and the period
itself bounds the budget, the name for this variable would be more
appropriately named 'MAX_PERIOD'

Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This commit is contained in:
Curtis Millar
2021-02-02 10:01:21 +11:00
committed by Curtis Millar
parent f2c96c3246
commit 295a5b2818
6 changed files with 12 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
CHANGES
View File

@@ -30,6 +30,7 @@ Upcoming release: BREAKING
- Constant bandwidth observes a continuous constant bandwidth of budget/period - Constant bandwidth observes a continuous constant bandwidth of budget/period
- Sporadic server behaves as described by Sprunt et. al. - Sporadic server behaves as described by Sprunt et. al.
- In an overcommitted system, sporadic preserves accumulated time - In an overcommitted system, sporadic preserves accumulated time
* MCS kernel configuration option KernelStaticMaxBudgetUs renamed to KernelStaticMaxPeriodUs
## Upgrade Notes ## Upgrade Notes

2
config.cmake
View File

@@ -454,7 +454,7 @@ config_string(
) )
config_string( config_string(
KernelStaticMaxBudgetUs KERNEL_STATIC_MAX_BUDGET_US KernelStaticMaxPeriodUs KERNEL_STATIC_MAX_PERIOD_US
"Specifies a static maximum to which scheduling context can have \ "Specifies a static maximum to which scheduling context can have \
either its period or budget configured." either its period or budget configured."
DEFAULT 0 DEFAULT 0

2
configs/ARM_MCS_verified.cmake
View File

@@ -22,5 +22,5 @@ set(KernelPrinting OFF CACHE BOOL "")
set(KernelNumDomains 16 CACHE STRING "") set(KernelNumDomains 16 CACHE STRING "")
set(KernelMaxNumBootinfoUntypedCap 166 CACHE STRING "") set(KernelMaxNumBootinfoUntypedCap 166 CACHE STRING "")
set(KernelIsMCS ON CACHE BOOL "") set(KernelIsMCS ON CACHE BOOL "")
set(KernelStaticMaxBudgetUs "(60 * 60 * MS_IN_S * US_IN_MS)" CACHE STRING "") set(KernelStaticMaxPeriodUs "(60 * 60 * MS_IN_S * US_IN_MS)" CACHE STRING "")
include(${CMAKE_CURRENT_LIST_DIR}/seL4Config.cmake) include(${CMAKE_CURRENT_LIST_DIR}/seL4Config.cmake)

2
configs/RISCV64_MCS_verified.cmake
View File

@@ -25,7 +25,7 @@ set(KernelMaxNumBootinfoUntypedCap 166 CACHE STRING "")
set(KernelRootCNodeSizeBits 19 CACHE STRING "") set(KernelRootCNodeSizeBits 19 CACHE STRING "")
set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "") set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
set(KernelIsMCS ON CACHE BOOL "") set(KernelIsMCS ON CACHE BOOL "")
set(KernelStaticMaxBudgetUs "(60 * 60 * MS_IN_S * US_IN_MS)" CACHE STRING "") set(KernelStaticMaxPeriodUs "(60 * 60 * MS_IN_S * US_IN_MS)" CACHE STRING "")
set(KernelClzNoBuiltin ON CACHE BOOL "") set(KernelClzNoBuiltin ON CACHE BOOL "")
set(KernelCtzNoBuiltin ON CACHE BOOL "") set(KernelCtzNoBuiltin ON CACHE BOOL "")
include(${CMAKE_CURRENT_LIST_DIR}/seL4Config.cmake) include(${CMAKE_CURRENT_LIST_DIR}/seL4Config.cmake)

8
include/kernel/sporadic.h
View File

@@ -33,11 +33,11 @@
* at least this much budget - see comment on refill_sufficient */ * at least this much budget - see comment on refill_sufficient */
#define MIN_BUDGET_US (2u * getKernelWcetUs() * CONFIG_KERNEL_WCET_SCALE) #define MIN_BUDGET_US (2u * getKernelWcetUs() * CONFIG_KERNEL_WCET_SCALE)
#define MIN_BUDGET (2u * getKernelWcetTicks() * CONFIG_KERNEL_WCET_SCALE) #define MIN_BUDGET (2u * getKernelWcetTicks() * CONFIG_KERNEL_WCET_SCALE)
#if (CONFIG_KERNEL_STATIC_MAX_BUDGET_US) != 0 #if (CONFIG_KERNEL_STATIC_MAX_PERIOD_US) != 0
#define MAX_BUDGET_US (CONFIG_KERNEL_STATIC_MAX_BUDGET_US) #define MAX_PERIOD_US (CONFIG_KERNEL_STATIC_MAX_PERIOD_US)
#else #else
#define MAX_BUDGET_US getMaxUsToTicks() #define MAX_PERIOD_US getMaxUsToTicks()
#endif /* CONFIG_KERNEL_STATIC_MAX_BUDGET_US != 0 */ #endif /* CONFIG_KERNEL_STATIC_MAX_PERIOD_US != 0 */
/* Short hand for accessing refill queue items */ /* Short hand for accessing refill queue items */
static inline refill_t *refill_index(sched_context_t *sc, word_t index) static inline refill_t *refill_index(sched_context_t *sc, word_t index)

8
src/object/schedcontrol.c
View File

@@ -116,19 +116,19 @@ static exception_t decodeSchedControl_ConfigureFlags(word_t length, cap_t cap, w
return EXCEPTION_SYSCALL_ERROR; return EXCEPTION_SYSCALL_ERROR;
} }
if (budget_us > MAX_BUDGET_US || budget_ticks < MIN_BUDGET) { if (budget_us > MAX_PERIOD_US || budget_ticks < MIN_BUDGET) {
userError("SchedControl_ConfigureFlags: budget out of range."); userError("SchedControl_ConfigureFlags: budget out of range.");
current_syscall_error.type = seL4_RangeError; current_syscall_error.type = seL4_RangeError;
current_syscall_error.rangeErrorMin = MIN_BUDGET_US; current_syscall_error.rangeErrorMin = MIN_BUDGET_US;
current_syscall_error.rangeErrorMax = MAX_BUDGET_US; current_syscall_error.rangeErrorMax = MAX_PERIOD_US;
return EXCEPTION_SYSCALL_ERROR; return EXCEPTION_SYSCALL_ERROR;
} }
if (period_us > MAX_BUDGET_US || period_ticks < MIN_BUDGET) { if (period_us > MAX_PERIOD_US || period_ticks < MIN_BUDGET) {
userError("SchedControl_ConfigureFlags: period out of range."); userError("SchedControl_ConfigureFlags: period out of range.");
current_syscall_error.type = seL4_RangeError; current_syscall_error.type = seL4_RangeError;
current_syscall_error.rangeErrorMin = MIN_BUDGET_US; current_syscall_error.rangeErrorMin = MIN_BUDGET_US;
current_syscall_error.rangeErrorMax = MAX_BUDGET_US; current_syscall_error.rangeErrorMax = MAX_PERIOD_US;
return EXCEPTION_SYSCALL_ERROR; return EXCEPTION_SYSCALL_ERROR;
} }