sel4test
sel4test copied to clipboard
Test MULTICORE0005 fails on SABRE sporadically
After the merge of https://github.com/seL4/seL4/pull/712 the CI run https://github.com/seL4/seL4/actions/runs/1606856772 failed. The change in the merge seems quite unrelated.
Running test MULTICORE0005 (Test remote delete thread running on other cores)
<error>counter != old_counter at line 153 of file /github/workspace/projects/sel4test/apps/sel4test-tests/src/tests/multicore.c</error>
Test MULTICORE0005 failed
<failure type="failure">result == SUCCESS at line 291 of file /github/workspace/projects/sel4test/apps/sel4test-driver/src/testtypes.c</failure>
<error>result == SUCCESS at line 217 of file /github/workspace/projects/sel4test/apps/sel4test-driver/src/main.c</error>
The code is https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/src/tests/multicore.c#L143
volatile seL4_Word counter;
...
create_helper_thread(env, &t1);
...
old_counter = counter;
/* Let it run on the current core. */
sleep_busy(env, 10 * NS_IN_MS);
/* Now, counter should not have moved. */
test_check(counter == old_counter);
It's the second check that fails, on line 153:
/* Counter should have moved. */
test_check(counter != old_counter);
Does increasing the busy sleep from 10ms to something higher help? What is the timer tick interval for Sabre?