search

seL4 / sel4test

Test suite for seL4.
http://sel4.systems
Other
25 stars 63 forks source link

Add test for race in seL4 issue 633 #56

Closed Indanz closed 3 years ago

Indanz commented 3 years ago

This triggers a race between scheduling context deletion and the out of budget timer IRQ. This test is very timing sensitive, it is known to trigger the race condition on tqma8xqp1gb with RELEASE disabled.

Also add MIN_BUDGET tests. This assumes WCET is at most 10us on all tested platforms!

Indanz commented 3 years ago

This depends on https://github.com/seL4/seL4/pull/634 being merged, otherwise it will trigger an assertion.

Indanz commented 3 years ago

This should run on real hardware before being merged. Hopefully it triggers the same bug on another platform than tqma8xqp1gb, so we have an extra way to test whatever fix we do.

lsf37 commented 3 years ago

Cool, thanks for this. I'll see if I can find a platform that triggers this.

lsf37 commented 3 years ago

Interestingly ia32 triggers the assertion failure, but none of the other Arm platforms in the test so far (tx2 is still running). But that is good enough to confirm its absence after the fix and to catch it should it re-occur.

(edit: it does trigger on tx2 as well, so there are two platforms that show the problem)