Hello guys,
I got confused on the implementation of receiveSignal in sel4 with MCS.
When the notification status is NtfnState_Active, the kernel will try to donate the notification's schedule context to the thread by calling maybeDonateSchedContext.
My confusion point is that: If the thread doesn't have a valid schedule context, the thread will not be able to execute, then how can this thread call receiveSignal to receive the signal?
void receiveSignal(tcb_t *thread, cap_t cap, bool_t isBlocking)
{
notification_t *ntfnPtr;
ntfnPtr = NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap));
switch (notification_ptr_get_state(ntfnPtr)) {
....
case NtfnState_Active:
setRegister(
thread, badgeRegister,
notification_ptr_get_ntfnMsgIdentifier(ntfnPtr));
notification_ptr_set_state(ntfnPtr, NtfnState_Idle);
#ifdef CONFIG_KERNEL_MCS
maybeDonateSchedContext(thread, ntfnPtr);
// If the SC has been donated to the current thread (in a reply_recv, send_recv scenario) then
// we may need to perform refill_unblock_check if the SC is becoming activated.
if (thread->tcbSchedContext != NODE_STATE(ksCurSC) && sc_sporadic(thread->tcbSchedContext)) {
refill_unblock_check(thread->tcbSchedContext);
}
#endif
break;
}
}
