Skip to content

Commit

Permalink
scheduler: resume does preempt
Browse files Browse the repository at this point in the history
If we're seeing failures on this test, they need to be investigated. The
resume invocation is definitely supposed to call the scheduler and leave
with the highest priority thread running.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
  • Loading branch information
lsf37 committed Jul 12, 2024
1 parent 17cac54 commit fe4839e
Showing 1 changed file with 0 additions and 8 deletions.
8 changes: 0 additions & 8 deletions apps/sel4test-tests/src/tests/scheduler.c
Original file line number Diff line number Diff line change
Expand Up @@ -182,14 +182,6 @@ static int suspend_test_helper_1(seL4_CPtr t1, seL4_CPtr t2a, seL4_CPtr t2b)

/* We should have been preempted immediately, so by the time we run again,
* the suspend_test_step should be 5. */

#if 1 // WE HAVE A BROKEN SCHEDULER IN SEL4
/* FIXME: The seL4 scheduler is broken, and seL4_TCB_Resume will not
* preempt. The only way to get preempted is to force it ourselves (or wait
* for a timer tick). */
seL4_Yield();
#endif

CHECK_STEP(suspend_test_step, 5);

return sel4test_get_result();
Expand Down

0 comments on commit fe4839e

Please sign in to comment.