Draft: Look at diff for just using ticks in public kernel api

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));

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);
 }

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,

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 */
 

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 */
 

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>

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)
 {

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)) {

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)

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 */

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);
 

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"

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 {

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@;
 }

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);

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

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 */