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;
    }
}
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

Reply via email to