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

mcs: Defer charging budget in preempted invocation

Browse source 
Rather than charge consumed time to the current thread at the point
where it is exhausted in a long-running syscall, we only check whether
checkBudget would fail and raise an exception if it would. We then
always charge after handleInvocation rather than avoid-double charging.

This is done as it is easier to add the exhaustion case in the abstract
spec in this manner (without also adding changes to the current SC).

Signed-off-by: Curtis Millar <curtis@curtism.me>
This commit is contained in:
Curtis Millar 2020-11-06 08:48:45 +11:00 committed by Curtis Millar
parent 0647a84c32
commit 8373f0a0a6
3 changed files with 17 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
include/kernel/thread.h
View file

@ -237,6 +237,16 @@ static inline void updateTimestamp(void)
NODE_STATE(ksConsumed) += (NODE_STATE(ksCurTime) - prev);
}
/* 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.
@ -249,13 +259,7 @@ static inline bool_t checkBudget(void)
/* currently running thread must have available capacity */
assert(refill_ready(NODE_STATE(ksCurSC)));
ticks_t capacity = refill_capacity(NODE_STATE(ksCurSC), NODE_STATE(ksConsumed));
/* 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. */
if (likely(capacity >= MIN_BUDGET && (isRoundRobin(NODE_STATE(ksCurSC)) ||
!refill_full(NODE_STATE(ksCurSC))))) {
if (likely(isSufficientAndSplittable())) {
if (unlikely(isCurDomainExpired())) {
NODE_STATE(ksReprogram) = true;
rescheduleRequired();

10
src/api/syscall.c
View file

@ -629,8 +629,8 @@ exception_t handleSyscall(syscall_t syscall)
ret = handleInvocation(false, true, false, false, getRegister(NODE_STATE(ksCurThread), capRegister));
if (unlikely(ret != EXCEPTION_NONE)) {
irq = getActiveIRQ();
mcsIRQ(irq);
if (IRQT_TO_IRQ(irq) != IRQT_TO_IRQ(irqInvalid)) {
mcsIRQ(irq);
handleInterrupt(irq);
Arch_finaliseInterrupt();
}
@ -642,8 +642,8 @@ exception_t handleSyscall(syscall_t syscall)
ret = handleInvocation(false, false, false, false, getRegister(NODE_STATE(ksCurThread), capRegister));
if (unlikely(ret != EXCEPTION_NONE)) {
irq = getActiveIRQ();
mcsIRQ(irq);
if (IRQT_TO_IRQ(irq) != IRQT_TO_IRQ(irqInvalid)) {
mcsIRQ(irq);
handleInterrupt(irq);
Arch_finaliseInterrupt();
}
@ -654,8 +654,8 @@ exception_t handleSyscall(syscall_t syscall)
ret = handleInvocation(true, true, true, false, getRegister(NODE_STATE(ksCurThread), capRegister));
if (unlikely(ret != EXCEPTION_NONE)) {
irq = getActiveIRQ();
mcsIRQ(irq);
if (IRQT_TO_IRQ(irq) != IRQT_TO_IRQ(irqInvalid)) {
mcsIRQ(irq);
handleInterrupt(irq);
Arch_finaliseInterrupt();
}
@ -697,8 +697,8 @@ exception_t handleSyscall(syscall_t syscall)
ret = handleInvocation(false, false, true, true, dest);
if (unlikely(ret != EXCEPTION_NONE)) {
irq = getActiveIRQ();
mcsIRQ(irq);
if (IRQT_TO_IRQ(irq) != IRQT_TO_IRQ(irqInvalid)) {
mcsIRQ(irq);
handleInterrupt(irq);
Arch_finaliseInterrupt();
}
@ -712,8 +712,8 @@ exception_t handleSyscall(syscall_t syscall)
ret = handleInvocation(false, false, true, true, getRegister(NODE_STATE(ksCurThread), replyRegister));
if (unlikely(ret != EXCEPTION_NONE)) {
irq = getActiveIRQ();
mcsIRQ(irq);
if (IRQT_TO_IRQ(irq) != IRQT_TO_IRQ(irqInvalid)) {
mcsIRQ(irq);
handleInterrupt(irq);
Arch_finaliseInterrupt();
}

2
src/model/preemption.c
View file

@ -33,7 +33,7 @@ exception_t preemptionPoint(void)
#ifdef CONFIG_KERNEL_MCS
} else {
updateTimestamp();
if (!(sc_active(NODE_STATE(ksCurSC)) && checkBudget())) {
if (!(sc_active(NODE_STATE(ksCurSC)) && isSufficientAndSplittable()) || isCurDomainExpired()) {
return EXCEPTION_PREEMPTED;
}
#endif