mcs: associate scheduling context + ntfn

This commit allows scheduling contexts to be bound
to notification objects. When a passive server
receives a notification it will receive the scheduling
context from the notification. When the server
blocks the scheduling context is returned.

include/object/schedcontext.h

@@ -69,4 +69,9 @@ void schedContext_resume(sched_context_t *sc);
  */
 void schedContext_donate(sched_context_t *sc, tcb_t *to);
 
+/* Bind scheduling context to a notification */
+void schedContext_bindNtfn(sched_context_t *sc, notification_t *ntfn);
+/* unbind scheduling context from a notification */
+void schedContext_unbindNtfn(sched_context_t *sc);
+
 #endif /* __OBJECT_SCHED_CONTEXT_H */

include/object/structures.h

@@ -328,6 +328,10 @@ struct sched_context {
      * when the scheduling context was passed over a Call */
     reply_t *scReply;
 
+    /* notification this scheduling context is bound to
+     * (scTcb and scNotification cannot be set at the same time) */
+    notification_t *scNotification;
+
     /* Amount of refills this sc tracks */
     word_t scRefillMax;
     /* Index of the head of the refill circular buffer */

include/object/structures_32.bf

@@ -159,8 +159,15 @@ block endpoint {
     field state 2
 }
 
--- Notification object: size = 16 bytes
+-- Notification object: size = 16 bytes (32 bytes on mcs)
 block notification {
+#ifdef CONFIG_KERNEL_MCS
+    padding 96
+
+    field_high ntfnSchedContext 28
+    padding 4
+#endif
+
     field_high ntfnBoundTCB 28
     padding 4
 

include/object/structures_64.bf

@@ -207,12 +207,20 @@ block endpoint {
     field state 2
 }
 
--- Async endpoint: size = 32 bytes
+-- Async endpoint: size = 32 bytes (64 bytes on mcs)
 block notification {
 #if BF_CANONICAL_RANGE == 48
+#ifdef CONFIG_KERNEL_MCS
+    padding 16
+    field_high ntfnSchedContext 48
+#endif
     padding 16
     field_high ntfnBoundTCB 48
 #elif BF_CANONICAL_RANGE == 39
+#ifdef CONFIG_KERNEL_MCS
+    padding 25
+    field_high ntfnSchedContext 39
+#endif
     padding 25
     field_high ntfnBoundTCB 39
 #else

libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h

@@ -151,10 +151,12 @@ enum {
 #endif
 
 #define seL4_EndpointBits 4
-#define seL4_NotificationBits 4
-#define seL4_SchedContextBits 8
 #ifdef CONFIG_KERNEL_MCS
+#define seL4_NotificationBits 5
+#define seL4_SchedContextBits 8
 #define seL4_ReplyBits 4
+#else
+#define seL4_NotificationBits 4
 #endif
 
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT

libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h

@@ -124,10 +124,12 @@ enum {
 #define seL4_SlotBits 5
 #define seL4_TCBBits 11
 #define seL4_EndpointBits 4
-#define seL4_NotificationBits 5
-#define seL4_SchedContextBits 8
 #ifdef CONFIG_KERNEL_MCS
+#define seL4_NotificationBits 6
+#define seL4_SchedContextBits 8
 #define seL4_ReplyBits           5
+#else
+#define seL4_NotificationBits 5
 #endif
 
 #define seL4_PageTableBits 12

libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h

@@ -30,7 +30,13 @@
 #define seL4_SlotBits         4
 #define seL4_TCBBits         11
 #define seL4_EndpointBits     4
+#ifdef CONFIG_KERNEL_MCS
+#define seL4_NotificationBits 5
+#define seL4_ReplyBits        4
+#define seL4_SchedContextBits 8
+#else
 #define seL4_NotificationBits 4
+#endif
 
 #define seL4_PageTableBits   12
 #define seL4_PageTableEntryBits 2
@@ -46,10 +52,6 @@
 #define seL4_ASIDPoolBits    12
 #define seL4_ASIDPoolIndexBits 10
 #define seL4_WordSizeBits 2
-#define seL4_SchedContextBits 8
-#ifdef CONFIG_KERNEL_MCS
-#define seL4_ReplyBits        4
-#endif
 
 #define seL4_HugePageBits    30 /* 1GB */
 #define seL4_PDPTBits         0

libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h

@@ -35,7 +35,13 @@
 #define seL4_TCBBits            11
 #endif
 #define seL4_EndpointBits       4
+#ifdef CONFIG_KERNEL_MCS
+#define seL4_NotificationBits   6
+#define seL4_ReplyBits          5
+#define seL4_SchedContextBits    8
+#else
 #define seL4_NotificationBits   5
+#endif
 
 #define seL4_PageTableBits      12
 #define seL4_PageTableEntryBits 3
@@ -60,10 +66,6 @@
 #define seL4_NumASIDPoolsBits    3
 #define seL4_ASIDPoolBits       12
 #define seL4_ASIDPoolIndexBits 9
-#define seL4_SchedContextBits    8
-#ifdef CONFIG_KERNEL_MCS
-#define seL4_ReplyBits           5
-#endif
 
 /* Untyped size limits */
 #define seL4_MinUntypedBits 4

src/object/notification.c

@@ -42,6 +42,27 @@ static inline void ntfn_set_active(notification_t *ntfnPtr, word_t badge)
     notification_ptr_set_ntfnMsgIdentifier(ntfnPtr, badge);
 }
 
+#ifdef CONFIG_KERNEL_MCS
+static inline void maybeDonateSchedContext(tcb_t *tcb, notification_t *ntfnPtr)
+{
+    if (tcb->tcbSchedContext == NULL) {
+        sched_context_t *sc = SC_PTR(notification_ptr_get_ntfnSchedContext(ntfnPtr));
+        if (sc != NULL && sc->scTcb == NULL) {
+            schedContext_donate(sc, tcb);
+        }
+    }
+}
+
+static inline void maybeReturnSchedContext(notification_t *ntfnPtr, tcb_t *tcb)
+{
+
+    sched_context_t *sc = SC_PTR(notification_ptr_get_ntfnSchedContext(ntfnPtr));
+    if (sc == tcb->tcbSchedContext) {
+        tcb->tcbSchedContext = NULL;
+        sc->scTcb = NULL;
+    }
+}
+#endif
 
 void sendSignal(notification_t *ntfnPtr, word_t badge)
 {
@@ -53,6 +74,9 @@ void sendSignal(notification_t *ntfnPtr, word_t badge)
             if (thread_state_ptr_get_tsType(&tcb->tcbState) == ThreadState_BlockedOnReceive) {
                 /* Send and start thread running */
                 cancelIPC(tcb);
+#ifdef CONFIG_KERNEL_MCS
+                maybeDonateSchedContext(tcb, ntfnPtr);
+#endif
                 setThreadState(tcb, ThreadState_Running);
                 setRegister(tcb, badgeRegister, badge);
                 possibleSwitchTo(tcb);
@@ -65,6 +89,9 @@ void sendSignal(notification_t *ntfnPtr, word_t badge)
                 } else
 #endif /* ENABLE_SMP_SUPPORT */
                 {
+#ifdef CONFIG_KERNEL_MCS
+                    maybeDonateSchedContext(tcb, ntfnPtr);
+#endif
                     setThreadState(tcb, ThreadState_Running);
                     setRegister(tcb, badgeRegister, badge);
                     Arch_leaveVMAsyncTransfer(tcb);
@@ -105,6 +132,9 @@ void sendSignal(notification_t *ntfnPtr, word_t badge)
             notification_ptr_set_state(ntfnPtr, NtfnState_Idle);
         }
 
+#ifdef CONFIG_KERNEL_MCS
+        maybeDonateSchedContext(dest, ntfnPtr);
+#endif
         setThreadState(dest, ThreadState_Running);
         setRegister(dest, badgeRegister, badge);
         possibleSwitchTo(dest);
@@ -140,6 +170,9 @@ void receiveSignal(tcb_t *thread, cap_t cap, bool_t isBlocking)
                                         ThreadState_BlockedOnNotification);
             thread_state_ptr_set_blockingObject(&thread->tcbState,
                                                 NTFN_REF(ntfnPtr));
+#ifdef CONFIG_KERNEL_MCS
+            maybeReturnSchedContext(ntfnPtr, thread);
+#endif
             scheduleTCB(thread);
 
             /* Enqueue TCB */
@@ -160,6 +193,9 @@ void receiveSignal(tcb_t *thread, cap_t cap, bool_t isBlocking)
             thread, badgeRegister,
             notification_ptr_get_ntfnMsgIdentifier(ntfnPtr));
         notification_ptr_set_state(ntfnPtr, NtfnState_Idle);
+#ifdef CONFIG_KERNEL_MCS
+        maybeDonateSchedContext(thread, ntfnPtr);
+#endif
         break;
     }
 }

src/object/objecttype.c

@@ -126,7 +126,9 @@ finaliseCap_ret_t finaliseCap(cap_t cap, bool_t final, bool_t exposed)
     case cap_notification_cap:
         if (final) {
             notification_t *ntfn = NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap));
-
+#ifdef CONFIG_KERNEL_MCS
+            schedContext_unbindNtfn(SC_PTR(notification_ptr_get_ntfnSchedContext(ntfn)));
+#endif
             unbindMaybeNotification(ntfn);
             cancelAllSignals(ntfn);
         }
@@ -212,6 +214,7 @@ finaliseCap_ret_t finaliseCap(cap_t cap, bool_t final, bool_t exposed)
         if (final) {
             sched_context_t *sc = SC_PTR(cap_sched_context_cap_get_capSCPtr(cap));
             schedContext_unbindAllTCBs(sc);
+            schedContext_unbindNtfn(sc);
             if (sc->scReply) {
                 assert(call_stack_get_isHead(sc->scReply->replyNext));
                 sc->scReply->replyNext = call_stack_new(0, false);

src/object/schedcontext.c

@@ -14,7 +14,17 @@
 
 static exception_t invokeSchedContext_UnbindObject(sched_context_t *sc, cap_t cap)
 {
-    schedContext_unbindTCB(sc, TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)));
+    switch (cap_get_capType(cap)) {
+    case cap_thread_cap:
+        schedContext_unbindTCB(sc, sc->scTcb);
+        break;
+    case cap_notification_cap:
+        schedContext_unbindNtfn(sc);
+        break;
+    default:
+        fail("invalid cap type");
+    }
+
     return EXCEPTION_NONE;
 }
 
@@ -27,18 +37,28 @@ static exception_t decodeSchedContext_UnbindObject(sched_context_t *sc, extra_ca
     }
 
     cap_t cap = extraCaps.excaprefs[0]->cap;
-    if (cap_get_capType(cap) != cap_thread_cap) {
+    switch (cap_get_capType(cap)) {
+    case cap_thread_cap:
+        if (sc->scTcb != TCB_PTR(cap_thread_cap_get_capTCBPtr(cap))) {
+            userError("SchedContext UnbindObject: object not bound");
+            current_syscall_error.type = seL4_IllegalOperation;
+            return EXCEPTION_SYSCALL_ERROR;
+        }
+        break;
+    case cap_notification_cap:
+        if (sc->scNotification != NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap))) {
+            userError("SchedContext UnbindObject: object not bound");
+            current_syscall_error.type = seL4_IllegalOperation;
+            return EXCEPTION_SYSCALL_ERROR;
+        }
+        break;
+
+    default:
         userError("SchedContext_Unbind: invalid cap");
         current_syscall_error.type = seL4_InvalidCapability;
         current_syscall_error.invalidCapNumber = 1;
         return EXCEPTION_SYSCALL_ERROR;
-    }
 
-    if (sc->scTcb != TCB_PTR(cap_thread_cap_get_capTCBPtr(cap))) {
-        userError("SchedContext_Unbind: object not bound to this sc");
-        current_syscall_error.type = seL4_InvalidCapability;
-        current_syscall_error.invalidCapNumber = 1;
-        return EXCEPTION_SYSCALL_ERROR;
     }
 
     setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
@@ -47,7 +67,17 @@ static exception_t decodeSchedContext_UnbindObject(sched_context_t *sc, extra_ca
 
 static exception_t invokeSchedContext_Bind(sched_context_t *sc, cap_t cap)
 {
-    schedContext_bindTCB(sc, TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)));
+    switch (cap_get_capType(cap)) {
+    case cap_thread_cap:
+        schedContext_bindTCB(sc, TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)));
+        break;
+    case cap_notification_cap:
+        schedContext_bindNtfn(sc, NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap)));
+        break;
+    default:
+        fail("invalid cap type");
+    }
+
     return EXCEPTION_NONE;
 }
 
@@ -61,25 +91,35 @@ static exception_t decodeSchedContext_Bind(sched_context_t *sc, extra_caps_t ext
 
     cap_t cap = extraCaps.excaprefs[0]->cap;
 
-    if (sc->scTcb != NULL) {
+    if (sc->scTcb != NULL || sc->scNotification != NULL) {
         userError("SchedContext_Bind: sched context already bound.");
         current_syscall_error.type = seL4_IllegalOperation;
         return EXCEPTION_SYSCALL_ERROR;
     }
 
-    if (cap_get_capType(cap) != cap_thread_cap) {
+    switch (cap_get_capType(cap)) {
+    case cap_thread_cap:
+        if (TCB_PTR(cap_thread_cap_get_capTCBPtr(cap))->tcbSchedContext != NULL) {
+            userError("SchedContext_Bind: tcb already bound.");
+            current_syscall_error.type = seL4_IllegalOperation;
+            return EXCEPTION_SYSCALL_ERROR;
+        }
+
+        break;
+    case cap_notification_cap:
+        if (notification_ptr_get_ntfnSchedContext(NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap)))) {
+            userError("SchedContext_Bind: notification already bound");
+            current_syscall_error.type = seL4_IllegalOperation;
+            return EXCEPTION_SYSCALL_ERROR;
+        }
+        break;
+    default:
         userError("SchedContext_Bind: invalid cap.");
         current_syscall_error.type = seL4_InvalidCapability;
         current_syscall_error.invalidCapNumber = 1;
         return EXCEPTION_SYSCALL_ERROR;
     }
 
-    if (TCB_PTR(cap_thread_cap_get_capTCBPtr(cap))->tcbSchedContext != NULL) {
-        userError("SchedContext_Bind: tcb already bound.");
-        current_syscall_error.type = seL4_IllegalOperation;
-        return EXCEPTION_SYSCALL_ERROR;
-    }
-
     setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
     return invokeSchedContext_Bind(sc, cap);
 }
@@ -87,6 +127,7 @@ static exception_t decodeSchedContext_Bind(sched_context_t *sc, extra_caps_t ext
 static exception_t invokeSchedContext_Unbind(sched_context_t *sc)
 {
     schedContext_unbindAllTCBs(sc);
+    schedContext_unbindNtfn(sc);
     if (sc->scReply) {
         sc->scReply->replyNext = call_stack_new(0, false);
         sc->scReply = NULL;
@@ -205,3 +246,17 @@ void schedContext_donate(sched_context_t *sc, tcb_t *to)
     }
 #endif
 }
+
+void schedContext_bindNtfn(sched_context_t *sc, notification_t *ntfn)
+{
+    notification_ptr_set_ntfnSchedContext(ntfn, SC_REF(sc));
+    sc->scNotification = ntfn;
+}
+
+void schedContext_unbindNtfn(sched_context_t *sc)
+{
+    if (sc && sc->scNotification) {
+        notification_ptr_set_ntfnSchedContext(sc->scNotification, SC_REF(0));
+        sc->scNotification = NULL;
+    }
+}