Skip to content

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

Open
midnightveil wants to merge 20 commits into
seL4:masterfrom
au-ts:julia/smp-migration
Open

Tests for https://github.com/seL4/seL4/issues/941#155
midnightveil wants to merge 20 commits into
seL4:masterfrom
au-ts:julia/smp-migration

Conversation

@midnightveil
Copy link
Copy Markdown
Contributor

@midnightveil midnightveil commented May 13, 2026

Depends on #123, which is merged in this branch.

Per seL4/seL4#941 (comment)

SchedContext_Bind on a TCB can give a task budget to run on another core.
    SCHED_CONTEXT_SMP_001
SchedContext_Bind on a signalled NF bound to a TCB can give a task budget to run on another core.
    SCHED_CONTEXT_SMP_003 but impossible due to https://github.com/seL4/seL4/issues/1617
SchedControl_Configure can migrate a task's SC to a different core (either the current task or another one).
    SCHED0022, every single test that calls set_helper_affinity
SchedControl_Configure can update a remote task's SC to have budget to run immediately.
    SCHED_CONTEXT_SMP_004
seL4_TCB_SetPriority can increase a remote task's priority.
    SCHED0023
A suspended remote task can be resumed.
    SCHED0024
seL4_SchedContext_YieldTo can give budget to a remote task.
    SCHED0025
A blocking remote task can be activated by a signal.
    SCHED_CONTEXT_SMP_005 (and many other tests)
A blocking remote task can be activated by a call.
    SCHED_CONTEXT_SMP_005 (and many other tests)
A blocking remote task can be activated by a reply.
    SCHED_CONTEXT_SMP_005 (and many other tests)
A blocking passive remote task can be activated by a signal, triggering core migration for the TCB.
    SCHED_CONTEXT_SMP_006/SCHED_CONTEXT_SMP_006/SCHED_CONTEXT_SMP_008
A blocking passive remote task can be activated by a call, triggering core migration for the TCB.
    IPC0028

seL4_SchedContext_Unbind and seL4_SchedContext_UnbindObject can take away a remote task's SC.
    SCHED_CONTEXT_SMP_010
SchedControl_Configure can migrate a remote task.
    SCHED0026
SchedControl_Configure can take away a remote task's budget.
    SCHED_CONTEXT_SMP_009
seL4_TCB_SetPriority can decrease a remote task's priority.
    SCHED0023
seL4_TCB_Suspend can suspend a remote task.
    SCHED0024
Remote task's TCB or SC objects can be destroyed.
    SCHED_CONTEXT_0014 already exists

Test with: seL4/seL4#1662

lsf37 and others added 18 commits May 7, 2026 16:34
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
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 <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
… is OK

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
'update a remote task's SC to have budget to run immediately.'

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
@midnightveil
Copy link
Copy Markdown
Contributor Author

midnightveil commented May 14, 2026

Note: simulation tests do not currently run either SMP or MCS configurations. I'm not sure why; I was testing with QEMU locally.

EDIT: probably because the ./simulate script won't generate the SMP flags to QEMU, actually... which Ivan did seL4/seL4_tools@80ae668 (#239).

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants