diff --git a/include/kernel/sporadic.h b/include/kernel/sporadic.h
index af9a89d73..54d90a9a1 100644
--- a/include/kernel/sporadic.h
+++ b/include/kernel/sporadic.h
@@ -53,6 +53,11 @@ static inline word_t refill_size(sched_context_t *sc)
     return sc->scRefillTail + 1u + (sc->scRefillMax - sc->scRefillHead);
 }
 
+static inline bool_t refill_full(sched_context_t *sc)
+{
+    return refill_size(sc) == sc->scRefillMax;
+}
+
 static inline bool_t refill_single(sched_context_t *sc)
 {
     return sc->scRefillHead == sc->scRefillTail;
@@ -101,9 +106,8 @@ void refill_update(sched_context_t *sc, ticks_t new_period, ticks_t new_budget,
  * `used` amount from its current replenishment without
  * depleting the budget, i.e refill_expired returns false.
  *
- * return any uncharged usage.
  */
-ticks_t refill_budget_check(sched_context_t *sc, ticks_t used);
+void refill_budget_check(sched_context_t *sc, ticks_t used, ticks_t capacity);
 
 /*
  * Charge a scheduling context `used` amount from its
diff --git a/include/kernel/thread.h b/include/kernel/thread.h
index 646494661..cf5c3d92f 100644
--- a/include/kernel/thread.h
+++ b/include/kernel/thread.h
@@ -86,28 +86,42 @@ static inline bool_t isHighestPrio(word_t dom, prio_t prio)
 }
 
 #ifdef CONFIG_KERNEL_MCS
+static inline bool_t PURE isRoundRobin(sched_context_t *sc)
+{
+    return sc->scPeriod == 0;
+}
+
 static inline bool_t isCurDomainExpired(void)
 {
     return CONFIG_NUM_DOMAINS > 1 &&
-           ksDomainTime < (NODE_STATE(ksConsumed) + getKernelWcetTicks());
+           ksDomainTime < (NODE_STATE(ksConsumed) + MIN_BUDGET);
 }
 
 static inline void commitTime(void)
 {
-
-    if (likely(NODE_STATE(ksConsumed) > 0 && (NODE_STATE(ksCurThread) != NODE_STATE(ksIdleThread)))) {
+    if (likely(NODE_STATE(ksConsumed) > 0)) {
+        /* if this function is called the head refil must be sufficient to
+         * charge ksConsumed */
         assert(refill_sufficient(NODE_STATE(ksCurSC), NODE_STATE(ksConsumed)));
+        /* and it must be ready to use */
         assert(refill_ready(NODE_STATE(ksCurSC)));
-        refill_split_check(NODE_STATE(ksCurSC), NODE_STATE(ksConsumed));
+
+        if (isRoundRobin(NODE_STATE(ksCurSC))) {
+            /* for round robin threads, there are only two refills: the HEAD, which is what
+             * we are consuming, and the tail, which is what we have consumed */
+            assert(refill_size(NODE_STATE(ksCurSC)) == MIN_REFILLS);
+            REFILL_HEAD(NODE_STATE(ksCurSC)).rAmount -= NODE_STATE(ksConsumed);
+            REFILL_TAIL(NODE_STATE(ksCurSC)).rAmount += NODE_STATE(ksConsumed);
+        } else {
+            refill_split_check(NODE_STATE(ksCurSC), NODE_STATE(ksConsumed));
+        }
         assert(refill_sufficient(NODE_STATE(ksCurSC), 0));
         assert(refill_ready(NODE_STATE(ksCurSC)));
     }
     if (CONFIG_NUM_DOMAINS > 1) {
-        if (unlikely(ksDomainTime < NODE_STATE(ksConsumed))) {
-            ksDomainTime = 0;
-        } else {
-            ksDomainTime -= NODE_STATE(ksConsumed);
-        }
+        assert(ksDomainTime > NODE_STATE(ksConsumed));
+        assert(ksDomainTime - NODE_STATE(ksConsumed) >= MIN_BUDGET);
+        ksDomainTime -= NODE_STATE(ksConsumed);
     }
 
     NODE_STATE(ksConsumed) = 0llu;
@@ -171,6 +185,9 @@ static inline void updateRestartPC(tcb_t *tcb)
  */
 void endTimeslice(void);
 
+/* called when a thread has used up its head refill */
+void chargeBudget(ticks_t capacity, ticks_t consumed);
+
 /* Update the kernels timestamp and stores in ksCurTime.
  * The difference between the previous kernel timestamp and the one just read
  * is stored in ksConsumed.
@@ -199,31 +216,23 @@ static inline bool_t checkBudget(void)
     /* currently running thread must have available capacity */
     assert(refill_ready(NODE_STATE(ksCurSC)));
 
-    if (unlikely(NODE_STATE(ksCurThread) == NODE_STATE(ksIdleThread))) {
+    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 (unlikely(isCurDomainExpired())) {
+            commitTime();
+            rescheduleRequired();
+            return false;
+        }
         return true;
     }
 
-    ticks_t capacity = refill_capacity(NODE_STATE(ksCurSC), NODE_STATE(ksConsumed));
-    if (unlikely(capacity < MIN_BUDGET)) {
-        if (capacity == 0) {
-            NODE_STATE(ksConsumed) = refill_budget_check(NODE_STATE(ksCurSC), NODE_STATE(ksConsumed));
-        }
-        if (NODE_STATE(ksConsumed) > 0) {
-            refill_split_check(NODE_STATE(ksCurSC), NODE_STATE(ksConsumed));
-        }
-        NODE_STATE(ksConsumed) = 0;
-        NODE_STATE(ksCurTime) += 1llu;
-        if (likely(isRunnable(NODE_STATE(ksCurThread)))) {
-            endTimeslice();
-            rescheduleRequired();
-        }
-        return false;
-    } else if (unlikely(isCurDomainExpired())) {
-        commitTime();
-        rescheduleRequired();
-        return false;
-    }
-    return true;
+    chargeBudget(capacity, NODE_STATE(ksConsumed));
+    return false;
 }
 
 /* Everything checkBudget does, but also set the thread
diff --git a/src/api/syscall.c b/src/api/syscall.c
index da8125450..0229d6347 100644
--- a/src/api/syscall.c
+++ b/src/api/syscall.c
@@ -42,7 +42,6 @@ exception_t handleInterruptEntry(void)
     irq = getActiveIRQ();
 #ifdef CONFIG_KERNEL_MCS
     if (SMP_TERNARY(clh_is_self_in_queue(), 1)) {
-        assert(irq != irq_remote_call_ipi);
         updateTimestamp();
         checkBudget();
     }
@@ -60,7 +59,6 @@ exception_t handleInterruptEntry(void)
 
 #ifdef CONFIG_KERNEL_MCS
     if (SMP_TERNARY(clh_is_self_in_queue(), 1)) {
-        assert(irq != irq_remote_call_ipi);
 #endif
         schedule();
         activateThread();
@@ -534,14 +532,8 @@ static inline void mcsIRQ(irq_t irq)
 static void handleYield(void)
 {
 #ifdef CONFIG_KERNEL_MCS
-    /* checkBudgetRestart should have failed if we got here */
-    assert(refill_sufficient(NODE_STATE(ksCurSC), NODE_STATE(ksConsumed)));
     /* Yield the current remaining budget */
-    refill_budget_check(NODE_STATE(ksCurSC), REFILL_HEAD(NODE_STATE(ksCurSC)).rAmount);
-    /* we just charged all of the time to the yielding thread */
-    NODE_STATE(ksConsumed) = 0;
-    endTimeslice();
-    rescheduleRequired();
+    chargeBudget(0, REFILL_HEAD(NODE_STATE(ksCurSC)).rAmount);
 #else
     tcbSchedDequeue(NODE_STATE(ksCurThread));
     SCHED_APPEND_CURRENT_TCB;
diff --git a/src/kernel/sporadic.c b/src/kernel/sporadic.c
index 430537d56..eb9905c00 100644
--- a/src/kernel/sporadic.c
+++ b/src/kernel/sporadic.c
@@ -73,16 +73,21 @@ static UNUSED bool_t refill_ordered(sched_context_t *sc)
     word_t next = refill_next(sc, sc->scRefillHead);
 
     while (current != sc->scRefillTail) {
-        assert(REFILL_INDEX(sc, current).rTime <= REFILL_INDEX(sc, next).rTime);
+        if (!(REFILL_INDEX(sc, current).rTime <= REFILL_INDEX(sc, next).rTime)) {
+            refill_print(sc);
+            return false;
+        }
         current = next;
         next = refill_next(sc, current);
     }
+
+    return true;
 }
 
-#define REFILL_SANITY_START(sc) ticks_t _sum = refill_sum(sc); refill_ordered(sc);
+#define REFILL_SANITY_START(sc) ticks_t _sum = refill_sum(sc); assert(refill_ordered(sc));
 #define REFILL_SANITY_CHECK(sc, budget) \
     do { \
-        assert(refill_sum(sc) == budget); refill_ordered(sc); \
+        assert(refill_sum(sc) == budget); assert(refill_ordered(sc)); \
     } while (0)
 
 #define REFILL_SANITY_END(sc) \
@@ -96,7 +101,7 @@ static UNUSED bool_t refill_ordered(sched_context_t *sc)
 #endif /* CONFIG_DEBUG_BUILD */
 
 /* compute the sum of a refill queue */
-static ticks_t refill_sum(sched_context_t *sc)
+static UNUSED ticks_t refill_sum(sched_context_t *sc)
 {
     ticks_t sum = REFILL_HEAD(sc).rAmount;
     word_t current = sc->scRefillHead;
@@ -128,8 +133,6 @@ static inline refill_t refill_pop_head(sched_context_t *sc)
 /* add item to tail of refill queue */
 static inline void refill_add_tail(sched_context_t *sc, refill_t refill)
 {
-    /* cannot add an empty refill */
-    assert(refill.rAmount != 0);
     /* cannot add beyond queue size */
     assert(refill_size(sc) < sc->scRefillMax);
 
@@ -141,6 +144,16 @@ static inline void refill_add_tail(sched_context_t *sc, refill_t refill)
     assert(new_tail < sc->scRefillMax);
 }
 
+static inline void maybe_add_empty_tail(sched_context_t *sc)
+{
+    if (isRoundRobin(sc)) {
+        /* add an empty refill - we track the used up time here */
+        refill_t empty_tail = { .rTime = NODE_STATE(ksCurTime)};
+        refill_add_tail(sc, empty_tail);
+        assert(refill_size(sc) == MIN_REFILLS);
+    }
+}
+
 void refill_new(sched_context_t *sc, word_t max_refills, ticks_t budget, ticks_t period)
 {
     sc->scPeriod = period;
@@ -152,6 +165,7 @@ void refill_new(sched_context_t *sc, word_t max_refills, ticks_t budget, ticks_t
     REFILL_HEAD(sc).rAmount = budget;
     /* budget can be used from now */
     REFILL_HEAD(sc).rTime = NODE_STATE(ksCurTime);
+    maybe_add_empty_tail(sc);
     REFILL_SANITY_CHECK(sc, budget);
 }
 
@@ -161,90 +175,78 @@ void refill_update(sched_context_t *sc, ticks_t new_period, ticks_t new_budget,
     /* refill must be initialised in order to be updated - otherwise refill_new should be used */
     assert(sc->scRefillMax > 0);
 
-    /* figure out how much budget is available */
-    ticks_t total_budget = refill_sum(sc);
-    REFILL_SANITY_CHECK(sc, total_budget);
+    /* this is called on an active thread. We want to preserve the sliding window constraint -
+     * so over new_period, new_budget should not be exceeded even temporarily */
 
-    /* first deal with a difference in max refills - merge
-     * any refills that exceed the new max */
-    while (new_max_refills < refill_size(sc)) {
-        /* merge refills */
-
-        assert(!refill_single(sc));
-        refill_t refill = refill_pop_head(sc);
-        REFILL_HEAD(sc).rAmount += refill.rAmount;
-    }
-
-    REFILL_SANITY_CHECK(sc, total_budget);
-
-    /* move anything in the list that is beyond the old max */
-    if (sc->scRefillMax > new_max_refills) {
-        word_t curr = sc->scRefillHead;
-        for (curr = sc->scRefillHead; curr < sc->scRefillMax; curr++) {
-            word_t diff = sc->scRefillMax - new_max_refills;
-            REFILL_INDEX(sc, curr - diff) = REFILL_INDEX(sc, curr);
-        }
-    }
+    /* move the head refill to the start of the list - it's ok as we're going to truncate the
+     * list to size 1 - and this way we can't be in an invalid list position once new_max_refills
+     * is updated */
+    REFILL_INDEX(sc, 0) = REFILL_HEAD(sc);
+    sc->scRefillHead = 0;
+    /* truncate refill list to size 1 */
+    sc->scRefillTail = sc->scRefillHead;
+    /* update max refills */
     sc->scRefillMax = new_max_refills;
-
-    /* now deal with the period change - update each refill by the difference in period */
-    word_t current = refill_next(sc, sc->scRefillHead);
-    while (current != sc->scRefillTail) {
-        /* adjust the period of each refill by new one  (except the head) */
-        REFILL_INDEX(sc, current).rTime += (new_period - sc->scPeriod);
-        current = refill_next(sc, current);
-    }
+    /* update period */
     sc->scPeriod = new_period;
-    REFILL_SANITY_CHECK(sc, total_budget);
 
-    /* now deal with the new budget */
-    if (new_budget > total_budget) {
-        /* if the budget has increased, just add it to the last refill */
-        REFILL_TAIL(sc).rAmount += (new_budget - total_budget);
-    } else {
-        /* if the budget has decreased, iterate through from head to
-         * tail until the amount decreased has been removed from the refill
-         * buffer */
-        ticks_t remove = total_budget - new_budget;
-        while (remove >= REFILL_HEAD(sc).rAmount) {
-            assert(!refill_single(sc));
-            refill_t old_head = refill_pop_head(sc);
-            remove -= old_head.rAmount;
-        }
-        REFILL_HEAD(sc).rAmount -= remove;
-        if (REFILL_HEAD(sc).rAmount < MIN_BUDGET) {
-            assert(!refill_single(sc));
-            refill_t old_head = refill_pop_head(sc);
-            REFILL_HEAD(sc).rAmount += old_head.rAmount;
-        }
+    if (refill_ready(sc)) {
+        REFILL_HEAD(sc).rTime = NODE_STATE(ksCurTime);
+    }
+
+    if (REFILL_HEAD(sc).rAmount >= new_budget) {
+        /* if the heads budget exceeds the new budget just trim it */
+        REFILL_HEAD(sc).rAmount = new_budget;
+        maybe_add_empty_tail(sc);
+    } else {
+        /* otherwise schedule the rest for the next period */
+        refill_t new = { .rAmount = (new_budget - REFILL_HEAD(sc).rAmount),
+                         .rTime = REFILL_HEAD(sc).rTime + new_period
+                       };
+        refill_add_tail(sc, new);
     }
 
-    /* merge any overlapping refills */
-    refill_unblock_check(sc);
     REFILL_SANITY_CHECK(sc, new_budget);
 }
 
-ticks_t refill_budget_check(sched_context_t *sc, ticks_t usage)
+static inline void schedule_used(sched_context_t *sc, refill_t new)
+{
+    /* schedule the used amount */
+    if (new.rAmount < MIN_BUDGET && !refill_single(sc)) {
+        /* used amount is to small - merge with last and delay */
+        REFILL_TAIL(sc).rAmount += new.rAmount;
+        REFILL_TAIL(sc).rTime = MAX(new.rTime, REFILL_TAIL(sc).rTime);
+    } else if (new.rTime <= REFILL_TAIL(sc).rTime) {
+        REFILL_TAIL(sc).rAmount += new.rAmount;
+    } else {
+        refill_add_tail(sc, new);
+    }
+}
+
+void refill_budget_check(sched_context_t *sc, ticks_t usage, ticks_t capacity)
 {
     /* this function should only be called when the sc is out of budget */
-    assert(refill_capacity(sc, usage) == 0);
+    assert(capacity < MIN_BUDGET || refill_full(sc));
+    assert(sc->scPeriod > 0);
     REFILL_SANITY_START(sc);
 
-    while (REFILL_HEAD(sc).rAmount <= usage) {
-        /* exhaust and schedule replenishment */
-        usage -= REFILL_HEAD(sc).rAmount;
-        if (refill_single(sc)) {
-            /* update in place */
-            REFILL_HEAD(sc).rTime += sc->scPeriod;
-        } else {
-            refill_t old_head = refill_pop_head(sc);
-            old_head.rTime = old_head.rTime + sc->scPeriod;
-            refill_add_tail(sc, old_head);
+    if (capacity == 0) {
+        while (REFILL_HEAD(sc).rAmount <= usage) {
+            /* exhaust and schedule replenishment */
+            usage -= REFILL_HEAD(sc).rAmount;
+            if (refill_single(sc)) {
+                /* update in place */
+                REFILL_HEAD(sc).rTime += sc->scPeriod;
+            } else {
+                refill_t old_head = refill_pop_head(sc);
+                old_head.rTime = old_head.rTime + sc->scPeriod;
+                schedule_used(sc, old_head);
+            }
         }
     }
 
     /* budget overrun */
-    if (usage > 0 && sc->scPeriod > 0) {
+    if (usage > 0) {
         /* budget reduced when calculating capacity */
         /* due to overrun delay next replenishment */
         REFILL_HEAD(sc).rTime += usage;
@@ -255,13 +257,25 @@ ticks_t refill_budget_check(sched_context_t *sc, ticks_t usage)
 
             refill_t refill = refill_pop_head(sc);
             REFILL_HEAD(sc).rAmount += refill.rAmount;
+            REFILL_HEAD(sc).rTime = refill.rTime;
         }
     }
 
-    REFILL_SANITY_END(sc);
+    capacity = refill_capacity(sc, usage);
+    if (capacity > 0 && refill_ready(sc)) {
+        refill_split_check(sc, usage);
+    }
 
-    /* return any usage we haven't dealt with */
-    return usage;
+    /* ensure the refill head is sufficient, such that when we wake in awaken,
+     * there is enough budget to run */
+    while (REFILL_HEAD(NODE_STATE(ksCurSC)).rAmount < MIN_BUDGET) {
+        refill_t refill = refill_pop_head(sc);
+        REFILL_HEAD(sc).rAmount += refill.rAmount;
+        /* this loop is guaranteed to terminate as the sum of
+         * rAmount in a refill must be >= MIN_BUDGET */
+    }
+
+    REFILL_SANITY_END(sc);
 }
 
 void refill_split_check(sched_context_t *sc, ticks_t usage)
@@ -272,40 +286,50 @@ void refill_split_check(sched_context_t *sc, ticks_t usage)
      * time has been used */
     assert(usage > 0);
     assert(usage <= REFILL_HEAD(sc).rAmount);
+    assert(sc->scPeriod > 0);
 
     REFILL_SANITY_START(sc);
 
     /* first deal with the remaining budget of the current replenishment */
     ticks_t remnant = REFILL_HEAD(sc).rAmount - usage;
-    if (remnant < MIN_BUDGET && refill_single(sc)) {
-        /* delay entire replenishment - can't merge, nothing to merge with */
-        REFILL_HEAD(sc).rTime += sc->scPeriod;
-        REFILL_SANITY_END(sc);
-        return;
-    }
 
-    if (refill_size(sc) == sc->scRefillMax || remnant < MIN_BUDGET) {
-        assert(!refill_single(sc));
-        /* merge remnant with next replenishment - either it's too small
-         * or we're out of space */
-        refill_pop_head(sc);
-        REFILL_HEAD(sc).rAmount += remnant;
-    } else  {
-        assert(remnant >= MIN_BUDGET);
-        /* split the head refill  */
-        REFILL_HEAD(sc).rAmount = remnant;
-    }
-
-    /* schedule the used amount */
+    /* set up a new replenishment structure */
     refill_t new = (refill_t) {
         .rAmount = usage, .rTime = REFILL_HEAD(sc).rTime + sc->scPeriod
     };
-    refill_add_tail(sc, new);
+
+    if (refill_size(sc) == sc->scRefillMax || remnant < MIN_BUDGET) {
+        /* merge remnant with next replenishment - either it's too small
+         * or we're out of space */
+        if (refill_single(sc)) {
+            /* update inplace */
+            new.rAmount += remnant;
+            REFILL_HEAD(sc) = new;
+        } else {
+            refill_pop_head(sc);
+            REFILL_HEAD(sc).rAmount += remnant;
+            schedule_used(sc, new);
+        }
+        assert(refill_ordered(sc));
+    } else  {
+        /* leave remnant as reduced replenishment */
+        assert(remnant >= MIN_BUDGET);
+        /* split the head refill  */
+        REFILL_HEAD(sc).rAmount = remnant;
+        schedule_used(sc, new);
+    }
+
     REFILL_SANITY_END(sc);
 }
 
 void refill_unblock_check(sched_context_t *sc)
 {
+
+    if (isRoundRobin(sc)) {
+        /* nothing to do */
+        return;
+    }
+
     /* advance earliest activation time to now */
     REFILL_SANITY_START(sc);
     if (refill_ready(sc)) {
@@ -323,14 +347,7 @@ void refill_unblock_check(sched_context_t *sc)
             }
         }
 
-        /* it's possible that a refill is not bigger than min budget (if a task
-         * uses less than min budget, it will still be scheduled for refill), if
-         * so merge with the next refill, as it's not enough to schedule the task. */
-        if (!refill_sufficient(sc, 0)) {
-            assert(!refill_single(sc));
-            refill_t insufficient = refill_pop_head(sc);
-            REFILL_HEAD(sc).rAmount += insufficient.rAmount;
-        }
+        assert(refill_sufficient(sc, 0));
     }
     REFILL_SANITY_END(sc);
 }
diff --git a/src/kernel/thread.c b/src/kernel/thread.c
index 4ab674c18..1523e66e3 100644
--- a/src/kernel/thread.c
+++ b/src/kernel/thread.c
@@ -50,6 +50,7 @@ static inline bool_t PURE isSchedulable(const tcb_t *thread)
 {
     return isRunnable(thread) &&
            thread->tcbSchedContext != NULL &&
+           thread->tcbSchedContext->scRefillMax > 0 &&
            !thread_state_get_tcbInReleaseQueue(thread->tcbState);
 }
 #else
@@ -114,8 +115,9 @@ void restart(tcb_t *target)
         cancelIPC(target);
 #ifdef CONFIG_KERNEL_MCS
         setThreadState(target, ThreadState_Restart);
-        if (likely(target->tcbSchedContext != NULL)) {
-            schedContext_resume(target->tcbSchedContext);
+        schedContext_resume(target->tcbSchedContext);
+        if (isSchedulable(target)) {
+            possibleSwitchTo(target);
         }
 #else
         setupReplyMaster(target);
@@ -330,9 +332,8 @@ static void switchSchedContext(void)
     }
 
     /* if a thread doesn't have enough budget, it should not be in the scheduler */
-    if (!refill_ready(NODE_STATE(ksCurSC)) || !refill_sufficient(NODE_STATE(ksCurSC), 0)) {
-        assert(!thread_state_get_tcbQueued(NODE_STATE(ksCurSC)->scTcb->tcbState));
-    }
+    assert((refill_ready(NODE_STATE(ksCurSC)) && refill_sufficient(NODE_STATE(ksCurSC), 0))
+           || !thread_state_get_tcbQueued(NODE_STATE(ksCurSC)->scTcb->tcbState));
 
     NODE_STATE(ksCurSC) = NODE_STATE(ksCurThread)->tcbSchedContext;
 }
@@ -578,8 +579,31 @@ void setNextInterrupt(void)
     setDeadline(next_interrupt - getTimerPrecision());
 }
 
+void chargeBudget(ticks_t capacity, ticks_t consumed)
+{
+
+    if (isRoundRobin(NODE_STATE(ksCurSC))) {
+        assert(refill_size(NODE_STATE(ksCurSC)) == MIN_REFILLS);
+        REFILL_HEAD(NODE_STATE(ksCurSC)).rAmount += REFILL_TAIL(NODE_STATE(ksCurSC)).rAmount;
+        REFILL_TAIL(NODE_STATE(ksCurSC)).rAmount = 0;
+    } else {
+        refill_budget_check(NODE_STATE(ksCurSC), consumed, capacity);
+    }
+
+    assert(REFILL_HEAD(NODE_STATE(ksCurSC)).rAmount >= MIN_BUDGET);
+    NODE_STATE(ksConsumed) = 0;
+    if (likely(isRunnable(NODE_STATE(ksCurThread)))) {
+        endTimeslice();
+        rescheduleRequired();
+    }
+}
+
 void endTimeslice(void)
 {
+    if (unlikely(NODE_STATE(ksCurThread) == NODE_STATE(ksIdleThread))) {
+        return;
+    }
+
     assert(isRunnable(NODE_STATE(ksCurSC->scTcb)));
     if (refill_ready(NODE_STATE(ksCurSC)) && refill_sufficient(NODE_STATE(ksCurSC), 0)) {
         /* apply round robin */
@@ -645,15 +669,17 @@ void awaken(void)
 {
     while (unlikely(NODE_STATE(ksReleaseHead) != NULL && refill_ready(NODE_STATE(ksReleaseHead)->tcbSchedContext))) {
         tcb_t *awakened = tcbReleaseDequeue();
+        /* the currently running thread cannot have just woken up */
+        assert(awakened != NODE_STATE(ksCurThread));
+        /* round robin threads should not be in the release queue */
+        assert(!isRoundRobin(awakened->tcbSchedContext));
+        /* threads should wake up on the correct core */
         SMP_COND_STATEMENT(assert(awakened->tcbAffinity == getCurrentCPUIndex()));
-        refill_unblock_check(awakened->tcbSchedContext);
-        if (unlikely(!refill_ready(awakened->tcbSchedContext))) {
-            tcbReleaseEnqueue(awakened);
-        } else {
-            assert(refill_sufficient(awakened->tcbSchedContext, 0));
-            tcbSchedAppend(awakened);
-            possibleSwitchTo(awakened);
-        }
+        /* threads HEAD refill should always be > MIN_BUDGET */
+        assert(refill_sufficient(awakened->tcbSchedContext, 0));
+        possibleSwitchTo(awakened);
+        /* changed head of release queue -> need to reprogram */
+        NODE_STATE(ksReprogram) = true;
     }
 }
 #endif
diff --git a/src/object/schedcontext.c b/src/object/schedcontext.c
index 5a6432eec..7e9f46c84 100644
--- a/src/object/schedcontext.c
+++ b/src/object/schedcontext.c
@@ -135,10 +135,21 @@ static exception_t invokeSchedContext_Unbind(sched_context_t *sc)
     return EXCEPTION_NONE;
 }
 
+#ifdef ENABLE_SMP_SUPPORT
+static inline void maybeStallSC(sched_context_t *sc)
+{
+    if (sc->scTcb) {
+        remoteTCBStall(sc->scTcb);
+    }
+}
+#endif
+
 exception_t decodeSchedContextInvocation(word_t label, cap_t cap, extra_caps_t extraCaps)
 {
     sched_context_t *sc = SC_PTR(cap_sched_context_cap_get_capSCPtr(cap));
 
+    SMP_COND_STATEMENT((maybeStallSC(sc));)
+
     switch (label) {
     case SchedContextBind:
         return decodeSchedContext_Bind(sc, extraCaps);
@@ -160,7 +171,6 @@ void schedContext_resume(sched_context_t *sc)
     assert(!sc || sc->scTcb != NULL);
     if (likely(sc) && isSchedulable(sc->scTcb)) {
         assert(sc->scTcb != NULL);
-        refill_unblock_check(sc);
 
         if (isRunnable(sc->scTcb) && sc->scRefillMax > 0) {
             if (!(refill_ready(sc) && refill_sufficient(sc, 0))) {
@@ -179,10 +189,10 @@ void schedContext_bindTCB(sched_context_t *sc, tcb_t *tcb)
     tcb->tcbSchedContext = sc;
     sc->scTcb = tcb;
 
-#if CONFIG_MAX_NUM_NODES > 1
+#ifdef ENABLE_SMP_SUPPORT
     if (tcb->tcbAffinity != sc->scCore) {
         if (isSchedulable(tcb)) {
-            SMP_COND_STATEMENT(remoteTCBStall(tcb));
+            remoteTCBStall(tcb);
             tcbSchedDequeue(tcb);
         }
         migrateTCB(tcb, sc->scCore);
diff --git a/src/object/schedcontrol.c b/src/object/schedcontrol.c
index adf4996de..66d5688fa 100644
--- a/src/object/schedcontrol.c
+++ b/src/object/schedcontrol.c
@@ -19,22 +19,35 @@
 static exception_t invokeSchedControl_Configure(sched_context_t *target, word_t core, ticks_t budget, ticks_t period,
                                                 word_t max_refills)
 {
-    /* don't modify parameters of tcb while it is in a sorted queue */
+
     if (target->scTcb) {
+        /* possibly stall a remote core */
         SMP_COND_STATEMENT(remoteTCBStall(target->scTcb));
+        /* remove from scheduler */
         tcbReleaseRemove(target->scTcb);
         tcbSchedDequeue(target->scTcb);
+        /* bill the current consumed amount before adjusting the params */
+        if (NODE_STATE_ON_CORE(ksCurSC, target->scCore) == target) {
+            ticks_t capacity = refill_capacity(target, NODE_STATE_ON_CORE(ksConsumed, target->scCore));
+            if (checkBudget()) {
+                commitTime();
+            } else {
+                chargeBudget(capacity, NODE_STATE_ON_CORE(ksConsumed, target->scCore));
+            }
+        }
     }
 
     if (budget == period) {
         /* this is a cool hack: for round robin, we set the
          * period to 0, which means that the budget will always be ready to be refilled
-         * and the code doesn't need special casing
+         * and avoids some special casing.
          */
         period = 0;
+        max_refills = MIN_REFILLS;
     }
 
-    if (core == target->scCore && target->scRefillMax > 0 && target->scTcb && isRunnable(target->scTcb)) {
+    if (SMP_COND_STATEMENT(core == target->scCore &&) target->scRefillMax > 0 && target->scTcb
+        && isRunnable(target->scTcb)) {
         /* the scheduling context is active - it can be used, so
          * we need to preserve the bandwidth */
         refill_update(target, period, budget, max_refills);
@@ -42,19 +55,21 @@ static exception_t invokeSchedControl_Configure(sched_context_t *target, word_t
         /* the scheduling context isn't active - it's budget is not being used, so
          * we can just populate the parameters from now */
         refill_new(target, max_refills, budget, period);
-
-        if (core != target->scCore && target->scTcb) {
-            /* if the core changed and the SC has a tcb, the SC is getting
-             * budget - so migrate it */
-            target->scCore = core;
-            SMP_COND_STATEMENT(Arch_migrateTCB(target->scTcb));
-            SMP_COND_STATEMENT(target->scTcb->tcbAffinity = target->scCore;)
+#ifdef ENABLE_SMP_SUPPORT
+        target->scCore = core;
+        if (target->scTcb && target->scTcb->tcbAffinity != target->scCore) {
+            migrateTCB(target->scTcb, target->scCore);
         }
+#endif /* ENABLE_SMP_SUPPORT */
     }
 
-    if (target->scTcb && isRunnable(target->scTcb) && target->scRefillMax > 0) {
+    if (target->scTcb && target->scRefillMax > 0) {
         schedContext_resume(target);
-        possibleSwitchTo(target->scTcb);
+        if (target->scTcb == NODE_STATE(ksCurThread)) {
+            rescheduleRequired();
+        } else if (isRunnable(target->scTcb)) {
+            possibleSwitchTo(target->scTcb);
+        }
     }
 
     return EXCEPTION_NONE;
@@ -76,7 +91,7 @@ static exception_t decodeSchedControl_Configure(word_t length, cap_t cap, extra_
 
     time_t budget_us = mode_parseTimeArg(0, buffer);
     time_t period_us = mode_parseTimeArg(TIME_ARG_SIZE, buffer);
-    word_t max_refills = MIN_REFILLS + getSyscallArg(TIME_ARG_SIZE * 2, buffer);
+    word_t max_refills = getSyscallArg(TIME_ARG_SIZE * 2, buffer);
 
     cap_t targetCap = extraCaps.excaprefs[0]->cap;
     if (unlikely(cap_get_capType(targetCap) != cap_sched_context_cap)) {
diff --git a/src/object/tcb.c b/src/object/tcb.c
index a336df018..01da00553 100644
--- a/src/object/tcb.c
+++ b/src/object/tcb.c
@@ -88,7 +88,6 @@ void tcbSchedEnqueue(tcb_t *tcb)
 #ifdef CONFIG_KERNEL_MCS
     assert(isSchedulable(tcb));
     assert(refill_sufficient(tcb->tcbSchedContext, 0));
-    assert(refill_ready(tcb->tcbSchedContext));
 #endif
 
     if (!thread_state_get_tcbQueued(tcb->tcbState)) {