Unexpected behaviour with minimum budget

[Ivan-Velickovic]

Reported by @lsf37 and @alainkaegi.

Having a PD with minimum budget (20us) on the Odroid-C4 seems to never make progress. Setting budget=21 fixes it somehow. This setup couldn't be reproduced within sel4test, so it could be an issue with Microkit.

More investigation required, need to test other platforms etc to see if it's a general problem or somehow isolated to Odroid-C4.

[lsf37]

It doesn't seem to matter which period the thread is set to or what else runs in the system. I encountered the behaviour with experimental domain support on, but Alain had the same without domains.

In the setting I was trying out, the thread needed only about 8us to actually run before it yielded when the budget was set to 21, so it was not an issue of not being able to make enough progress within the 20us.

[Indanz]

It can actually be reproduced by sel4test, it's the same issue I ran into with seL4/sel4test#134, but the test is currently disabled in CI for the Odroid-C4.

It's high on my TODO list.

[lsf37]

Do you get it deterministically on sel4test? Because I'm sure I saw it working there when I tried to reproduce Alain's initial report.

Edit: a possible explanation is a difference in configs -- I would not have been using a hyp or smp config when trying to reproduce on sel4test, only MCS.

[Indanz]

Do you get it deterministically on sel4test? Because I'm sure I saw it working there when I tried to reproduce Alain's initial report.

I did for the tx2 before, and would be very surprised if it isn't failing either all the time or almost all the time on the Odroid too. Haven't gotten to it yet, hopefully Thursday.

Edit: a possible explanation is a difference in configs -- I would not have been using a hyp or smp config when trying to reproduce on sel4test, only MCS.

I've only seen it on SMP configs. That said, SCHED_CONTEXT_0014 only runs on SMP configs. Would be interesting to try to reproduce it on unicore.