portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

mcs: remove getKernelWcetTicks from refill_ready

Browse source 
Previously, a refill would be ready if its head time
was at most getKernelWcetTicks after the current time.
This would mean that refill_unblock_check could
bring a refill's time forward, which violates an
invariant (namely that the time of the last refill
is at most the period from the time of the head refill).

Moreover, since the time to exit the kernel is always
less than the WCET, this might result in us running
a thread whose refill time is in the future, which
seems to violate the timing model.

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
Michael McInerney 2023-02-02 17:22:30 +10:30 committed by Gerwin Klein
parent d8f4a95b72
commit 521f7e3c19
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
include/kernel/sporadic.h
View file

@ -126,7 +126,7 @@ static inline bool_t refill_sufficient(sched_context_t *sc, ticks_t usage)
*/
static inline bool_t refill_ready(sched_context_t *sc)
{
return refill_head(sc)->rTime <= (NODE_STATE(ksCurTime) + getKernelWcetTicks());
return refill_head(sc)->rTime <= NODE_STATE(ksCurTime);
}
/*