portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

mcs: small changes to ease verification

Browse source 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
Michael McInerney 2025-03-17 10:53:57 +10:30 committed by Gerwin Klein
parent 52725dd5b4
commit 019e4b608f
4 changed files with 16 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
include/kernel/faulthandler.h
View file

@ -11,7 +11,8 @@
#ifdef CONFIG_KERNEL_MCS
static inline bool_t validTimeoutHandler(tcb_t *tptr)
{
return cap_get_capType(TCB_PTR_CTE_PTR(tptr, tcbTimeoutHandler)->cap) == cap_endpoint_cap;
cap_t timeoutHandlerCap = TCB_PTR_CTE_PTR(tptr, tcbTimeoutHandler)->cap;
return cap_get_capType(timeoutHandlerCap) == cap_endpoint_cap;
}
void handleTimeout(tcb_t *tptr);

5
src/api/syscall.c
View file

@ -482,7 +482,7 @@ static inline void mcsPreemptionPoint(void)
if (isSchedulable(NODE_STATE(ksCurThread))) {
/* if the thread is schedulable, the tcb and scheduling context are still valid */
checkBudget();
} else if (NODE_STATE(ksCurSC)->scRefillMax) {
} else if (sc_active(NODE_STATE(ksCurSC))) {
/* otherwise, if the thread is not schedulable, the SC could be valid - charge it if so */
chargeBudget(NODE_STATE(ksConsumed), false);
} else {
@ -504,7 +504,8 @@ static void handleYield(void)
#ifdef CONFIG_KERNEL_MCS
/* Yield the current remaining budget */
ticks_t consumed = NODE_STATE(ksCurSC)->scConsumed + NODE_STATE(ksConsumed);
chargeBudget(refill_head(NODE_STATE(ksCurSC))->rAmount, false);
refill_t head = *refill_head(NODE_STATE(ksCurSC));
chargeBudget(head.rAmount, false);
/* Manually updated the scConsumed so that the full timeslice isn't added, just what was consumed */
NODE_STATE(ksCurSC)->scConsumed = consumed;
#else

7
src/kernel/faulthandler.c
View file

@ -14,8 +14,8 @@
#ifdef CONFIG_KERNEL_MCS
void handleFault(tcb_t *tptr)
{
bool_t hasFaultHandler = sendFaultIPC(tptr, TCB_PTR_CTE_PTR(tptr, tcbFaultHandler)->cap,
tptr->tcbSchedContext != NULL);
cap_t faultHandlerCap = TCB_PTR_CTE_PTR(tptr, tcbFaultHandler)->cap;
bool_t hasFaultHandler = sendFaultIPC(tptr, faultHandlerCap, tptr->tcbSchedContext != NULL);
if (!hasFaultHandler) {
handleNoFaultHandler(tptr);
}
@ -24,7 +24,8 @@ void handleFault(tcb_t *tptr)
void handleTimeout(tcb_t *tptr)
{
assert(validTimeoutHandler(tptr));
sendFaultIPC(tptr, TCB_PTR_CTE_PTR(tptr, tcbTimeoutHandler)->cap, false);
cap_t timeoutHandlerCap = TCB_PTR_CTE_PTR(tptr, tcbTimeoutHandler)->cap;
sendFaultIPC(tptr, timeoutHandlerCap, false);
}
bool_t sendFaultIPC(tcb_t *tptr, cap_t handlerCap, bool_t can_donate)

9
src/kernel/thread.c
View file

@ -607,7 +607,9 @@ void chargeBudget(ticks_t consumed, bool_t canTimeoutFault)
if (likely(NODE_STATE(ksCurSC) != NODE_STATE(ksIdleSC))) {
if (isRoundRobin(NODE_STATE(ksCurSC))) {
assert(refill_size(NODE_STATE(ksCurSC)) == MIN_REFILLS);
refill_head(NODE_STATE(ksCurSC))->rAmount += refill_tail(NODE_STATE(ksCurSC))->rAmount;
refill_t head = *refill_head(NODE_STATE(ksCurSC));
refill_t tail = *refill_tail(NODE_STATE(ksCurSC));
refill_head(NODE_STATE(ksCurSC))->rAmount = head.rAmount + tail.rAmount;
refill_tail(NODE_STATE(ksCurSC))->rAmount = 0;
} else {
refill_budget_check(consumed);
@ -627,7 +629,10 @@ void chargeBudget(ticks_t consumed, bool_t canTimeoutFault)
void endTimeslice(bool_t can_timeout_fault)
{
if (can_timeout_fault && !isRoundRobin(NODE_STATE(ksCurSC)) && validTimeoutHandler(NODE_STATE(ksCurThread))) {
bool_t round_robin = isRoundRobin(NODE_STATE(ksCurSC));
bool_t valid = validTimeoutHandler(NODE_STATE(ksCurThread));
if (can_timeout_fault && !round_robin && valid) {
current_fault = seL4_Fault_Timeout_new(NODE_STATE(ksCurSC)->scBadge);
handleTimeout(NODE_STATE(ksCurThread));
} else if (refill_ready(NODE_STATE(ksCurSC)) && refill_sufficient(NODE_STATE(ksCurSC), 0)) {