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

mcs: use local variable in restart

Browse Source 
This eases verification by using a local variable
which remains unchanged during execution of the
function.

This preserves semantics since refill_unblock_check
will not modify the tcbSchedContext field of any TCB.

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
Michael McInerney
2026-02-25 11:53:18 +10:30
committed by Gerwin Klein
parent b5cc70d753
commit efd9426e17
1 changed files with 4 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
src/kernel/thread.c
View File

@@ -93,11 +93,11 @@ void restart(tcb_t *target)
cancelIPC(target); cancelIPC(target);
#ifdef CONFIG_KERNEL_MCS #ifdef CONFIG_KERNEL_MCS
setThreadState(target, ThreadState_Restart); setThreadState(target, ThreadState_Restart);
if (sc_sporadic(target->tcbSchedContext) sched_context_t *sc = target->tcbSchedContext;
&& target->tcbSchedContext != NODE_STATE(ksCurSC)) { if (sc_sporadic(sc) && sc != NODE_STATE(ksCurSC)) {
refill_unblock_check(target->tcbSchedContext); refill_unblock_check(sc);
} }
schedContext_resume(target->tcbSchedContext); schedContext_resume(sc);
if (isSchedulable(target)) { if (isSchedulable(target)) {
possibleSwitchTo(target); possibleSwitchTo(target);
} }