Hello Sam Myself and Gerwin attempted to get simulation platforms working with MCS for the CI and noticed that the MCS tests were not consistently passing. I don’t think it’s a bug with the kernel but rather to do with how QEMU emulates timers. There’s more details here: https://github.com/seL4/ci-actions/pull/233.
Ivan On 6/01/2023, at 5:13 AM, Sam Leffler via Devel <[email protected]<mailto:[email protected]>> wrote: We run sel4test regularly for a 64-bit raspi target under qemu and occasionally see failures like this: Starting test 129: TIMEOUTFAULT0003 Running test TIMEOUTFAULT0003 (Nested timeout fault) Error: Check badge(3) == expected_badge(2) failed. at line 9 This is a stock sel4test <https://github.com/AmbiML/sparrow-sel4test> + dep libs but an older kernel <https://github.com/AmbiML/sparrow-kernel>. Anyone know if this is an old (presumably fixed) bug or known issue? -Sam _______________________________________________ Devel mailing list -- [email protected]<mailto:[email protected]> To unsubscribe send an email to [email protected]<mailto:[email protected]> _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
