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; } }