From cd95ae19dcdf3e88dc5f9d125ba6a658be705805 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 17 Jun 2024 20:12:15 +1000 Subject: [PATCH 01/21] ipc: re-enable test IPC0028 Signed-off-by: Gerwin Klein --- apps/sel4test-tests/src/tests/ipc.c | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/apps/sel4test-tests/src/tests/ipc.c b/apps/sel4test-tests/src/tests/ipc.c index 1de6b426d..5054e35ee 100644 --- a/apps/sel4test-tests/src/tests/ipc.c +++ b/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 */ From b82f10a7c9e43fabc1f29ffddca2778b31b7aa18 Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Fri, 8 May 2026 11:52:02 +1000 Subject: [PATCH 02/21] SCHED022: test self core-migration on non-MCS Use the set_helper_affinity[_fallible] to change the current thread's affinity, so that we can test this on both MCS and non-MCS. Signed-off-by: Julia Vassiliki --- apps/sel4test-tests/src/helpers.c | 22 ++++++++++++++------ apps/sel4test-tests/src/helpers.h | 7 ++++++- apps/sel4test-tests/src/tests/scheduler.c | 25 ++++++++--------------- 3 files changed, 30 insertions(+), 24 deletions(-) diff --git a/apps/sel4test-tests/src/helpers.c b/apps/sel4test-tests/src/helpers.c index f3a824392..b3bb8cc5f 100644 --- a/apps/sel4test-tests/src/helpers.c +++ b/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 } diff --git a/apps/sel4test-tests/src/helpers.h b/apps/sel4test-tests/src/helpers.h index efb60cfa6..e783715e3 100644 --- a/apps/sel4test-tests/src/helpers.h +++ b/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 */ diff --git a/apps/sel4test-tests/src/tests/scheduler.c b/apps/sel4test-tests/src/tests/scheduler.c index 600842ac1..7bb1481ec 100644 --- a/apps/sel4test-tests/src/tests/scheduler.c +++ b/apps/sel4test-tests/src/tests/scheduler.c @@ -1648,23 +1648,14 @@ int sched0022_to_fn(struct env *env, helper_thread_t *thread, seL4_CPtr ep) seL4_MessageInfo_t tag = {0}; seL4_MessageInfo_ptr_set_length(&tag, 2); - /* change to core 1 */ - seL4_Error error = api_sched_ctrl_configure(simple_get_sched_ctrl(&env->simple, 1), - thread->thread.sched_context.cptr, - 10000, - 10000, - 0, - 0); + /* change our affinity to core 1 then back to core 0 and report errors */ + + int error = set_helper_affinity_fallible(env, thread, /* core */ 1); seL4_SetMR(0, error); - /* and back to core 0 */ - error = api_sched_ctrl_configure(simple_get_sched_ctrl(&env->simple, 0), - thread->thread.sched_context.cptr, - 10000, - 10000, - 0, - 0); + error = set_helper_affinity_fallible(env, thread, /* core */ 0); seL4_SetMR(1, error); + seL4_Send(ep, tag); return 0; } @@ -1672,7 +1663,7 @@ int sched0022_to_fn(struct env *env, helper_thread_t *thread, seL4_CPtr ep) /* Test that a helper thread can move itself back from another core. * Save the return values and check them in test thread. */ -static int test_changing_affinity(struct env *env) +static int test_changing_affinity_self(struct env *env) { int error; helper_thread_t t0; @@ -1699,5 +1690,5 @@ static int test_changing_affinity(struct env *env) return sel4test_get_result(); } -DEFINE_TEST(SCHED0022, "test changing a helper threads core", test_changing_affinity, - (config_set(CONFIG_KERNEL_MCS) &&(CONFIG_MAX_NUM_NODES > 1))); +DEFINE_TEST(SCHED0022, "test helper thread changing its own core", test_changing_affinity_self, + (CONFIG_MAX_NUM_NODES > 1)); From 957f657e16fea2f86d3a8be399119aa7d8dccc9c Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Mon, 11 May 2026 13:24:10 +1000 Subject: [PATCH 03/21] SCHED_CONTEXT_SMP_001: add Signed-off-by: Julia Vassiliki --- .../src/tests/schedcontext_smp.c | 159 ++++++++++++++++++ 1 file changed, 159 insertions(+) create mode 100644 apps/sel4test-tests/src/tests/schedcontext_smp.c diff --git a/apps/sel4test-tests/src/tests/schedcontext_smp.c b/apps/sel4test-tests/src/tests/schedcontext_smp.c new file mode 100644 index 000000000..57b8247bc --- /dev/null +++ b/apps/sel4test-tests/src/tests/schedcontext_smp.c @@ -0,0 +1,159 @@ +/* + * Copyright 2026, UNSW + * + * SPDX-License-Identifier: BSD-2-Clause + */ +#include +#include +#include +#include +#include +#include + +#include "../helpers.h" + +void sched_context_smp_001_helper_fn(seL4_CPtr ep, seL4_CPtr sc, seL4_CPtr tcb, void *arg3) +{ + int error = seL4_SchedContext_Bind(sc, tcb); + + seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1); + seL4_SetMR(0, error); + seL4_Send(ep, tag); +} + +void sched_context_smp_001_recipient_fn(seL4_CPtr ep, void *arg1, void *arg2, void *arg3) +{ + /* Basically, say yes we ran */ + seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 0); + seL4_Send(ep, tag); +} + +int test_smp_bind_tcb_other_core(env_t env) +{ + /** + * This is for testing when the target TCB has no SchedContext. + * + * Cases: + * - bind local SC to not running remote TCB + * - bind remote SC to not running remote TCB + * - bind remote SC to local thread (which necessarily is not running) + * + * The local:local case is tested elsewhere. + **/ + + helper_thread_t bind_helper; + helper_thread_t bind_recipient; + seL4_CPtr ep_helper; + seL4_CPtr ep_recipient; + seL4_CPtr sc; + seL4_CPtr ntfn; + int error; + + seL4_CPtr sc_ctrl_local = simple_get_sched_ctrl(&env->simple, 0); + seL4_CPtr sc_ctrl_remote = simple_get_sched_ctrl(&env->simple, 1); + seL4_Time timeslice = CONFIG_BOOT_THREAD_TIME_SLICE * US_IN_S; + + ep_helper = vka_alloc_endpoint_leaky(&env->vka); + ep_recipient = vka_alloc_endpoint_leaky(&env->vka); + ntfn = vka_alloc_notification_leaky(&env->vka); + + { + printf("Local SC to not running remote TCB\n"); + + /* Our SC is local */ + sc = vka_alloc_sched_context_leaky(&env->vka); + error = seL4_SchedControl_Configure(sc_ctrl_local, sc, timeslice, timeslice, 0, 0); + ZF_LOGF_IF(error, "should be able to configure SC"); + + create_helper_thread(env, &bind_helper); + create_helper_thread(env, &bind_recipient); + NAME_THREAD(get_helper_tcb(&bind_helper), "SCHED_CONTEXT_SMP_001 Bind Helper"); + NAME_THREAD(get_helper_tcb(&bind_recipient), "SCHED_CONTEXT_SMP_001 Bind Recipient"); + + /* move the recipient to the other core so it is a remote TCB. */ + set_helper_affinity(env, &bind_recipient, /* core */ 1); + /* unbind recipient so we can bind to it, also so it doesn't run */ + error = api_sc_unbind(get_helper_sched_context(&bind_recipient)); + ZF_LOGF_IF(error, "unable to unbind"); + + start_helper(env, &bind_helper, (helper_fn_t) sched_context_smp_001_helper_fn, ep_helper, sc, get_helper_tcb(&bind_recipient), 0); + start_helper(env, &bind_recipient, (helper_fn_t) sched_context_smp_001_recipient_fn, ep_recipient, 0, 0, 0); + + seL4_Wait(ep_helper, NULL); + test_eq(seL4_GetMR(0), seL4_NoError); + + /* We know that this thread got to run */ + seL4_Wait(ep_recipient, NULL); + + cleanup_helper(env, &bind_helper); + cleanup_helper(env, &bind_recipient); + } + + { + printf("Remote SC to not running remote TCB\n"); + + /* Our SC is remote */ + sc = vka_alloc_sched_context_leaky(&env->vka); + error = seL4_SchedControl_Configure(sc_ctrl_remote, sc, timeslice, timeslice, 0, 0); + ZF_LOGF_IF(error, "should be able to configure SC"); + + create_helper_thread(env, &bind_helper); + create_helper_thread(env, &bind_recipient); + NAME_THREAD(get_helper_tcb(&bind_helper), "SCHED_CONTEXT_SMP_001 Bind Helper"); + NAME_THREAD(get_helper_tcb(&bind_recipient), "SCHED_CONTEXT_SMP_001 Bind Recipient"); + + /* move the recipient to the other core so it is a remote TCB. */ + set_helper_affinity(env, &bind_recipient, /* core */ 1); + /* unbind recipient so we can bind to it, also so it doesn't run */ + error = api_sc_unbind(get_helper_sched_context(&bind_recipient)); + ZF_LOGF_IF(error, "unable to unbind"); + + start_helper(env, &bind_helper, (helper_fn_t) sched_context_smp_001_helper_fn, ep_helper, sc, get_helper_tcb(&bind_recipient), 0); + start_helper(env, &bind_recipient, (helper_fn_t) sched_context_smp_001_recipient_fn, ep_recipient, 0, 0, 0); + + seL4_Wait(ep_helper, NULL); + test_eq(seL4_GetMR(0), seL4_NoError); + + /* We know that this thread got to run */ + seL4_Wait(ep_recipient, NULL); + + cleanup_helper(env, &bind_helper); + cleanup_helper(env, &bind_recipient); + } + + { + printf("Remote SC to local thread\n"); + + /* Our SC is remote */ + sc = vka_alloc_sched_context_leaky(&env->vka); + error = seL4_SchedControl_Configure(sc_ctrl_remote, sc, timeslice, timeslice, 0, 0); + ZF_LOGF_IF(error, "should be able to configure SC"); + + create_helper_thread(env, &bind_helper); + create_helper_thread(env, &bind_recipient); + NAME_THREAD(get_helper_tcb(&bind_helper), "SCHED_CONTEXT_SMP_001 Bind Helper"); + NAME_THREAD(get_helper_tcb(&bind_recipient), "SCHED_CONTEXT_SMP_001 Bind Recipient"); + + /* unbind recipient so we can bind to it, also so it doesn't run */ + error = api_sc_unbind(get_helper_sched_context(&bind_recipient)); + ZF_LOGF_IF(error, "unable to unbind"); + + start_helper(env, &bind_helper, (helper_fn_t) sched_context_smp_001_helper_fn, ep_helper, sc, get_helper_tcb(&bind_recipient), 0); + start_helper(env, &bind_recipient, (helper_fn_t) sched_context_smp_001_recipient_fn, ep_recipient, 0, 0, 0); + + seL4_Wait(ep_helper, NULL); + test_eq(seL4_GetMR(0), seL4_NoError); + + /* We know that this thread got to run */ + seL4_Wait(ep_recipient, NULL); + + cleanup_helper(env, &bind_helper); + cleanup_helper(env, &bind_recipient); + } + + return sel4test_get_result(); +} + +DEFINE_TEST(SCHED_CONTEXT_SMP_001, "Test SC bind to a TCB on another core", + test_smp_bind_tcb_other_core, config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 1)); + From 3688e7d4816fd2077d9d4d0ffabc2c1885c1f017 Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Mon, 11 May 2026 13:40:23 +1000 Subject: [PATCH 04/21] SCHED_CONTEXT_SMP_001: remove unnecessary helper thread Signed-off-by: Julia Vassiliki --- .../src/tests/schedcontext_smp.c | 44 ++++--------------- 1 file changed, 9 insertions(+), 35 deletions(-) diff --git a/apps/sel4test-tests/src/tests/schedcontext_smp.c b/apps/sel4test-tests/src/tests/schedcontext_smp.c index 57b8247bc..21c5dc3a7 100644 --- a/apps/sel4test-tests/src/tests/schedcontext_smp.c +++ b/apps/sel4test-tests/src/tests/schedcontext_smp.c @@ -12,15 +12,6 @@ #include "../helpers.h" -void sched_context_smp_001_helper_fn(seL4_CPtr ep, seL4_CPtr sc, seL4_CPtr tcb, void *arg3) -{ - int error = seL4_SchedContext_Bind(sc, tcb); - - seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1); - seL4_SetMR(0, error); - seL4_Send(ep, tag); -} - void sched_context_smp_001_recipient_fn(seL4_CPtr ep, void *arg1, void *arg2, void *arg3) { /* Basically, say yes we ran */ @@ -41,21 +32,16 @@ int test_smp_bind_tcb_other_core(env_t env) * The local:local case is tested elsewhere. **/ - helper_thread_t bind_helper; helper_thread_t bind_recipient; - seL4_CPtr ep_helper; seL4_CPtr ep_recipient; seL4_CPtr sc; - seL4_CPtr ntfn; int error; seL4_CPtr sc_ctrl_local = simple_get_sched_ctrl(&env->simple, 0); seL4_CPtr sc_ctrl_remote = simple_get_sched_ctrl(&env->simple, 1); seL4_Time timeslice = CONFIG_BOOT_THREAD_TIME_SLICE * US_IN_S; - ep_helper = vka_alloc_endpoint_leaky(&env->vka); ep_recipient = vka_alloc_endpoint_leaky(&env->vka); - ntfn = vka_alloc_notification_leaky(&env->vka); { printf("Local SC to not running remote TCB\n"); @@ -65,9 +51,7 @@ int test_smp_bind_tcb_other_core(env_t env) error = seL4_SchedControl_Configure(sc_ctrl_local, sc, timeslice, timeslice, 0, 0); ZF_LOGF_IF(error, "should be able to configure SC"); - create_helper_thread(env, &bind_helper); create_helper_thread(env, &bind_recipient); - NAME_THREAD(get_helper_tcb(&bind_helper), "SCHED_CONTEXT_SMP_001 Bind Helper"); NAME_THREAD(get_helper_tcb(&bind_recipient), "SCHED_CONTEXT_SMP_001 Bind Recipient"); /* move the recipient to the other core so it is a remote TCB. */ @@ -76,16 +60,14 @@ int test_smp_bind_tcb_other_core(env_t env) error = api_sc_unbind(get_helper_sched_context(&bind_recipient)); ZF_LOGF_IF(error, "unable to unbind"); - start_helper(env, &bind_helper, (helper_fn_t) sched_context_smp_001_helper_fn, ep_helper, sc, get_helper_tcb(&bind_recipient), 0); start_helper(env, &bind_recipient, (helper_fn_t) sched_context_smp_001_recipient_fn, ep_recipient, 0, 0, 0); - seL4_Wait(ep_helper, NULL); - test_eq(seL4_GetMR(0), seL4_NoError); + int error = seL4_SchedContext_Bind(sc, get_helper_tcb(&bind_recipient)); + test_eq(error, seL4_NoError); - /* We know that this thread got to run */ + /* We know that this thread got to run if it signalled this */ seL4_Wait(ep_recipient, NULL); - cleanup_helper(env, &bind_helper); cleanup_helper(env, &bind_recipient); } @@ -97,9 +79,7 @@ int test_smp_bind_tcb_other_core(env_t env) error = seL4_SchedControl_Configure(sc_ctrl_remote, sc, timeslice, timeslice, 0, 0); ZF_LOGF_IF(error, "should be able to configure SC"); - create_helper_thread(env, &bind_helper); create_helper_thread(env, &bind_recipient); - NAME_THREAD(get_helper_tcb(&bind_helper), "SCHED_CONTEXT_SMP_001 Bind Helper"); NAME_THREAD(get_helper_tcb(&bind_recipient), "SCHED_CONTEXT_SMP_001 Bind Recipient"); /* move the recipient to the other core so it is a remote TCB. */ @@ -108,16 +88,14 @@ int test_smp_bind_tcb_other_core(env_t env) error = api_sc_unbind(get_helper_sched_context(&bind_recipient)); ZF_LOGF_IF(error, "unable to unbind"); - start_helper(env, &bind_helper, (helper_fn_t) sched_context_smp_001_helper_fn, ep_helper, sc, get_helper_tcb(&bind_recipient), 0); start_helper(env, &bind_recipient, (helper_fn_t) sched_context_smp_001_recipient_fn, ep_recipient, 0, 0, 0); - seL4_Wait(ep_helper, NULL); - test_eq(seL4_GetMR(0), seL4_NoError); + int error = seL4_SchedContext_Bind(sc, get_helper_tcb(&bind_recipient)); + test_eq(error, seL4_NoError); - /* We know that this thread got to run */ + /* We know that this thread got to run if it signalled this */ seL4_Wait(ep_recipient, NULL); - cleanup_helper(env, &bind_helper); cleanup_helper(env, &bind_recipient); } @@ -129,25 +107,21 @@ int test_smp_bind_tcb_other_core(env_t env) error = seL4_SchedControl_Configure(sc_ctrl_remote, sc, timeslice, timeslice, 0, 0); ZF_LOGF_IF(error, "should be able to configure SC"); - create_helper_thread(env, &bind_helper); create_helper_thread(env, &bind_recipient); - NAME_THREAD(get_helper_tcb(&bind_helper), "SCHED_CONTEXT_SMP_001 Bind Helper"); NAME_THREAD(get_helper_tcb(&bind_recipient), "SCHED_CONTEXT_SMP_001 Bind Recipient"); /* unbind recipient so we can bind to it, also so it doesn't run */ error = api_sc_unbind(get_helper_sched_context(&bind_recipient)); ZF_LOGF_IF(error, "unable to unbind"); - start_helper(env, &bind_helper, (helper_fn_t) sched_context_smp_001_helper_fn, ep_helper, sc, get_helper_tcb(&bind_recipient), 0); start_helper(env, &bind_recipient, (helper_fn_t) sched_context_smp_001_recipient_fn, ep_recipient, 0, 0, 0); - seL4_Wait(ep_helper, NULL); - test_eq(seL4_GetMR(0), seL4_NoError); + int error = seL4_SchedContext_Bind(sc, get_helper_tcb(&bind_recipient)); + test_eq(error, seL4_NoError); - /* We know that this thread got to run */ + /* We know that this thread got to run if it signalled this */ seL4_Wait(ep_recipient, NULL); - cleanup_helper(env, &bind_helper); cleanup_helper(env, &bind_recipient); } From 9c668ccdcb1f4b630e9f1ddd8a33dea87c71fb20 Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Mon, 11 May 2026 14:00:52 +1000 Subject: [PATCH 05/21] [unrelated] add BIND007 that tests current MCS design quirk behaviour Signed-off-by: Julia Vassiliki --- apps/sel4test-tests/src/tests/binding.c | 50 +++++++++++++++++++++++++ 1 file changed, 50 insertions(+) diff --git a/apps/sel4test-tests/src/tests/binding.c b/apps/sel4test-tests/src/tests/binding.c index bff64e1d9..ef389e479 100644 --- a/apps/sel4test-tests/src/tests/binding.c +++ b/apps/sel4test-tests/src/tests/binding.c @@ -292,3 +292,53 @@ 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)); From 0111440ff230ad641af13cac6e7490381310498e Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Mon, 11 May 2026 17:23:36 +1000 Subject: [PATCH 06/21] [unrelated] add a test BIND008 to just confirm signal and lazy rebind is OK Signed-off-by: Julia Vassiliki --- apps/sel4test-tests/src/tests/binding.c | 82 +++++++++++++++++++++++++ 1 file changed, 82 insertions(+) diff --git a/apps/sel4test-tests/src/tests/binding.c b/apps/sel4test-tests/src/tests/binding.c index ef389e479..c879dcb35 100644 --- a/apps/sel4test-tests/src/tests/binding.c +++ b/apps/sel4test-tests/src/tests/binding.c @@ -342,3 +342,85 @@ test_active_notification_binding_with_sc(env_t env) } 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)); From 68ee258437e83f3d1f1cbf3b89b5610ce295328f Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Tue, 12 May 2026 17:10:21 +1000 Subject: [PATCH 07/21] SMP/MCS: add test for passive server setup on other core Signed-off-by: Julia Vassiliki --- .../src/tests/schedcontext_smp.c | 103 ++++++++++++++++++ 1 file changed, 103 insertions(+) diff --git a/apps/sel4test-tests/src/tests/schedcontext_smp.c b/apps/sel4test-tests/src/tests/schedcontext_smp.c index 21c5dc3a7..969ccb3f4 100644 --- a/apps/sel4test-tests/src/tests/schedcontext_smp.c +++ b/apps/sel4test-tests/src/tests/schedcontext_smp.c @@ -131,3 +131,106 @@ int test_smp_bind_tcb_other_core(env_t env) DEFINE_TEST(SCHED_CONTEXT_SMP_001, "Test SC bind to a TCB on another core", test_smp_bind_tcb_other_core, config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 1)); +int sched_context_smp_002_helper_fn(void) +{ + return 1; +} + +void sched_context_smp_002_lazy_fn(seL4_CPtr notification_in, seL4_CPtr notification_out) +{ + seL4_Signal(notification_out); + + seL4_Wait(notification_in, NULL); + + seL4_Signal(notification_out); + + seL4_Wait(notification_in, NULL); +} + +int test_passive_thread_start_smp(env_t env) +{ + helper_thread_t helper; + seL4_CPtr notification = vka_alloc_notification_leaky(&env->vka); + int error; + + seL4_Time timeslice = CONFIG_BOOT_THREAD_TIME_SLICE * US_IN_S; + + seL4_CPtr sc_remote = vka_alloc_sched_context_leaky(&env->vka); + error = seL4_SchedControl_Configure(simple_get_sched_ctrl(&env->simple, 1), sc_remote, timeslice, timeslice, 0, 0); + ZF_LOGF_IF(error, "should be able to configure SC"); + + create_helper_thread(env, &helper); + + /* unbind the default SC; + make it so that there is no SC. */ + error = api_sc_unbind(helper.thread.sched_context.cptr); + test_eq(error, seL4_NoError); + + /* ========== resume then bind ================ */ + start_helper(env, &helper, (helper_fn_t) sched_context_smp_002_helper_fn, 0, 0, 0, 0); + + error = api_sc_bind(sc_remote, helper.thread.tcb.cptr); + test_eq(error, seL4_NoError); + + error = wait_for_helper(&helper); + test_eq(error, 1); + + /* cleanup */ + cleanup_helper(env, &helper); + + /* ============ bind then resume =============== */ + create_helper_thread(env, &helper); + + /* unbind the default SC; + make it so that there is no SC. */ + error = api_sc_unbind(helper.thread.sched_context.cptr); + test_eq(error, seL4_NoError); + + error = api_sc_bind(sc_remote, helper.thread.tcb.cptr); + test_eq(error, seL4_NoError); + + start_helper(env, &helper, (helper_fn_t) sched_context_smp_002_helper_fn, 0, 0, 0, 0); + + error = seL4_TCB_Resume(helper.thread.tcb.cptr); + test_eq(error, seL4_NoError); + + error = wait_for_helper(&helper); + test_eq(error, 1); + + /* cleanup */ + cleanup_helper(env, &helper); + + /* ============ lazy unbind =================== */ + create_helper_thread(env, &helper); + + /* unbind the default SC */ + error = api_sc_unbind(helper.thread.sched_context.cptr); + test_eq(error, seL4_NoError); + /* add back our desired SC */ + error = api_sc_bind(sc_remote, helper.thread.tcb.cptr); + test_eq(error, seL4_NoError); + + error = api_sc_bind(sc_remote, notification); + test_eq(error, seL4_NoError); + /* set helper to higher prio to make behaviour deterministic */ + set_helper_priority(env, &helper, env->priority + 1); + + /* double check that the tcb is still bound */ + error = api_sc_bind(sc_remote, helper.thread.tcb.cptr); + test_eq(error, seL4_IllegalOperation); + + seL4_CPtr notification_in = vka_alloc_notification_leaky(&env->vka); + start_helper(env, &helper, (helper_fn_t)sched_context_smp_002_lazy_fn, notification, notification_in, 0, 0); + + /* Unfortunately, unlike SCHED_CONTEXT_0007 we can't test that we can rebind the + * TCB SC to test that this is the case, because there's no way to atomically + * or deterministically wait for the helper thread on the other core to run + * the seL4_Wait(). + * However we can check that it has run and that it can run again after + * being signalled. */ + seL4_Wait(notification_in, NULL); + seL4_Signal(notification); + seL4_Wait(notification_in, NULL); + + return sel4test_get_result(); +} +DEFINE_TEST(SCHED_CONTEXT_SMP_002, "test resuming a passive thread and binding scheduling context on another core", + test_passive_thread_start_smp, config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 1)); From 1d29a0dfca8afcffb7d5e26bb097d7771cccb6b4 Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Wed, 13 May 2026 10:47:44 +1000 Subject: [PATCH 08/21] SCHED_CONTEXT_SMP_002: make deterministic using NBSendWait Signed-off-by: Julia Vassiliki --- .../src/tests/schedcontext_smp.c | 52 ++++++++++++------- 1 file changed, 34 insertions(+), 18 deletions(-) diff --git a/apps/sel4test-tests/src/tests/schedcontext_smp.c b/apps/sel4test-tests/src/tests/schedcontext_smp.c index 969ccb3f4..3e5d2a8da 100644 --- a/apps/sel4test-tests/src/tests/schedcontext_smp.c +++ b/apps/sel4test-tests/src/tests/schedcontext_smp.c @@ -136,15 +136,17 @@ int sched_context_smp_002_helper_fn(void) return 1; } -void sched_context_smp_002_lazy_fn(seL4_CPtr notification_in, seL4_CPtr notification_out) +void sched_context_smp_002_lazy_fn(seL4_CPtr endpoint, seL4_CPtr notification) { - seL4_Signal(notification_out); - - seL4_Wait(notification_in, NULL); + seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 0); + (void)seL4_NBSendWait(endpoint, tag, notification, NULL); +} - seL4_Signal(notification_out); +void sched_context_smp_002_high_priority_helper(seL4_CPtr endpoint_cross, seL4_CPtr ep_hi_to_low) +{ + (void)seL4_Wait(endpoint_cross, NULL); - seL4_Wait(notification_in, NULL); + seL4_Send(ep_hi_to_low, seL4_MessageInfo_new(0, 0, 0, 0)); } int test_passive_thread_start_smp(env_t env) @@ -217,18 +219,32 @@ int test_passive_thread_start_smp(env_t env) error = api_sc_bind(sc_remote, helper.thread.tcb.cptr); test_eq(error, seL4_IllegalOperation); - seL4_CPtr notification_in = vka_alloc_notification_leaky(&env->vka); - start_helper(env, &helper, (helper_fn_t)sched_context_smp_002_lazy_fn, notification, notification_in, 0, 0); - - /* Unfortunately, unlike SCHED_CONTEXT_0007 we can't test that we can rebind the - * TCB SC to test that this is the case, because there's no way to atomically - * or deterministically wait for the helper thread on the other core to run - * the seL4_Wait(). - * However we can check that it has run and that it can run again after - * being signalled. */ - seL4_Wait(notification_in, NULL); - seL4_Signal(notification); - seL4_Wait(notification_in, NULL); + /* To be able to reproduce the test in SCHED_CONTEXT_007 where we rebind the + * TCB SC to test that it has been returned away, it is difficult to do + * deterministically. The best solution I can think of is to start a higher + * priority thread on this core that waits on an endpoint; this test thread + * should then only continue once that is blocked. Then the other core thread + * can perform an NBSendWait which should result in returning the TCB SC. + * This will then allow us to in this thread wait for the higher priority + * local thread to signal us, and so we can guarantee at this point the + * remote thread will be blocked on Wait. + */ + + helper_thread_t hi_helper; + create_helper_thread(env, &hi_helper); + set_helper_priority(env, &hi_helper, env->priority + 1); + seL4_CPtr endpoint_cross = vka_alloc_endpoint_leaky(&env->vka); + seL4_CPtr endpoint_hi_low = vka_alloc_endpoint_leaky(&env->vka); + /* this will run and receive first */ + start_helper(env, &hi_helper, (helper_fn_t)sched_context_smp_002_high_priority_helper, endpoint_cross, endpoint_hi_low, 0, 0); + + start_helper(env, &helper, (helper_fn_t)sched_context_smp_002_lazy_fn, endpoint_cross, notification, 0, 0); + + seL4_Wait(endpoint_hi_low, NULL); + + /* the tcb should have been unbound lazily when the helper called seL4_Wait */ + error = api_sc_bind(get_helper_sched_context(&helper), get_helper_tcb(&helper)); + test_eq(error, seL4_NoError); return sel4test_get_result(); } From c3945a0dedf093bed9fdaaf571411ce201d320b6 Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Wed, 13 May 2026 12:06:15 +1000 Subject: [PATCH 09/21] add SCHED_CONTEXT_SMP_004 'update a remote task's SC to have budget to run immediately.' Signed-off-by: Julia Vassiliki --- .../src/tests/schedcontext_smp.c | 97 +++++++++++++++++++ 1 file changed, 97 insertions(+) diff --git a/apps/sel4test-tests/src/tests/schedcontext_smp.c b/apps/sel4test-tests/src/tests/schedcontext_smp.c index 3e5d2a8da..2ec420b6f 100644 --- a/apps/sel4test-tests/src/tests/schedcontext_smp.c +++ b/apps/sel4test-tests/src/tests/schedcontext_smp.c @@ -12,6 +12,30 @@ #include "../helpers.h" +/* FIXME: this is a temporary hack and should be exported via libsel4. + * https://github.com/seL4/seL4/issues/1659 + */ +#ifndef MAX_PERIOD_US +/* Conservative, but long enough (~ half an hour) */ +#define MAX_PERIOD_US (1ULL << 31) +#endif + +#ifndef MIN_BUDGET_US +#ifdef CONFIG_PLAT_TK1 +#define MIN_BUDGET_US (2 * 100) +#else +#define MIN_BUDGET_US (2 * 10) +#endif +#endif + +static inline seL4_CPtr badge_endpoint(env_t env, seL4_Word badge, seL4_CPtr ep) +{ + seL4_CPtr slot = get_free_slot(env); + int error = cnode_mint(env, ep, slot, seL4_AllRights, badge); + test_error_eq(error, seL4_NoError); + return slot; +} + void sched_context_smp_001_recipient_fn(seL4_CPtr ep, void *arg1, void *arg2, void *arg3) { /* Basically, say yes we ran */ @@ -250,3 +274,76 @@ int test_passive_thread_start_smp(env_t env) } DEFINE_TEST(SCHED_CONTEXT_SMP_002, "test resuming a passive thread and binding scheduling context on another core", test_passive_thread_start_smp, config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 1)); + +/* + * Once https://github.com/seL4/seL4/issues/1617 is fixed, an equivalent of + * BIND0007 should be added here as SCHED_CONTEXT_SMP_003. + */ + +void sched_context_smp_004_helper_fn(env_t env, seL4_CPtr ep) +{ + /* Make sure this has run for at least MIN_BUDGET_US by poll-waiting that long */ + uint64_t start_ns = sel4test_timestamp(env); + uint64_t end_ns = start_ns + MIN_BUDGET_US * NS_IN_US; + while (sel4test_timestamp(env) < end_ns) { + for (int i = 0; i < 1000; i++) { + asm volatile("nop" ::: "memory"); + } + } + + seL4_Send(ep, seL4_MessageInfo_new(0, 0, 0, 0)); +} + +int test_update_remote_sc_with_budget(env_t env) +{ + + /** + * Idea behind this: a remote thread might have run out of a budget. + * If we make a remote thread that has a tiny budget (the minimum) + * but a very long period (the maximum) then once it will runout it will + * basically never refill: so, if we reconfigure the SC to have full + * bandwidth (budget = period) then it should start running again. + **/ + + int error; + helper_thread_t helper; + seL4_CPtr ep_unbadged = vka_alloc_endpoint_leaky(&env->vka); + seL4_CPtr ep = badge_endpoint(env, 0x100, ep_unbadged); + + create_helper_thread(env, &helper); + + /* make the helper run on the remote core with no budget */ + error = seL4_SchedControl_Configure( + /* schedcontrol */ simple_get_sched_ctrl(&env->simple, 1), + /* schedcontext */ get_helper_sched_context(&helper), + /* budget */ MIN_BUDGET_US, /* period */ MAX_PERIOD_US, /* refills */ 0, /* badge */ 0); + ZF_LOGF_IF(error, "should be able to configure SC"); + + start_helper(env, &helper, (helper_fn_t)sched_context_smp_004_helper_fn, (seL4_Word)env, ep, 0, 0); + + /* Mostly a hack: wait at least twice MIN_BUDGET_US */ + sel4test_sleep(env, 2 * MIN_BUDGET_US * NS_IN_US); + + seL4_Word sender_badge; + seL4_NBWait(ep, &sender_badge); + /* if the badge is zero then NBWait failed (see doNBRecvFailedTransfer) + * and so it must haven't run up to seL4_Send. but we've waited at least + * 2x as long as we needed for this remote helper to to have run if it + * did have the budget. basically this is testing that the remote thread got + * blocked due to not having enough budget. */ + test_eq(sender_badge, 0); + + /* give the helper on the remote core infinite budget, so it should run again */ + error = seL4_SchedControl_Configure( + /* schedcontrol */ simple_get_sched_ctrl(&env->simple, 1), + /* schedcontext */ get_helper_sched_context(&helper), + /* budget */ MAX_PERIOD_US, /* period */ MAX_PERIOD_US, /* refills */ 0, /* badge */ 0); + + seL4_Wait(ep, NULL); + + cleanup_helper(env, &helper); + + return sel4test_get_result(); +} +DEFINE_TEST(SCHED_CONTEXT_SMP_004, "update a remote task's SC to have budget to run immediately.", + test_update_remote_sc_with_budget, config_set(CONFIG_HAVE_TIMER) && config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 1)); From b17e95b15ea1eeb98243e07a955a36886bf070b6 Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Wed, 13 May 2026 12:26:56 +1000 Subject: [PATCH 10/21] SCHED0023: increase a remote task's priority Signed-off-by: Julia Vassiliki --- apps/sel4test-tests/src/tests/scheduler.c | 52 +++++++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/apps/sel4test-tests/src/tests/scheduler.c b/apps/sel4test-tests/src/tests/scheduler.c index 7bb1481ec..7fd0c7c01 100644 --- a/apps/sel4test-tests/src/tests/scheduler.c +++ b/apps/sel4test-tests/src/tests/scheduler.c @@ -1692,3 +1692,55 @@ static int test_changing_affinity_self(struct env *env) } DEFINE_TEST(SCHED0022, "test helper thread changing its own core", test_changing_affinity_self, (CONFIG_MAX_NUM_NODES > 1)); + +void sched_0023_helper_high_fn(void) +{ + /* Infinitely loop taking up budget */ + while (true) { + asm volatile("nop" ::: "memory"); + } +} + +void sched_0023_helper_low_fn(volatile int *state, seL4_CPtr ntfn) +{ + *state = 2; + seL4_Signal(ntfn); +} + +static int test_set_higher_prio_remote(struct env *env) +{ + helper_thread_t high_thread, low_thread; + seL4_CPtr ntfn = vka_alloc_notification_leaky(&env->vka); + + create_helper_thread(env, &high_thread); + create_helper_thread(env, &low_thread); + + assert(CONFIG_NUM_PRIORITIES > 3); + + set_helper_priority(env, &high_thread, 2); + set_helper_priority(env, &low_thread, 1); + + set_helper_affinity(env, &high_thread, 1); + set_helper_affinity(env, &low_thread, 1); + + /* fine to use this cross core because of single-copy atomicity on an aligned (32-bit) variable */ + volatile int state = 0; + + /* start our two remote helpers */ + start_helper(env, &high_thread, (helper_fn_t) sched_0023_helper_high_fn, 0, 0, 0, 0); + start_helper(env, &low_thread, (helper_fn_t) sched_0023_helper_low_fn, (seL4_Word)&state, ntfn, 0, 0); + + /* check that the low function hasn't run and update the state */ + test_eq(state, 0); + + /* raise the helper priority of low above high */ + set_helper_priority(env, &low_thread, 3); + + /* helper should run and set state to 2 */ + seL4_Wait(ntfn, NULL); + test_eq(state, 2); + + return sel4test_get_result(); +} +DEFINE_TEST(SCHED0023, "test set prio to a higher prio runs higher prio thread remote core", + test_set_higher_prio, (CONFIG_MAX_NUM_NODES > 1)); From 326b2f61b0123f1574c16ed45c63852cb03ed646 Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Wed, 13 May 2026 12:39:47 +1000 Subject: [PATCH 11/21] SCHED0024: resuming a suspended remote task Signed-off-by: Julia Vassiliki --- apps/sel4test-tests/src/tests/scheduler.c | 48 +++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/apps/sel4test-tests/src/tests/scheduler.c b/apps/sel4test-tests/src/tests/scheduler.c index 7fd0c7c01..f986e43c7 100644 --- a/apps/sel4test-tests/src/tests/scheduler.c +++ b/apps/sel4test-tests/src/tests/scheduler.c @@ -1744,3 +1744,51 @@ static int test_set_higher_prio_remote(struct env *env) } DEFINE_TEST(SCHED0023, "test set prio to a higher prio runs higher prio thread remote core", test_set_higher_prio, (CONFIG_MAX_NUM_NODES > 1)); + +void sched_0024_helper_fn(volatile int *state, seL4_CPtr ntfn) +{ + /* tell the test that we're ready (non-blocking as cross-core) */ + seL4_Signal(ntfn); + + /* start spinning so we can be suspend+resume somewhere OK */ + while (*state != 1); + + /* tell the test that the resume worked */ + *state = 2; + seL4_Signal(ntfn); +} + +static int test_resume_suspended_remote_task(struct env *env) +{ + helper_thread_t thread; + int error; + seL4_CPtr ntfn = vka_alloc_notification_leaky(&env->vka); + + create_helper_thread(env, &thread); + set_helper_affinity(env, &thread, 1); + + /* fine to use this cross core because of single-copy atomicity on an aligned (32-bit) variable */ + volatile int state = 0; + + /* start our remote helper */ + start_helper(env, &thread, (helper_fn_t) sched_0024_helper_fn, (seL4_Word)&state, ntfn, 0, 0); + + /* wait for remote helper to tell us it is ready - it should then be spinning */ + seL4_Wait(ntfn, NULL); + + error = seL4_TCB_Suspend(get_helper_tcb(&thread)); + test_error_eq(error, seL4_NoError); + + /* resume the remote thread now */ + state = 1; + error = seL4_TCB_Resume(get_helper_tcb(&thread)); + test_error_eq(error, seL4_NoError); + + /* helper should run and set state to 2 */ + seL4_Wait(ntfn, NULL); + test_eq(state, 2); + + return sel4test_get_result(); +} +DEFINE_TEST(SCHED0024, "test resuming a suspended remote task", + test_resume_suspended_remote_task, (CONFIG_MAX_NUM_NODES > 1)); From 51881aec5284cda8c3325381ba0ea4ab3649bb93 Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Wed, 13 May 2026 12:48:24 +1000 Subject: [PATCH 12/21] SCHED0025: seL4_SchedContext_YieldTo remote task Signed-off-by: Julia Vassiliki --- apps/sel4test-tests/src/tests/scheduler.c | 33 +++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/apps/sel4test-tests/src/tests/scheduler.c b/apps/sel4test-tests/src/tests/scheduler.c index f986e43c7..3740c7dbb 100644 --- a/apps/sel4test-tests/src/tests/scheduler.c +++ b/apps/sel4test-tests/src/tests/scheduler.c @@ -1792,3 +1792,36 @@ static int test_resume_suspended_remote_task(struct env *env) } DEFINE_TEST(SCHED0024, "test resuming a suspended remote task", test_resume_suspended_remote_task, (CONFIG_MAX_NUM_NODES > 1)); + +int test_yieldTo_remote(env_t env) +{ + int error; + helper_thread_t to, from; + volatile seL4_SchedContext_YieldTo_t ret; + + create_helper_thread(env, &to); + create_helper_thread(env, &from); + + start_helper(env, &to, (helper_fn_t) sched0018_to_fn, 0, 0, 0, 0); + start_helper(env, &from, (helper_fn_t) sched0017_helper_fn, to.thread.sched_context.cptr, (seL4_Word) &ret, 0, 0); + + /* To on a different core than From */ + set_helper_affinity(env, &to, 1); + set_helper_affinity(env, &from, 0); + + set_helper_mcp(env, &to, seL4_MaxPrio); + set_helper_mcp(env, &from, seL4_MaxPrio); + error = set_helper_sched_params(env, &to, 500 * US_IN_MS, 500 * US_IN_MS, 0); + test_eq(error, seL4_NoError); + error = set_helper_sched_params(env, &from, 500 * US_IN_MS, 500 * US_IN_MS, 0); + test_eq(error, seL4_NoError); + + ZF_LOGD("Wait for from\n"); + wait_for_helper(&from); + test_eq(ret.error, seL4_NoError); + test_geq(ret.consumed, 0llu); + + return sel4test_get_result(); +} +DEFINE_TEST(SCHED0025, "Test seL4_SchedContext_YieldTo remote", + test_yieldTo_remote, config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 1)); From c018d86d09e124c273d7ba7495450f9ff2d13f38 Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Wed, 13 May 2026 13:25:38 +1000 Subject: [PATCH 13/21] SCHED_CONTEXT_SMP_005: blocking remote tasks Signed-off-by: Julia Vassiliki --- .../src/tests/schedcontext_smp.c | 74 +++++++++++++++++++ 1 file changed, 74 insertions(+) diff --git a/apps/sel4test-tests/src/tests/schedcontext_smp.c b/apps/sel4test-tests/src/tests/schedcontext_smp.c index 2ec420b6f..9b07d0f3f 100644 --- a/apps/sel4test-tests/src/tests/schedcontext_smp.c +++ b/apps/sel4test-tests/src/tests/schedcontext_smp.c @@ -347,3 +347,77 @@ int test_update_remote_sc_with_budget(env_t env) } DEFINE_TEST(SCHED_CONTEXT_SMP_004, "update a remote task's SC to have budget to run immediately.", test_update_remote_sc_with_budget, config_set(CONFIG_HAVE_TIMER) && config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 1)); + +void sched_context_smp_005_helper_fn(volatile int *state, seL4_CPtr ntfn, seL4_CPtr ep) +{ + *state = 1; + /* wait on ntfn */ + seL4_Wait(ntfn, NULL); + *state = 2; + + /* wait on ep */ + seL4_Wait(ep, NULL); + *state = 3; + + /* perform a send so we generate a reply that server can use to wake us up */ + seL4_Call(ep, seL4_MessageInfo_new(0, 0, 0, 0)); + *state = 4; +} + +void wait_eq_timeout(volatile int *state, int value, int timeout) +{ + int count = 0; + while (true) { + if (*state == value) { + return; + } else if (count >= timeout) { + /* register the failure */ + test_lt(count, timeout); + return; + } + + count++; + } +} + +int test_blocking_remote_task_activation(env_t env) +{ + seL4_CPtr ep = vka_alloc_endpoint_leaky(&env->vka); + seL4_CPtr ntfn = vka_alloc_notification_leaky(&env->vka); + seL4_CPtr reply = vka_alloc_reply_leaky(&env->vka); + + /* fine to use this cross core because of single-copy atomicity on an aligned (32-bit) variable */ + volatile int state = 0; + + /* make remote helper */ + helper_thread_t helper; + create_helper_thread(env, &helper); + set_helper_affinity(env, &helper, 1); + start_helper(env, &helper, (helper_fn_t)sched_context_smp_005_helper_fn, + (seL4_Word)&state, ntfn, ep, 0); + + /* wait like a whole second (at 1GHz) to start */ + wait_eq_timeout(&state, 1, 1 * NS_IN_S); + + /* test notification waking blocked remote */ + seL4_Signal(ntfn); + /* wait a bit for the next state */ + wait_eq_timeout(&state, 2, 1 * US_IN_S); + + /* test endpoint waking blocked remote */ + seL4_Send(ep, seL4_MessageInfo_new(0, 0, 0, 0)); + /* wait a bit for the next state */ + wait_eq_timeout(&state, 3, 1 * US_IN_S); + + (void)seL4_Recv(ep, NULL, reply); + + /* test reply waiting blocked remote */ + seL4_Send(reply, seL4_MessageInfo_new(0, 0, 0, 0)); + wait_eq_timeout(&state, 4, 1 * US_IN_S); + + cleanup_helper(env, &helper); + + return sel4test_get_result(); +} +DEFINE_TEST(SCHED_CONTEXT_SMP_005, "test activation of blocking remote tasks (call/reply/signal)", + test_blocking_remote_task_activation, config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 1)); From ad0e06ea1a69044e87013388568c8f1a73a0e1e2 Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Wed, 13 May 2026 16:58:44 +1000 Subject: [PATCH 14/21] Test core migrations triggerred by remote signals Signed-off-by: Julia Vassiliki --- .../src/tests/schedcontext_smp.c | 236 ++++++++++++++++++ 1 file changed, 236 insertions(+) diff --git a/apps/sel4test-tests/src/tests/schedcontext_smp.c b/apps/sel4test-tests/src/tests/schedcontext_smp.c index 9b07d0f3f..2536b8339 100644 --- a/apps/sel4test-tests/src/tests/schedcontext_smp.c +++ b/apps/sel4test-tests/src/tests/schedcontext_smp.c @@ -421,3 +421,239 @@ int test_blocking_remote_task_activation(env_t env) } DEFINE_TEST(SCHED_CONTEXT_SMP_005, "test activation of blocking remote tasks (call/reply/signal)", test_blocking_remote_task_activation, config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 1)); + +#define SC_SMP_006_EP 1 +#define SC_SMP_006_NTFN 2 + +int sched_context_smp_006_helper_fn(seL4_CPtr ep, seL4_CPtr reply, seL4_CPtr ntfn, seL4_CPtr tcb) +{ + seL4_Word sender; + + /* This ReplyRecv will cause passive server-ification */ + seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 0); + tag = seL4_ReplyRecv(ep, tag, &sender, reply); + test_eq(sender, SC_SMP_006_EP); + + test_eq(0, seL4_DebugGetThreadAffinity(tcb)); + + /* Now running on the SC of our `seL4_Call`er we signal our bound ntfn before + * ReplyRecv'ing */ + seL4_Signal(ntfn); + + /* After this we will be running on the notification SC on a different core */ + tag = seL4_ReplyRecv(ep, tag, &sender, reply); + test_eq(sender, SC_SMP_006_NTFN); + + test_eq(1, seL4_DebugGetThreadAffinity(tcb)); + + return sel4test_get_result(); +} + +int test_passive_remote_task_signal_migration_bound(env_t env) +{ + int error; + seL4_CPtr unbadged_ep = vka_alloc_endpoint_leaky(&env->vka); + seL4_CPtr unbadged_ntfn = vka_alloc_notification_leaky(&env->vka); + seL4_CPtr reply = vka_alloc_reply_leaky(&env->vka); + /* badge_endpoint does work for a ntfn too */ + seL4_CPtr ntfn = badge_endpoint(env, SC_SMP_006_NTFN, unbadged_ntfn); + seL4_CPtr ep = badge_endpoint(env, SC_SMP_006_EP, unbadged_ep); + + /* make helper */ + helper_thread_t helper; + create_helper_thread(env, &helper); + + /* make the helper (and the bound ntfn sc) run on the second core */ + set_helper_affinity(env, &helper, 1); + + /* setup a bound notification */ + error = seL4_TCB_BindNotification(get_helper_tcb(&helper), ntfn); + test_eq(error, seL4_NoError); + + /* do lazy rebind for passive */ + error = api_sc_bind(get_helper_sched_context(&helper), ntfn); + test_eq(error, seL4_NoError); + + /* set helper to higher prio so it runs until blocked above us. */ + set_helper_priority(env, &helper, env->priority + 1); + + start_helper(env, &helper, (helper_fn_t)sched_context_smp_006_helper_fn, + ep, reply, ntfn, get_helper_tcb(&helper)); + + /* Make it run on our core and then continue with migration via signal on self */ + seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 0); + tag = seL4_Call(ep, tag); + + error = wait_for_helper(&helper); + test_eq(error, seL4_NoError); + + cleanup_helper(env, &helper); + + return sel4test_get_result(); +} +DEFINE_TEST(SCHED_CONTEXT_SMP_006, "signal on bound notification causing core migration passive task (current task)", + test_passive_remote_task_signal_migration_bound, config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 1)); + +int sched_context_smp_007_helper_fn(seL4_CPtr ep, seL4_CPtr reply, seL4_CPtr ntfn, seL4_CPtr tcb) +{ + seL4_Word sender; + + /* This ReplyRecv will cause passive server-ification */ + seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 0); + tag = seL4_ReplyRecv(ep, tag, &sender, reply); + test_eq(sender, SC_SMP_006_EP); + + test_eq(0, seL4_DebugGetThreadAffinity(tcb)); + + seL4_Signal(ntfn); + /* wait on the notification as an alternative to bound notification ep wait */ + seL4_Wait(ntfn, NULL); + + test_eq(1, seL4_DebugGetThreadAffinity(tcb)); + + return sel4test_get_result(); +} + +int test_passive_remote_task_signal_migration_wait(env_t env) +{ + int error; + seL4_CPtr unbadged_ep = vka_alloc_endpoint_leaky(&env->vka); + seL4_CPtr unbadged_ntfn = vka_alloc_notification_leaky(&env->vka); + seL4_CPtr reply = vka_alloc_reply_leaky(&env->vka); + /* badge_endpoint does work for a ntfn too */ + seL4_CPtr ntfn = badge_endpoint(env, SC_SMP_006_NTFN, unbadged_ntfn); + seL4_CPtr ep = badge_endpoint(env, SC_SMP_006_EP, unbadged_ep); + + /* make helper */ + helper_thread_t helper; + create_helper_thread(env, &helper); + + /* make the helper (and the bound ntfn sc) run on the second core */ + set_helper_affinity(env, &helper, 1); + + /* setup a bound notification */ + error = seL4_TCB_BindNotification(get_helper_tcb(&helper), ntfn); + test_eq(error, seL4_NoError); + + /* do lazy rebind for passive */ + error = api_sc_bind(get_helper_sched_context(&helper), ntfn); + test_eq(error, seL4_NoError); + + /* set helper to higher prio so it runs until blocked above us. */ + set_helper_priority(env, &helper, env->priority + 1); + + start_helper(env, &helper, (helper_fn_t)sched_context_smp_007_helper_fn, + ep, reply, ntfn, get_helper_tcb(&helper)); + + /* Make it run on our core and then continue with migration via signal on self */ + seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 0); + tag = seL4_Call(ep, tag); + + error = wait_for_helper(&helper); + test_eq(error, seL4_NoError); + + cleanup_helper(env, &helper); + + return sel4test_get_result(); +} +DEFINE_TEST(SCHED_CONTEXT_SMP_007, "signal causing (seL4_Wait) core migration current passive task", + test_passive_remote_task_signal_migration_wait, config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 1)); + +int sched_context_smp_008_helper_fn(seL4_CPtr ep, seL4_CPtr reply, seL4_CPtr ntfn_to_helper, seL4_CPtr tcb) +{ + seL4_Word sender; + + /* Tell helper 2 we're ready and also do passive server-ification */ + seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 0); + tag = seL4_NBSendRecv(ntfn_to_helper, tag, ep, NULL, reply); + + /* now running on core 2 (helper 2's core) */ + test_eq(2, seL4_DebugGetThreadAffinity(tcb)); + + /* respond to helper 2 and wait for the notification from core 0 */ + tag = seL4_ReplyRecv(ep, tag, &sender, reply); + test_eq(sender, SC_SMP_006_NTFN); + + test_eq(1, seL4_DebugGetThreadAffinity(tcb)); + + return sel4test_get_result(); +} + +int sched_context_smp_008_core2_helper_fn(seL4_CPtr ep, seL4_CPtr ntfn_from_helper) +{ + /* wait for the other helper to be ready - so that when it does the + * passive server Recv() it goes into a blocked state, instead of immediately + * progressing as this helper already made the ep into a send state */ + seL4_Wait(ntfn_from_helper, NULL); + + seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 0); + /* Call helper 1 and make it migrate to core 2 */ + (void)seL4_Call(ep, tag); + /* die */ + return 0; +} + +int test_passive_remote_task_migration(env_t env) +{ + int error; + seL4_CPtr unbadged_ep = vka_alloc_endpoint_leaky(&env->vka); + seL4_CPtr unbadged_ntfn = vka_alloc_notification_leaky(&env->vka); + seL4_CPtr reply = vka_alloc_reply_leaky(&env->vka); + /* badge_endpoint does work for a ntfn too */ + seL4_CPtr ntfn = badge_endpoint(env, SC_SMP_006_NTFN, unbadged_ntfn); + seL4_CPtr ep = badge_endpoint(env, SC_SMP_006_EP, unbadged_ep); + seL4_CPtr ntfn_between_helpers = vka_alloc_notification_leaky(&env->vka); + + /* make helper */ + helper_thread_t helper_1, helper_2; + create_helper_thread(env, &helper_1); + create_helper_thread(env, &helper_2); + + /* make the bound ntfn sc (and initial server setup) run on the second core */ + set_helper_affinity(env, &helper_1, 1); + set_helper_affinity(env, &helper_2, 2); + + /* setup a bound notification */ + error = seL4_TCB_BindNotification(get_helper_tcb(&helper_1), ntfn); + test_eq(error, seL4_NoError); + + /* do lazy rebind for passive */ + error = api_sc_bind(get_helper_sched_context(&helper_1), ntfn); + test_eq(error, seL4_NoError); + + /** + * Situation at start: + * + * Core 0: Core 1: Core 2 + * test program helper 1 (blocked on signal) helper 2 (that calls 1) + * + * Helper 1/2 run; helper 2 blocks waiting for helper 1 to NBSendRecv. + * This means helper 2 passive-server-ifies before helper 2 runs. + * Helper 2 performs seL4_Call(helper 1). This causes helper 1 to run + * on core 2. Then helper 1 rplies to helper 2, which tells core 0 to signal + * helper 1 and cause a migration to core 1. + * + **/ + + start_helper(env, &helper_1, (helper_fn_t)sched_context_smp_008_helper_fn, + ep, reply, ntfn_between_helpers, get_helper_tcb(&helper_1)); + start_helper(env, &helper_2, (helper_fn_t)sched_context_smp_008_core2_helper_fn, + ep, ntfn_between_helpers, 0, 0); + + /* wait for helper 2 to start and die */ + error = wait_for_helper(&helper_2); + test_eq(error, seL4_NoError); + + seL4_Signal(ntfn); + + /* wait for helper to die */ + error = wait_for_helper(&helper_1); + test_eq(error, seL4_NoError); + + cleanup_helper(env, &helper_1); + cleanup_helper(env, &helper_2); + + return sel4test_get_result(); +} +DEFINE_TEST(SCHED_CONTEXT_SMP_008, "signal on bound notification remote task causing core migration (two remote cores)", + test_passive_remote_task_migration, config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 2)); From 67f3684618b6ce4645780d05323bcab0f2e169ba Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Wed, 13 May 2026 17:15:07 +1000 Subject: [PATCH 15/21] SCHED0026: SchedControl_Configure/SetAffinity remote tasks work Signed-off-by: Julia Vassiliki --- apps/sel4test-tests/src/tests/scheduler.c | 63 +++++++++++++++++++++++ 1 file changed, 63 insertions(+) diff --git a/apps/sel4test-tests/src/tests/scheduler.c b/apps/sel4test-tests/src/tests/scheduler.c index 3740c7dbb..54f056d6b 100644 --- a/apps/sel4test-tests/src/tests/scheduler.c +++ b/apps/sel4test-tests/src/tests/scheduler.c @@ -1825,3 +1825,66 @@ int test_yieldTo_remote(env_t env) } DEFINE_TEST(SCHED0025, "Test seL4_SchedContext_YieldTo remote", test_yieldTo_remote, config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 1)); + +void sched_0026_helper_fn(volatile uint64_t *counter, seL4_CPtr ntfn) +{ + /* tell server we started */ + seL4_Signal(ntfn); + + /* Infinitely loop taking up budget */ + while (true) { + *counter += 1; + } +} + +/* Test moving a helper thread between remote cores */ +static int test_changing_affinity_remote(struct env *env) +{ + int error; + helper_thread_t helper; + seL4_CPtr ntfn; + volatile uint64_t counter = 0; + + ntfn = vka_alloc_notification_leaky(&env->vka); + create_helper_thread(env, &helper); + + /* make the budget/period such that only 1 timer interrupt per hour is required, + * so that the helper should never enter the kernel unnecessarily + * as we don't need round robin. */ + error = set_helper_sched_params(env, &helper, 3600 * US_IN_S, 3600 * US_IN_S, 0); + test_eq(error, seL4_NoError); + + /* start on core 1 */ + set_helper_affinity(env, &helper, 1); + + start_helper(env, &helper, (helper_fn_t)sched_0026_helper_fn, (seL4_Word)&counter, ntfn, 0, 0); + + /* wait for it to start helper */ + seL4_Wait(ntfn, NULL); + + for (volatile int i = 0; i < 1000; i++) { } + + uint64_t local_count_0 = counter; + /* it should have run some amount */ + test_gt(local_count_0, 0); + + /* move remote task to another remote core */ + set_helper_affinity(env, &helper, 2); + + uint64_t local_count_1 = counter; + /* should have incremented some more */ + test_gt(local_count_1, local_count_0); + + for (volatile int i = 0; i < 1000; i++) { } + + /* it should still be incrementing */ + uint64_t local_count_2 = counter; + /* should have incremented some more */ + test_gt(local_count_2, local_count_1); + + cleanup_helper(env, &helper); + + return sel4test_get_result(); +} +DEFINE_TEST(SCHED0026, "test migrating remote tasks", test_changing_affinity_remote, + (CONFIG_MAX_NUM_NODES > 2)); From 220bdb2a3aec02a9e3217f36ef9d6481e2194119 Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Wed, 13 May 2026 17:45:17 +1000 Subject: [PATCH 16/21] SCHED_CONTEXT_SMP_009: take away budget Signed-off-by: Julia Vassiliki --- .../src/tests/schedcontext_smp.c | 85 +++++++++++++++++++ 1 file changed, 85 insertions(+) diff --git a/apps/sel4test-tests/src/tests/schedcontext_smp.c b/apps/sel4test-tests/src/tests/schedcontext_smp.c index 2536b8339..7e13adc42 100644 --- a/apps/sel4test-tests/src/tests/schedcontext_smp.c +++ b/apps/sel4test-tests/src/tests/schedcontext_smp.c @@ -657,3 +657,88 @@ int test_passive_remote_task_migration(env_t env) } DEFINE_TEST(SCHED_CONTEXT_SMP_008, "signal on bound notification remote task causing core migration (two remote cores)", test_passive_remote_task_migration, config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 2)); + +void sc_smp_009_helper_fn(volatile uint64_t *counter, seL4_CPtr ntfn) +{ + /* tell remote we are started now */ + seL4_Signal(ntfn); + + /* Infinitely loop taking up budget */ + while (true) { + *counter += 1; + } +} + +int test_update_remote_sc_with_no_budget(env_t env) +{ + + /** + * Idea behind this: a remote thread might have run out of a budget. + * If we make a remote thread that has a tiny budget (the minimum) + * but a very long period (the maximum) then once it will runout it will + * basically never refill: so, if we reconfigure the SC to have full + * bandwidth (budget = period) then it should start running again. + **/ + + int error; + helper_thread_t helper; + volatile uint64_t counter = 0; + seL4_CPtr ntfn; + + ntfn = vka_alloc_notification_leaky(&env->vka); + create_helper_thread(env, &helper); + + /* give the helper infinite budget */ + error = seL4_SchedControl_Configure( + /* schedcontrol */ simple_get_sched_ctrl(&env->simple, 1), + /* schedcontext */ get_helper_sched_context(&helper), + /* budget */ MAX_PERIOD_US, /* period */ MAX_PERIOD_US, /* refills */ 0, /* badge */ 0); + ZF_LOGF_IF(error, "should be able to configure SC"); + + start_helper(env, &helper, (helper_fn_t)sc_smp_009_helper_fn, (seL4_Word)&counter, ntfn, 0, 0); + + /* wait for it to tell us it is ready */ + seL4_Wait(ntfn, NULL); + + /* wait a little while for the other core to run */ + for (volatile int i = 0; i < 1000; i++) { } + + uint64_t local_count_0 = counter; + test_gt(local_count_0, 0); + + /* remove the remote helper's budget. it should stop counting immediately. + specifically: since it has infinite budget if we don't make it stop rather + quickly then it means it kept going. the idea is that if we don't stall + the remote TCB it will continue to run and never need to drop back into + the kernel as no timer interrupts are scheduled for over an hour. */ + error = seL4_SchedControl_Configure( + /* schedcontrol */ simple_get_sched_ctrl(&env->simple, 1), + /* schedcontext */ get_helper_sched_context(&helper), + /* budget */ MIN_BUDGET_US, /* period */ MAX_PERIOD_US, /* refills */ 0, /* badge */ 0); + test_error_eq(error, seL4_NoError); + + uint64_t local_count_1 = counter; + test_gt(local_count_1, local_count_0); + + /* wait a little while for the core to run and expire its budget */ + // TODO: do it with a timeout fault? + for (volatile int i = 0; i < 1000000; i++) { } + + uint64_t local_count_2 = counter; + if (local_count_2 == local_count_1) { + /* already might have stopped pre the 1000000 wait */ + goto skip; + } + /* wait a bit more and see what happens */ + for (volatile int i = 0; i < 1000; i++) { } + + uint64_t local_count_3 = counter; + test_gt(local_count_3, local_count_2); + +skip: + cleanup_helper(env, &helper); + + return sel4test_get_result(); +} +DEFINE_TEST(SCHED_CONTEXT_SMP_009, "update a remote task's SC to remove budget to run immediately.", + test_update_remote_sc_with_no_budget, config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 1)); From 1b94e27c6ef6210526f01eba91a63dbef386fd70 Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Wed, 13 May 2026 17:45:29 +1000 Subject: [PATCH 17/21] SCHED0023: test also lowering Signed-off-by: Julia Vassiliki --- apps/sel4test-tests/src/tests/scheduler.c | 25 ++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/apps/sel4test-tests/src/tests/scheduler.c b/apps/sel4test-tests/src/tests/scheduler.c index 54f056d6b..571e9ae3a 100644 --- a/apps/sel4test-tests/src/tests/scheduler.c +++ b/apps/sel4test-tests/src/tests/scheduler.c @@ -1740,9 +1740,32 @@ static int test_set_higher_prio_remote(struct env *env) seL4_Wait(ntfn, NULL); test_eq(state, 2); + /* ==== part 2: lowering instead of raising */ + + /* reset the priorities and state */ + state = 0; + set_helper_priority(env, &high_thread, 3); + set_helper_priority(env, &low_thread, 2); + + /* restart the low function */ + start_helper(env, &low_thread, (helper_fn_t) sched_0023_helper_low_fn, (seL4_Word)&state, ntfn, 0, 0); + + /* check that the low function hasn't run and update the state */ + test_eq(state, 0); + + /* lower the prio of high below low*/ + set_helper_priority(env, &high_thread, 1); + + /* helper should run and set state to 2 */ + seL4_Wait(ntfn, NULL); + test_eq(state, 2); + + cleanup_helper(env, &high_thread); + cleanup_helper(env, &low_thread); + return sel4test_get_result(); } -DEFINE_TEST(SCHED0023, "test set prio to a higher prio runs higher prio thread remote core", +DEFINE_TEST(SCHED0023, "test set prio to higher/lower on remote core", test_set_higher_prio, (CONFIG_MAX_NUM_NODES > 1)); void sched_0024_helper_fn(volatile int *state, seL4_CPtr ntfn) From 4ba30655a5fa726a988c9d0104ace25645f236a7 Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Thu, 14 May 2026 10:48:05 +1000 Subject: [PATCH 18/21] SCHED_CONTEXT_SMP_009: use timeout fault Signed-off-by: Julia Vassiliki --- .../src/tests/schedcontext_smp.c | 45 +++++++------------ 1 file changed, 16 insertions(+), 29 deletions(-) diff --git a/apps/sel4test-tests/src/tests/schedcontext_smp.c b/apps/sel4test-tests/src/tests/schedcontext_smp.c index 7e13adc42..ce2366c54 100644 --- a/apps/sel4test-tests/src/tests/schedcontext_smp.c +++ b/apps/sel4test-tests/src/tests/schedcontext_smp.c @@ -658,15 +658,15 @@ int test_passive_remote_task_migration(env_t env) DEFINE_TEST(SCHED_CONTEXT_SMP_008, "signal on bound notification remote task causing core migration (two remote cores)", test_passive_remote_task_migration, config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 2)); -void sc_smp_009_helper_fn(volatile uint64_t *counter, seL4_CPtr ntfn) +void sc_smp_009_helper_fn(seL4_CPtr ntfn) { /* tell remote we are started now */ seL4_Signal(ntfn); /* Infinitely loop taking up budget */ while (true) { - *counter += 1; - } + asm volatile("nop" ::: "memory"); + }; } int test_update_remote_sc_with_no_budget(env_t env) @@ -682,10 +682,15 @@ int test_update_remote_sc_with_no_budget(env_t env) int error; helper_thread_t helper; - volatile uint64_t counter = 0; seL4_CPtr ntfn; + seL4_CPtr timeout_ep; + seL4_CPtr timeout_reply; + seL4_MessageInfo_t tag; ntfn = vka_alloc_notification_leaky(&env->vka); + timeout_ep = vka_alloc_endpoint_leaky(&env->vka); + timeout_reply = vka_alloc_reply_leaky(&env->vka); + create_helper_thread(env, &helper); /* give the helper infinite budget */ @@ -695,17 +700,14 @@ int test_update_remote_sc_with_no_budget(env_t env) /* budget */ MAX_PERIOD_US, /* period */ MAX_PERIOD_US, /* refills */ 0, /* badge */ 0); ZF_LOGF_IF(error, "should be able to configure SC"); - start_helper(env, &helper, (helper_fn_t)sc_smp_009_helper_fn, (seL4_Word)&counter, ntfn, 0, 0); + /* configure a timeout EP so we know when it's budget expire s*/ + set_helper_tfep(env, &helper, timeout_ep); + + start_helper(env, &helper, (helper_fn_t)sc_smp_009_helper_fn, ntfn, 0, 0, 0); /* wait for it to tell us it is ready */ seL4_Wait(ntfn, NULL); - /* wait a little while for the other core to run */ - for (volatile int i = 0; i < 1000; i++) { } - - uint64_t local_count_0 = counter; - test_gt(local_count_0, 0); - /* remove the remote helper's budget. it should stop counting immediately. specifically: since it has infinite budget if we don't make it stop rather quickly then it means it kept going. the idea is that if we don't stall @@ -717,25 +719,10 @@ int test_update_remote_sc_with_no_budget(env_t env) /* budget */ MIN_BUDGET_US, /* period */ MAX_PERIOD_US, /* refills */ 0, /* badge */ 0); test_error_eq(error, seL4_NoError); - uint64_t local_count_1 = counter; - test_gt(local_count_1, local_count_0); - - /* wait a little while for the core to run and expire its budget */ - // TODO: do it with a timeout fault? - for (volatile int i = 0; i < 1000000; i++) { } - - uint64_t local_count_2 = counter; - if (local_count_2 == local_count_1) { - /* already might have stopped pre the 1000000 wait */ - goto skip; - } - /* wait a bit more and see what happens */ - for (volatile int i = 0; i < 1000; i++) { } - - uint64_t local_count_3 = counter; - test_gt(local_count_3, local_count_2); + tag = seL4_Recv(timeout_ep, NULL, timeout_reply); + seL4_Fault_t fault = seL4_getFault(tag); + test_eq(seL4_Fault_get_seL4_FaultType(fault), seL4_Fault_Timeout); -skip: cleanup_helper(env, &helper); return sel4test_get_result(); From 0381ecb93e686cf4d9993ea30da74468ec0b2498 Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Thu, 14 May 2026 11:12:06 +1000 Subject: [PATCH 19/21] define mcs tests only on mcs Signed-off-by: Julia Vassiliki --- apps/sel4test-tests/src/tests/schedcontext_smp.c | 4 ++++ apps/sel4test-tests/src/tests/scheduler.c | 4 +++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/apps/sel4test-tests/src/tests/schedcontext_smp.c b/apps/sel4test-tests/src/tests/schedcontext_smp.c index ce2366c54..8c2b30456 100644 --- a/apps/sel4test-tests/src/tests/schedcontext_smp.c +++ b/apps/sel4test-tests/src/tests/schedcontext_smp.c @@ -28,6 +28,8 @@ #endif #endif +#ifdef CONFIG_KERNEL_MCS + static inline seL4_CPtr badge_endpoint(env_t env, seL4_Word badge, seL4_CPtr ep) { seL4_CPtr slot = get_free_slot(env); @@ -729,3 +731,5 @@ int test_update_remote_sc_with_no_budget(env_t env) } DEFINE_TEST(SCHED_CONTEXT_SMP_009, "update a remote task's SC to remove budget to run immediately.", test_update_remote_sc_with_no_budget, config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 1)); + +#endif /* CONFIG_KERNEL_MCS */ diff --git a/apps/sel4test-tests/src/tests/scheduler.c b/apps/sel4test-tests/src/tests/scheduler.c index 571e9ae3a..6d05de11a 100644 --- a/apps/sel4test-tests/src/tests/scheduler.c +++ b/apps/sel4test-tests/src/tests/scheduler.c @@ -1816,6 +1816,7 @@ static int test_resume_suspended_remote_task(struct env *env) DEFINE_TEST(SCHED0024, "test resuming a suspended remote task", test_resume_suspended_remote_task, (CONFIG_MAX_NUM_NODES > 1)); +#ifdef CONFIG_KERNEL_MCS int test_yieldTo_remote(env_t env) { int error; @@ -1848,6 +1849,7 @@ int test_yieldTo_remote(env_t env) } DEFINE_TEST(SCHED0025, "Test seL4_SchedContext_YieldTo remote", test_yieldTo_remote, config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 1)); +#endif /* CONFIG_KERNEL_MCS */ void sched_0026_helper_fn(volatile uint64_t *counter, seL4_CPtr ntfn) { @@ -1910,4 +1912,4 @@ static int test_changing_affinity_remote(struct env *env) return sel4test_get_result(); } DEFINE_TEST(SCHED0026, "test migrating remote tasks", test_changing_affinity_remote, - (CONFIG_MAX_NUM_NODES > 2)); + config_set(CONFIG_KERNEL_MCS) && (CONFIG_MAX_NUM_NODES > 2)); From 8218c59679d11045429553a30141fa8e1ffb9dbf Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Thu, 14 May 2026 14:17:12 +1000 Subject: [PATCH 20/21] fix SCHED_CONTEXT_SMP_007 Signed-off-by: Julia Vassiliki --- apps/sel4test-tests/src/tests/schedcontext_smp.c | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/apps/sel4test-tests/src/tests/schedcontext_smp.c b/apps/sel4test-tests/src/tests/schedcontext_smp.c index 8c2b30456..13b7c86b9 100644 --- a/apps/sel4test-tests/src/tests/schedcontext_smp.c +++ b/apps/sel4test-tests/src/tests/schedcontext_smp.c @@ -500,6 +500,9 @@ int sched_context_smp_007_helper_fn(seL4_CPtr ep, seL4_CPtr reply, seL4_CPtr ntf { seL4_Word sender; + /* we start running on the SC of the notification, i.e. core 1 */ + test_eq(1, seL4_DebugGetThreadAffinity(tcb)); + /* This ReplyRecv will cause passive server-ification */ seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 0); tag = seL4_ReplyRecv(ep, tag, &sender, reply); @@ -508,8 +511,9 @@ int sched_context_smp_007_helper_fn(seL4_CPtr ep, seL4_CPtr reply, seL4_CPtr ntf test_eq(0, seL4_DebugGetThreadAffinity(tcb)); seL4_Signal(ntfn); - /* wait on the notification as an alternative to bound notification ep wait */ - seL4_Wait(ntfn, NULL); + + /* reply (to donate away our SC) and then wait on our notification */ + tag = seL4_NBSendWait(reply, tag, ntfn, NULL); test_eq(1, seL4_DebugGetThreadAffinity(tcb)); From 1b0975297bbf7004f259aa7b19d2cf2402eda50c Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Tue, 14 Jul 2026 11:48:44 +1000 Subject: [PATCH 21/21] increase wait time as this sometimes fails Running test SCHED0026 (test migrating remote tasks) Error: Check local_count_2(44446) > local_count_1(44446) failed. Signed-off-by: Julia Vassiliki --- apps/sel4test-tests/src/tests/scheduler.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/apps/sel4test-tests/src/tests/scheduler.c b/apps/sel4test-tests/src/tests/scheduler.c index 6d05de11a..168f9aeda 100644 --- a/apps/sel4test-tests/src/tests/scheduler.c +++ b/apps/sel4test-tests/src/tests/scheduler.c @@ -1887,7 +1887,7 @@ static int test_changing_affinity_remote(struct env *env) /* wait for it to start helper */ seL4_Wait(ntfn, NULL); - for (volatile int i = 0; i < 1000; i++) { } + for (volatile int i = 0; i < 100000; i++) { } uint64_t local_count_0 = counter; /* it should have run some amount */ @@ -1900,7 +1900,7 @@ static int test_changing_affinity_remote(struct env *env) /* should have incremented some more */ test_gt(local_count_1, local_count_0); - for (volatile int i = 0; i < 1000; i++) { } + for (volatile int i = 0; i < 100000; i++) { } /* it should still be incrementing */ uint64_t local_count_2 = counter;