28 lines
809 B
Diff
28 lines
809 B
Diff
--- src/kernel/sel4/src/kernel/thread.c
|
|
+++ src/kernel/sel4/src/kernel/thread.c
|
|
@@ -437,8 +437,11 @@ scheduleTCB(tcb_t *tptr)
|
|
void
|
|
timerTick(void)
|
|
{
|
|
- if (likely(thread_state_get_tsType(NODE_STATE(ksCurThread)->tcbState) ==
|
|
- ThreadState_Running)) {
|
|
+ switch (thread_state_get_tsType(NODE_STATE(ksCurThread)->tcbState)) {
|
|
+ case ThreadState_Running:
|
|
+#ifdef CONFIG_VTX
|
|
+ case ThreadState_RunningVM:
|
|
+#endif
|
|
if (NODE_STATE(ksCurThread)->tcbTimeSlice > 1) {
|
|
NODE_STATE(ksCurThread)->tcbTimeSlice--;
|
|
} else {
|
|
@@ -446,6 +449,10 @@ timerTick(void)
|
|
SCHED_APPEND_CURRENT_TCB;
|
|
rescheduleRequired();
|
|
}
|
|
+ break;
|
|
+ default:
|
|
+ /* no tick updates */
|
|
+ break;
|
|
}
|
|
|
|
if (CONFIG_NUM_DOMAINS > 1) {
|