Thanks Indan for your detail reply.
By ready queue, I did mean the scheduling queue since the code named it as
ksReadyQueues.
For threads unbound from a SC, this thread will be removed from both
ksReadyQueues and ksReleaseHead according the code below:
void schedContext_unbindTCB(sched_context_t *sc, tcb_t *tcb)
{
assert(sc->scTcb == tcb);
/* tcb must already be stalled at this point */
if (tcb == NODE_STATE(ksCurThread)) {
rescheduleRequired();
}
tcbSchedDequeue(sc->scTcb);
tcbReleaseRemove(sc->scTcb);
sc->scTcb->tcbSchedContext = NULL;
sc->scTcb = NULL;
}
But for threads which are blocked at waiting for a signal/message, according
to your reply and the code, my current understanding is that:
Those threads which are in ThreadState_BlockedOnNotification(for example) will
be in neither ksReadyQueues nor ksReleaseHead, and these threads will be either
notification's queue or endpoint's queue which saves the blocked TCBs.
Am I right now?
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
