diff --git a/include/32/mode/api/ipc_buffer.h b/include/32/mode/api/ipc_buffer.h
index c4e6a942959..4e533fcfff1 100644
--- a/include/32/mode/api/ipc_buffer.h
+++ b/include/32/mode/api/ipc_buffer.h
@@ -10,12 +10,12 @@
 #include <api/syscall.h>
 #include <object/structures.h>
 
-static inline time_t mode_parseTimeArg(word_t i, word_t *buffer)
+static inline ticks_t mode_parseTimeArg(word_t i, word_t *buffer)
 {
-    return (((time_t) getSyscallArg(i + 1, buffer) << 32llu) + getSyscallArg(i, buffer));
+    return (((ticks_t) getSyscallArg(i + 1, buffer) << 32llu) + getSyscallArg(i, buffer));
 }
 
-static inline word_t mode_setTimeArg(word_t i, time_t time, word_t *buffer, tcb_t *thread)
+static inline word_t mode_setTimeArg(word_t i, ticks_t time, word_t *buffer, tcb_t *thread)
 {
     setMR(thread, buffer, i, (uint32_t) time);
     return setMR(thread, buffer, i + 1, (uint32_t)(time >> 32llu));
diff --git a/include/64/mode/api/ipc_buffer.h b/include/64/mode/api/ipc_buffer.h
index 12956a7a436..e2c5833f5e1 100644
--- a/include/64/mode/api/ipc_buffer.h
+++ b/include/64/mode/api/ipc_buffer.h
@@ -9,12 +9,12 @@
 #include <types.h>
 #include <api/syscall.h>
 
-static inline time_t mode_parseTimeArg(word_t i, word_t *buffer)
+static inline ticks_t mode_parseTimeArg(word_t i, word_t *buffer)
 {
     return getSyscallArg(i, buffer);
 }
 
-static inline word_t mode_setTimeArg(word_t i, time_t time, word_t *buffer, tcb_t *thread)
+static inline word_t mode_setTimeArg(word_t i, ticks_t time, word_t *buffer, tcb_t *thread)
 {
     return setMR(thread, buffer, i, time);
 }
diff --git a/include/api/types.h b/include/api/types.h
index 3f6675066d2..47065de7522 100644
--- a/include/api/types.h
+++ b/include/api/types.h
@@ -22,11 +22,9 @@
 typedef word_t prio_t;
 
 /* The kernel uses ticks_t internally to represent time to make it easy to
- * interact with hardware timers. The userland API uses time in micro seconds,
- * which is represented by time_t in the kernel.
+ * interact with hardware timers. The userland API uses ticks also.
  */
 typedef uint64_t ticks_t;
-typedef uint64_t time_t;
 
 enum domainConstants {
     minDom = 0,
diff --git a/include/arch/arm/arch/32/mode/machine/timer.h b/include/arch/arm/arch/32/mode/machine/timer.h
index 443b5ee4ac9..f0901866065 100644
--- a/include/arch/arm/arch/32/mode/machine/timer.h
+++ b/include/arch/arm/arch/32/mode/machine/timer.h
@@ -12,30 +12,5 @@
 #ifdef CONFIG_KERNEL_MCS
 #include <util.h>
 
-/* timer function definitions that work for all 32bit arm platforms that provide
- * CLK_MAGIC and TIMER_CLOCK_MHZ -- these definitions might need to move
- * if we come across an arm platform that does not suit this model */
-
-/* Get the max. ticks_t value that can be expressed in time_t (time in us). This
- * is the max. value ticksToUs() can be passed without overflowing.
- */
-static inline CONST ticks_t getMaxTicksToUs(void)
-{
-#if USE_KHZ
-    return UINT64_MAX / KHZ_IN_MHZ / CLK_MAGIC;
-#else
-    return UINT64_MAX / CLK_MAGIC;
-#endif
-}
-
-static inline CONST time_t ticksToUs(ticks_t ticks)
-{
-    /* simulate 64bit division using multiplication by reciprocal */
-#if USE_KHZ
-    return (ticks * KHZ_IN_MHZ) * CLK_MAGIC >> CLK_SHIFT;
-#else
-    return (ticks * CLK_MAGIC) >> CLK_SHIFT;
-#endif
-}
 #endif /* CONFIG_KERNEL_MCS */
 
diff --git a/include/arch/arm/arch/64/mode/machine/timer.h b/include/arch/arm/arch/64/mode/machine/timer.h
index 5c968675ff1..1d0218084c0 100644
--- a/include/arch/arm/arch/64/mode/machine/timer.h
+++ b/include/arch/arm/arch/64/mode/machine/timer.h
@@ -11,27 +11,5 @@
 #include <stdint.h>
 #include <util.h>
 
-/* timer function definitions that work for all 64 bit arm platforms */
-
-/* Get the max. ticks_t value that can be expressed in time_t (time in us). This
- * is the max. value ticksToUs() can be passed without overflowing.
- */
-static inline CONST ticks_t getMaxTicksToUs(void)
-{
-#if USE_KHZ
-    return UINT64_MAX / TIMER_CLOCK_KHZ;
-#else
-    return UINT64_MAX;
-#endif
-}
-
-static inline CONST time_t ticksToUs(ticks_t ticks)
-{
-#if USE_KHZ
-    return (ticks * KHZ_IN_MHZ) / TIMER_CLOCK_KHZ;
-#else
-    return ticks / TIMER_CLOCK_MHZ;
-#endif
-}
 #endif /* CONFIG_KERNEL_MCS */
 
diff --git a/include/arch/arm/arch/machine/timer.h b/include/arch/arm/arch/machine/timer.h
index 553d85291b1..afe9428fc7b 100644
--- a/include/arch/arm/arch/machine/timer.h
+++ b/include/arch/arm/arch/machine/timer.h
@@ -26,33 +26,10 @@
 
 void initTimer(void);
 
-/* Get the max. time_t value (time in us) that can be expressed in ticks_t. This
- * is the max. value usToTicks() can be passed without overflowing.
- */
-static inline CONST time_t getMaxUsToTicks(void)
-{
-#if USE_KHZ
-    return UINT64_MAX / TIMER_CLOCK_KHZ;
-#else
-    return UINT64_MAX / TIMER_CLOCK_MHZ;
-#endif
-}
-
-static inline CONST ticks_t usToTicks(time_t us)
-{
-#if USE_KHZ
-    /* reciprocal division overflows too quickly for dividing by KHZ_IN_MHZ.
-     * This operation isn't used frequently or on many platforms, so use manual
-     * division here */
-    return div64(us * TIMER_CLOCK_KHZ, KHZ_IN_MHZ);
-#else
-    return us * TIMER_CLOCK_MHZ;
-#endif
-}
 
 static inline CONST ticks_t getTimerPrecision(void)
 {
-    return usToTicks(TIMER_PRECISION) + TIMER_OVERHEAD_TICKS;
+    return TIMER_PRECISION + TIMER_OVERHEAD_TICKS;
 }
 #else /* CONFIG_KERNEL_MCS */
 #include <mode/machine/timer.h>
diff --git a/include/arch/riscv/arch/machine/timer.h b/include/arch/riscv/arch/machine/timer.h
index eb287c0c8cf..f9c901303b3 100644
--- a/include/arch/riscv/arch/machine/timer.h
+++ b/include/arch/riscv/arch/machine/timer.h
@@ -13,28 +13,15 @@
 #include <arch/sbi.h>
 #include <arch/machine/hardware.h>
 
-/* The scheduler clock is greater than 1MHz */
-#define TICKS_IN_US (TIMER_CLOCK_HZ / (US_IN_MS * MS_IN_S))
-
-static inline CONST time_t getKernelWcetUs(void)
+static inline CONST ticks_t getKernelWcetTicks(void)
 {
     /* Copied from x86_64. Hopefully it's an overestimate here. */
     return  10u;
 }
 
-static inline PURE ticks_t usToTicks(time_t us)
-{
-    return us * TICKS_IN_US;
-}
-
-static inline PURE time_t ticksToUs(ticks_t ticks)
-{
-    return div64(ticks, TICKS_IN_US);
-}
-
 static inline PURE ticks_t getTimerPrecision(void)
 {
-    return usToTicks(1);
+    return 1;
 }
 
 /* Get the max. ticks_t value that can be expressed in time_t (time in us). This
@@ -45,14 +32,6 @@ static inline CONST ticks_t getMaxTicksToUs(void)
     return UINT64_MAX;
 }
 
-/* Get the max. time_t value (time in us) that can be expressed in ticks_t. This
- * is the max. value usToTicks() can be passed without overflowing.
- */
-static inline CONST time_t getMaxUsToTicks(void)
-{
-    return UINT64_MAX / TICKS_IN_US;
-}
-
 /* Read the current time from the timer. */
 static inline ticks_t getCurrentTime(void)
 {
diff --git a/include/arch/x86/arch/machine/timer.h b/include/arch/x86/arch/machine/timer.h
index 5771277b584..94dab94bd9e 100644
--- a/include/arch/x86/arch/machine/timer.h
+++ b/include/arch/x86/arch/machine/timer.h
@@ -14,28 +14,14 @@
 #include <mode/util.h>
 #include <arch/kernel/apic.h>
 
-static inline CONST time_t getKernelWcetUs(void)
+static inline CONST ticks_t getKernelWcetTicks(void)
 {
     return  10u;
 }
 
-static inline PURE ticks_t usToTicks(time_t us)
-{
-    assert(x86KStscMhz > 0);
-    return us * x86KStscMhz;
-}
-
-/* Get the max. time_t value (time in us) that can be expressed in ticks_t. This
- * is the max. value usToTicks() can be passed without overflowing.
- */
-static inline PURE time_t getMaxUsToTicks(void)
-{
-    return div64(UINT64_MAX, x86KStscMhz);
-}
-
 static inline PURE ticks_t getTimerPrecision(void)
 {
-    return usToTicks(1u);
+    return 1u;
 }
 
 static inline void ackDeadlineIRQ(void)
@@ -47,19 +33,6 @@ static inline ticks_t getCurrentTime(void)
     return x86_rdtsc();
 }
 
-/* Get the max. ticks_t value that can be expressed in time_t (time in us). This
- * is the max. value ticksToUs() can be passed without overflowing.
- */
-static inline CONST ticks_t getMaxTicksToUs(void)
-{
-    return UINT64_MAX;
-}
-
-static inline PURE time_t ticksToUs(ticks_t ticks)
-{
-    return div64(ticks, x86KStscMhz);
-}
-
 static inline void setDeadline(ticks_t deadline)
 {
     if (likely(x86KSapicRatio == 0)) {
diff --git a/include/kernel/sporadic.h b/include/kernel/sporadic.h
index 35518b7b864..730cbb09d0b 100644
--- a/include/kernel/sporadic.h
+++ b/include/kernel/sporadic.h
@@ -31,10 +31,9 @@
 
 /* To do an operation in the kernel, the thread must have
  * at least this much budget - see comment on refill_sufficient */
-#define MIN_BUDGET_US (2u * getKernelWcetUs() * CONFIG_KERNEL_WCET_SCALE)
 #define MIN_BUDGET    (2u * getKernelWcetTicks() * CONFIG_KERNEL_WCET_SCALE)
 #if (CONFIG_KERNEL_STATIC_MAX_PERIOD_US) != 0
-#define MAX_PERIOD_US (CONFIG_KERNEL_STATIC_MAX_PERIOD_US)
+#define MAX_PERIOD_TICKS (CONFIG_KERNEL_STATIC_MAX_PERIOD_US)
 #else
 /* The maximum period determines the point at which the scheduling logic
  * will no longer function correctly (UINT64_MAX - 5 * MAX_PERIOD), so
@@ -44,9 +43,9 @@
  * Anything below getMaxUsToTicks() / 8 would ensure that time up to
  * 2^63 would still be be valid as 5 * (getMaxUsToTicks()) must be less
  * than 2^62. */
-#define MAX_PERIOD_US (getMaxUsToTicks() / 8)
+#define MAX_PERIOD_TICKS (UINT64_MAX / 8)
 #endif /* CONFIG_KERNEL_STATIC_MAX_PERIOD_US != 0 */
-#define MAX_RELEASE_TIME (UINT64_MAX - 5 * usToTicks(MAX_PERIOD_US))
+#define MAX_RELEASE_TIME (UINT64_MAX - 5 * MAX_PERIOD_TICKS)
 
 /* Short hand for accessing refill queue items */
 static inline refill_t *refill_index(sched_context_t *sc, word_t index)
diff --git a/include/machine/timer.h b/include/machine/timer.h
index 70f412b69f1..457011443fd 100644
--- a/include/machine/timer.h
+++ b/include/machine/timer.h
@@ -25,11 +25,6 @@ static inline void setDeadline(ticks_t deadline);
 /** MODIFIES: [*] */
 static inline void ackDeadlineIRQ(void);
 
-/* get the expected wcet of the kernel for this platform */
-static PURE inline ticks_t getKernelWcetTicks(void)
-{
-    return usToTicks(getKernelWcetUs());
-}
 #else /* CONFIG_KERNEL_MCS */
 static inline void resetTimer(void);
 #endif /* !CONFIG_KERNEL_MCS */
diff --git a/include/object/schedcontext.h b/include/object/schedcontext.h
index 3f2a0948c24..7810bc24ba9 100644
--- a/include/object/schedcontext.h
+++ b/include/object/schedcontext.h
@@ -65,7 +65,7 @@ void schedContext_bindNtfn(sched_context_t *sc, notification_t *ntfn);
 /* unbind scheduling context from a notification */
 void schedContext_unbindNtfn(sched_context_t *sc);
 
-time_t schedContext_updateConsumed(sched_context_t *sc);
+ticks_t schedContext_updateConsumed(sched_context_t *sc);
 void schedContext_completeYieldTo(tcb_t *yielder);
 void schedContext_cancelYieldTo(tcb_t *yielder);
 
diff --git a/libsel4/include/interfaces/object-api.xml b/libsel4/include/interfaces/object-api.xml
index 07e5623e56f..81139f3e511 100644
--- a/libsel4/include/interfaces/object-api.xml
+++ b/libsel4/include/interfaces/object-api.xml
@@ -1346,9 +1346,9 @@
             <param dir="in" name="schedcontext" type="seL4_SchedContext"
                 description="Capability to the scheduling context which is being operated on."/>
             <param dir="in" name="budget" type="seL4_Time"
-                description="Timeslice in microseconds, when the budget expires the thread will be pre-empted."/>
+                description="Timeslice in ticks, when the budget expires the thread will be pre-empted."/>
             <param dir="in" name="period" type="seL4_Time"
-                description="Period in microseconds, if equal to budget, this thread will be treated as a round-robin thread. Otherwise, sporadic servers will be used to assure the scheduling context does not exceed the budget over the specified period."/>
+                description="Period in ticks, if equal to budget, this thread will be treated as a round-robin thread. Otherwise, sporadic servers will be used to assure the scheduling context does not exceed the budget over the specified period."/>
             <param dir="in" name="extra_refills" type="seL4_Word"
                 description="Number of extra sporadic replenishments this scheduling context should use. Ignored for round-robin threads."/>
             <param dir="in" name="badge" type="seL4_Word"
diff --git a/src/api/faults.c b/src/api/faults.c
index 6efe1869cf1..187d634a935 100644
--- a/src/api/faults.c
+++ b/src/api/faults.c
@@ -222,7 +222,7 @@ word_t setMRs_fault(tcb_t *sender, tcb_t *receiver, word_t *receiveIPCBuffer)
         word_t len = setMR(receiver, receiveIPCBuffer, seL4_Timeout_Data,
                            seL4_Fault_Timeout_get_badge(sender->tcbFault));
         if (sender->tcbSchedContext) {
-            time_t consumed = schedContext_updateConsumed(sender->tcbSchedContext);
+            ticks_t consumed = schedContext_updateConsumed(sender->tcbSchedContext);
             return mode_setTimeArg(len, consumed,
                                    receiveIPCBuffer, receiver);
         } else {
diff --git a/src/arch/arm/platform_gen.h.in b/src/arch/arm/platform_gen.h.in
index 217933a0548..a896bf9b149 100644
--- a/src/arch/arm/platform_gen.h.in
+++ b/src/arch/arm/platform_gen.h.in
@@ -38,7 +38,7 @@ enum IRQConstants {
 #endif
 
 #ifdef CONFIG_KERNEL_MCS
-static inline CONST time_t getKernelWcetUs(void)
+static inline CONST ticks_t getKernelWcetTicks(void)
 {
     return @CONFIGURE_KERNEL_WCET@;
 }
diff --git a/src/kernel/boot.c b/src/kernel/boot.c
index 0159dee3dd2..09337e1a44a 100644
--- a/src/kernel/boot.c
+++ b/src/kernel/boot.c
@@ -481,7 +481,7 @@ BOOT_CODE void create_idle_thread(void)
         SMP_COND_STATEMENT(NODE_STATE_ON_CORE(ksIdleThread, i)->tcbAffinity = i);
 #ifdef CONFIG_KERNEL_MCS
         configure_sched_context(NODE_STATE_ON_CORE(ksIdleThread, i), SC_PTR(&ksIdleThreadSC[SMP_TERNARY(i, 0)]),
-                                usToTicks(CONFIG_BOOT_THREAD_TIME_SLICE * US_IN_MS));
+                                CONFIG_BOOT_THREAD_TIME_SLICE);
         SMP_COND_STATEMENT(NODE_STATE_ON_CORE(ksIdleThread, i)->tcbSchedContext->scCore = i;)
         NODE_STATE_ON_CORE(ksIdleSC, i) = SC_PTR(&ksIdleThreadSC[SMP_TERNARY(i, 0)]);
 #endif
@@ -530,7 +530,7 @@ BOOT_CODE tcb_t *create_initial_thread(cap_t root_cnode_cap, cap_t it_pd_cap, vp
 
     /* initialise TCB */
 #ifdef CONFIG_KERNEL_MCS
-    configure_sched_context(tcb, SC_PTR(rootserver.sc), usToTicks(CONFIG_BOOT_THREAD_TIME_SLICE * US_IN_MS));
+    configure_sched_context(tcb, SC_PTR(rootserver.sc), CONFIG_BOOT_THREAD_TIME_SLICE);
 #endif
 
     tcb->tcbPriority = seL4_MaxPrio;
@@ -543,7 +543,7 @@ BOOT_CODE tcb_t *create_initial_thread(cap_t root_cnode_cap, cap_t it_pd_cap, vp
 
     ksCurDomain = ksDomSchedule[ksDomScheduleIdx].domain;
 #ifdef CONFIG_KERNEL_MCS
-    ksDomainTime = usToTicks(ksDomSchedule[ksDomScheduleIdx].length * US_IN_MS);
+    ksDomainTime = ksDomSchedule[ksDomScheduleIdx].length;
 #else
     ksDomainTime = ksDomSchedule[ksDomScheduleIdx].length;
 #endif
@@ -572,7 +572,7 @@ BOOT_CODE tcb_t *create_initial_thread(cap_t root_cnode_cap, cap_t it_pd_cap, vp
 BOOT_CODE void clock_sync_test(void)
 {
     ticks_t t, t0;
-    ticks_t margin = usToTicks(CLOCK_SYNC_DELTA) + getTimerPrecision();
+    ticks_t margin = CLOCK_SYNC_DELTA + getTimerPrecision();
 
     assert(getCurrentCPUIndex() != 0);
     t = NODE_STATE_ON_CORE(ksCurTime, 0);
diff --git a/src/kernel/thread.c b/src/kernel/thread.c
index 5ef186a8feb..bbcfb287752 100644
--- a/src/kernel/thread.c
+++ b/src/kernel/thread.c
@@ -310,11 +310,7 @@ static void nextDomain(void)
 #endif
     ksWorkUnitsCompleted = 0;
     ksCurDomain = ksDomSchedule[ksDomScheduleIdx].domain;
-#ifdef CONFIG_KERNEL_MCS
-    ksDomainTime = usToTicks(ksDomSchedule[ksDomScheduleIdx].length * US_IN_MS);
-#else
     ksDomainTime = ksDomSchedule[ksDomScheduleIdx].length;
-#endif
 }
 
 #ifdef CONFIG_KERNEL_MCS
diff --git a/src/machine/capdl.c b/src/machine/capdl.c
index 6acd820f70a..cf9869d4fba 100644
--- a/src/machine/capdl.c
+++ b/src/machine/capdl.c
@@ -124,10 +124,10 @@ void obj_sc_print_attrs(cap_t sc_cap)
     sched_context_t *sc = SC_PTR(cap_sched_context_cap_get_capSCPtr(sc_cap));
     ticks_t period = sc->scPeriod;
     ticks_t budget = sc_get_budget(sc);
-    printf("(period: %"PRIu64" us (%"PRIu64" ticks), budget: %"PRIu64 " us "
-           "(%"PRIu64" ticks), %"SEL4_PRIu_word" bits)\n",
-           ticksToUs(period), period,
-           ticksToUs(budget), budget,
+    printf("(period: %"PRIu64" ticks, budget: %"PRIu64 " ticks "
+           ", %"SEL4_PRIu_word" bits)\n",
+           period,
+           budget,
            (word_t)cap_sched_context_cap_get_capSCSizeBits(sc_cap));
 }
 #endif /* CONFIG_KERNEL_MCS */
diff --git a/src/object/schedcontext.c b/src/object/schedcontext.c
index 0c5d8eaa0b2..a656a4c3d27 100644
--- a/src/object/schedcontext.c
+++ b/src/object/schedcontext.c
@@ -161,7 +161,7 @@ static inline void maybeStallSC(sched_context_t *sc)
 
 static inline void setConsumed(sched_context_t *sc, word_t *buffer)
 {
-    time_t consumed = schedContext_updateConsumed(sc);
+    ticks_t consumed = schedContext_updateConsumed(sc);
     word_t length = mode_setTimeArg(0, consumed, buffer, NODE_STATE(ksCurThread));
     setRegister(NODE_STATE(ksCurThread), msgInfoRegister, wordFromMessageInfo(seL4_MessageInfo_new(0, 0, 0, length)));
 }
@@ -378,16 +378,11 @@ void schedContext_unbindNtfn(sched_context_t *sc)
     }
 }
 
-time_t schedContext_updateConsumed(sched_context_t *sc)
+ticks_t schedContext_updateConsumed(sched_context_t *sc)
 {
     ticks_t consumed = sc->scConsumed;
-    if (consumed >= getMaxTicksToUs()) {
-        sc->scConsumed -= getMaxTicksToUs();
-        return ticksToUs(getMaxTicksToUs());
-    } else {
-        sc->scConsumed = 0;
-        return ticksToUs(consumed);
-    }
+    sc->scConsumed = 0;
+    return consumed;
 }
 
 void schedContext_cancelYieldTo(tcb_t *tcb)
diff --git a/src/object/schedcontrol.c b/src/object/schedcontrol.c
index 408daf74fe6..5e635231474 100644
--- a/src/object/schedcontrol.c
+++ b/src/object/schedcontrol.c
@@ -91,10 +91,8 @@ static exception_t decodeSchedControl_ConfigureFlags(word_t length, cap_t cap, w
         return EXCEPTION_SYSCALL_ERROR;
     }
 
-    time_t budget_us = mode_parseTimeArg(0, buffer);
-    ticks_t budget_ticks = usToTicks(budget_us);
-    time_t period_us = mode_parseTimeArg(TIME_ARG_SIZE, buffer);
-    ticks_t period_ticks = usToTicks(period_us);
+    ticks_t budget_ticks = mode_parseTimeArg(0, buffer);
+    ticks_t period_ticks = mode_parseTimeArg(TIME_ARG_SIZE, buffer);
     word_t extra_refills = getSyscallArg(TIME_ARG_SIZE * 2, buffer);
     word_t badge = getSyscallArg(TIME_ARG_SIZE * 2 + 1, buffer);
     word_t flags = getSyscallArg(TIME_ARG_SIZE * 2 + 2, buffer);
@@ -107,27 +105,27 @@ static exception_t decodeSchedControl_ConfigureFlags(word_t length, cap_t cap, w
         return EXCEPTION_SYSCALL_ERROR;
     }
 
-    if (budget_us > MAX_PERIOD_US || budget_ticks < MIN_BUDGET) {
+    if (budget_ticks > MAX_PERIOD_TICKS || budget_ticks < MIN_BUDGET) {
         userError("SchedControl_ConfigureFlags: budget out of range.");
         current_syscall_error.type = seL4_RangeError;
-        current_syscall_error.rangeErrorMin = MIN_BUDGET_US;
-        current_syscall_error.rangeErrorMax = MAX_PERIOD_US;
+        current_syscall_error.rangeErrorMin = MIN_BUDGET;
+        current_syscall_error.rangeErrorMax = MAX_PERIOD_TICKS;
         return EXCEPTION_SYSCALL_ERROR;
     }
 
-    if (period_us > MAX_PERIOD_US || period_ticks < MIN_BUDGET) {
+    if (period_ticks > MAX_PERIOD_TICKS || period_ticks < MIN_BUDGET) {
         userError("SchedControl_ConfigureFlags: period out of range.");
         current_syscall_error.type = seL4_RangeError;
-        current_syscall_error.rangeErrorMin = MIN_BUDGET_US;
-        current_syscall_error.rangeErrorMax = MAX_PERIOD_US;
+        current_syscall_error.rangeErrorMin = MIN_BUDGET;
+        current_syscall_error.rangeErrorMax = MAX_PERIOD_TICKS;
         return EXCEPTION_SYSCALL_ERROR;
     }
 
     if (budget_ticks > period_ticks) {
         userError("SchedControl_ConfigureFlags: budget must be <= period");
         current_syscall_error.type = seL4_RangeError;
-        current_syscall_error.rangeErrorMin = MIN_BUDGET_US;
-        current_syscall_error.rangeErrorMax = period_us;
+        current_syscall_error.rangeErrorMin = MIN_BUDGET;
+        current_syscall_error.rangeErrorMax = period_ticks;
         return EXCEPTION_SYSCALL_ERROR;
     }