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

mcs: Remove refill_full check from checkBudget

Browse source 
A refill can still be charged if the refill list is full. This means
that we only require sufficient capacity to continue a timeslice.

Signed-off-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This commit is contained in:
Kent McLeod 2021-04-14 15:10:51 +10:00 committed by Curtis Millar
parent 4b519e8ccb
commit e2ca0b6119
2 changed files with 4 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
include/kernel/thread.h
View file

@ -242,16 +242,6 @@ static inline void updateTimestamp(void)
}
/* if the budget isn't enough, the timeslice for this SC is over. For
* round robin threads this is sufficient, however for periodic threads
* we also need to check there is space to schedule the replenishment - if the refill
* is full then the timeslice is also over as the rest of the budget is forfeit. */
static inline bool_t isSufficientAndSplittable(void)
{
return refill_sufficient(NODE_STATE(ksCurSC), NODE_STATE(ksConsumed)) && (isRoundRobin(NODE_STATE(ksCurSC))
|| !refill_full(NODE_STATE(ksCurSC)));
}
/* Check if the current thread/domain budget has expired.
* if it has, bill the thread, add it to the scheduler and
* set up a reschedule.
@ -264,7 +254,8 @@ static inline bool_t checkBudget(void)
/* currently running thread must have available capacity */
assert(refill_ready(NODE_STATE(ksCurSC)));
if (likely(isSufficientAndSplittable())) {
/* if the budget isn't enough, the timeslice for this SC is over. */
if (likely(refill_sufficient(NODE_STATE(ksCurSC), NODE_STATE(ksConsumed)))) {
if (unlikely(isCurDomainExpired())) {
return false;
}

3
src/model/preemption.c
View file

@ -30,7 +30,8 @@ exception_t preemptionPoint(void)
ksWorkUnitsCompleted = 0;
#ifdef CONFIG_KERNEL_MCS
updateTimestamp();
if (!(sc_active(NODE_STATE(ksCurSC)) && isSufficientAndSplittable()) || isCurDomainExpired() || isIRQPending()) {
if (!(sc_active(NODE_STATE(ksCurSC)) && refill_sufficient(NODE_STATE(ksCurSC), NODE_STATE(ksConsumed)))
|| isCurDomainExpired() || isIRQPending()) {
#else
if (isIRQPending()) {
#endif