seL4/src/model
Anna Lyons 7c3b80d3ed mcs: check budget is sufficient in preemptionPoint
When we enter the kernel we know we have at least getKernelWcetUs
budget. Preemption points need to maintain this invariant and check
again.
2019-08-22 11:22:39 +10:00
..
preemption.c mcs: check budget is sufficient in preemptionPoint 2019-08-22 11:22:39 +10:00
smp.c [STYLE_FIX] 2017-08-23 02:57:42 +00:00
statedata.c mcs: configurable scheduling context size 2019-08-22 11:22:38 +10:00