Tests for https://github.com/seL4/seL4/issues/941

apps/sel4test-tests/src/helpers.c

@@ -376,16 +376,26 @@ void set_helper_mcp(env_t env, helper_thread_t *thread, seL4_Word mcp)
     assert(error == seL4_NoError);
 }
 
-void set_helper_affinity(UNUSED env_t env, helper_thread_t *thread, seL4_Word affinity)
+int set_helper_affinity_fallible(UNUSED env_t env, helper_thread_t *thread, seL4_Word affinity)
 {
 #ifdef CONFIG_KERNEL_MCS
     seL4_Time timeslice = CONFIG_BOOT_THREAD_TIME_SLICE * US_IN_S;
-    int error = seL4_SchedControl_Configure(simple_get_sched_ctrl(&env->simple, affinity),
-                                            thread->thread.sched_context.cptr,
-                                            timeslice, timeslice, 0, 0);
-    ZF_LOGF_IF(error, "Failed to configure scheduling context");
+    return seL4_SchedControl_Configure(simple_get_sched_ctrl(&env->simple, affinity),
+                                       thread->thread.sched_context.cptr,
+                                       timeslice, timeslice, 0, 0);
+#elif CONFIG_MAX_NUM_NODES > 1
+    return seL4_TCB_SetAffinity(thread->thread.tcb.cptr, affinity);
+#else
+    assert(affinity == 0);
+#endif
+}
+
+void set_helper_affinity(UNUSED env_t env, helper_thread_t *thread, seL4_Word affinity)
+{
+    int error = set_helper_affinity_fallible(env, thread, affinity);
+#ifdef CONFIG_KERNEL_MCS
+    ZF_LOGF_IF(error, "Failed to configure scheduling context for affinity");
 #elif CONFIG_MAX_NUM_NODES > 1
-    int error = seL4_TCB_SetAffinity(thread->thread.tcb.cptr, affinity);
     ZF_LOGF_IF(error, "Failed to set tcb affinity");
 #endif
 }

apps/sel4test-tests/src/helpers.h

@@ -71,7 +71,12 @@ void set_helper_priority(env_t env, helper_thread_t *thread, seL4_Word prio);
 /* set a helper threads max control priority */
 void set_helper_mcp(env_t env, helper_thread_t *thread, seL4_Word mcp);
 
-/* set a helper threads core affinity. This will have no effect on passive threads. */
+/* set a helper threads core affinity. This will have no effect on passive threads (MCS).
+ * if it fails, return an error. */
+int set_helper_affinity_fallible(env_t env, helper_thread_t *thread, seL4_Word affinity);
+
+/* set a helper threads core affinity. This will have no effect on passive threads (MCS).
+ * if it fails, calls ZF_LOGF. */
 void set_helper_affinity(env_t env, helper_thread_t *thread, seL4_Word affinity);
 
 /* if CONFIG_KERNEL_MCS is set, set the helpers scheduling parameters */

apps/sel4test-tests/src/tests/binding.c

@@ -292,3 +292,135 @@ test_notification_binding_with_sc(env_t env)
 }
 DEFINE_TEST(BIND006, "Test passing thread notification binding with a scheduling context",
             test_notification_binding_with_sc, config_set(CONFIG_KERNEL_MCS))
+
+static int
+test_active_notification_binding_with_sc(env_t env)
+{
+    seL4_CPtr endpoint, notification;
+    int error;
+    helper_thread_t helper;
+    volatile int state = 0;
+
+    endpoint = vka_alloc_endpoint_leaky(&env->vka);
+    notification = vka_alloc_notification_leaky(&env->vka);
+
+    create_helper_thread(env, &helper);
+
+    /* set our prio lower so the helper thread runs when we start it */
+    set_helper_priority(env, &helper, 10);
+    error = seL4_TCB_SetPriority(env->tcb, env->tcb, 9);
+    test_eq(error, seL4_NoError);
+
+    error = seL4_TCB_BindNotification(helper.thread.tcb.cptr, notification);
+    test_eq(error, seL4_NoError);
+
+    /* start the helper so it is waiting on the endpoint */
+    start_helper(env, &helper, (helper_fn_t) bind0005_helper, endpoint,
+                 (seL4_Word) &state, 0, 0);
+    test_eq(state, 1);
+
+    /* clear its sc */
+    error = api_sc_unbind(helper.thread.sched_context.cptr);
+    test_eq(error, seL4_NoError);
+
+    /* signal it */
+    seL4_Signal(notification);
+    /* it should not progress until it has an SC */
+    test_eq(state, 1);
+
+    error = api_sc_bind(helper.thread.sched_context.cptr, notification);
+    test_eq(error, seL4_NoError);
+
+    /* now it should have got the signal.
+     * However: due to a kernel design issue https://github.com/seL4/seL4/issues/1617
+     * instead it blocks forever.
+     */
+    // test_eq(state, 2);
+    test_eq(state, 1);
+
+    return sel4test_get_result();
+}
+DEFINE_TEST(BIND007, "Test unbind TCB / rebind ntfn (passive server migration) with an active notification",
+            test_active_notification_binding_with_sc, config_set(CONFIG_KERNEL_MCS));
+
+static void
+bind0008_helper(seL4_CPtr endpoint, volatile int *state)
+{
+    *state = 1;
+    seL4_Wait(endpoint, NULL);
+    *state = 2;
+    seL4_Wait(endpoint, NULL);
+    *state = 3;
+}
+
+
+static int
+test_active_notification_binding_with_sc_lazy_rebind(env_t env)
+{
+    seL4_CPtr endpoint, notification;
+    int error;
+    helper_thread_t helper;
+    volatile int state = 0;
+
+    endpoint = vka_alloc_endpoint_leaky(&env->vka);
+    notification = vka_alloc_notification_leaky(&env->vka);
+
+    create_helper_thread(env, &helper);
+
+    /* set our prio lower so the helper thread runs when we start it */
+    set_helper_priority(env, &helper, 10);
+    error = seL4_TCB_SetPriority(env->tcb, env->tcb, 9);
+    test_eq(error, seL4_NoError);
+
+    /* set up a bound notification (so endpoint wait <-> notification) */
+    error = seL4_TCB_BindNotification(helper.thread.tcb.cptr, notification);
+    test_eq(error, seL4_NoError);
+
+    /* start the helper so it is waiting on the endpoint */
+    start_helper(env, &helper, (helper_fn_t) bind0008_helper, endpoint,
+                 (seL4_Word) &state, 0, 0);
+    test_eq(state, 1);
+
+    /* lower the helper priority so it won't be running */
+    set_helper_priority(env, &helper, 8);
+
+    /* signal the notification - will progress to running on the TCB's SC */
+    seL4_Signal(notification);
+
+    /* it should not progress until it is higher priority than us */
+    test_eq(state, 1);
+
+    /* check SC still bound to TCB */
+    error = api_sc_bind(helper.thread.sched_context.cptr, helper.thread.tcb.cptr);
+    test_eq(error, seL4_IllegalOperation);
+
+    /* perform lazy rebind */
+    error = api_sc_bind(helper.thread.sched_context.cptr, notification);
+    test_eq(error, seL4_NoError);
+
+    /* allow helper to run by bumping its priority */
+    set_helper_priority(env, &helper, 10);
+
+    /* it should now be waiting on its endpoint and will have unbound its TCB SC */
+    test_eq(state, 2);
+
+    /* bind and unbind TCB SC to demonstrate that it had been unbound */
+    error = api_sc_bind(helper.thread.sched_context.cptr, helper.thread.tcb.cptr);
+    test_eq(error, seL4_NoError);
+
+    error = api_sc_unbind_object(helper.thread.sched_context.cptr, helper.thread.tcb.cptr);
+    test_eq(error, seL4_NoError);
+
+    /* the notification should still be bound */
+    error = api_sc_bind(helper.thread.sched_context.cptr, notification);
+    test_eq(error, seL4_IllegalOperation);
+
+    /* signal so it should continue */
+    seL4_Signal(notification);
+
+    test_eq(state, 3);
+
+    return sel4test_get_result();
+}
+DEFINE_TEST(BIND008, "Test lazy SC rebind (passive server migration) with an active notification",
+            test_active_notification_binding_with_sc_lazy_rebind, config_set(CONFIG_KERNEL_MCS));

apps/sel4test-tests/src/tests/ipc.c

@@ -1356,8 +1356,6 @@ static int test_sched_donation_cross_core(env_t env)
 
     return sel4test_get_result();
 }
-/* This test currently fails.
-   See https://github.com/seL4/seL4/issues/941 and https://github.com/seL4/seL4/pull/986 */
-DEFINE_TEST(IPC0028, "Cross core sched donation", test_sched_donation_cross_core, false);
-/*            config_set(CONFIG_KERNEL_MCS) &&(CONFIG_MAX_NUM_NODES > 1)); */
+DEFINE_TEST(IPC0028, "Cross core sched donation", test_sched_donation_cross_core,
+            config_set(CONFIG_KERNEL_MCS) &&(CONFIG_MAX_NUM_NODES > 1));
 #endif /* CONFIG_KERNEL_MCS */