-#if STAT_TIME
-
-#include <kern/macro_help.h>
-
-/* Advance a timer by a 32 bit value */
-#define TIMER_BUMP(timer, ticks) \
-MACRO_BEGIN \
- uint32_t old_low, low; \
- \
- old_low = (timer)->low_bits; \
- low = old_low + (ticks); \
- if (low < old_low) \
- timer_update((timer), (timer)->high_bits + 1, low); \
- else \
- (timer)->low_bits = low; \
-MACRO_END
-
-#define timer_start(timer, tstamp)
-#define timer_stop(timer, tstamp)
-#define timer_switch(timer, tstamp, new_timer)
-#define thread_timer_event(tstamp, new_timer)
-
-#else /* STAT_TIME */
-
-#define TIMER_BUMP(timer, ticks)
-
-/* Start a timer by setting the timestamp */
-extern void timer_start(
- timer_t timer,
- uint64_t tstamp);
-
-/* Stop a timer by updating from the timestamp */
-extern void timer_stop(
- timer_t timer,
- uint64_t tstamp);
-
-/* Update the timer and start a new one */
-extern void timer_switch(
- timer_t timer,
- uint64_t tstamp,
- timer_t new_timer);
-
-/* Update the thread timer at an event */
-extern void thread_timer_event(
- uint64_t tstamp,
- timer_t new_timer);
-
-#endif /* STAT_TIME */
-
-/* Initialize a timer */
-extern void timer_init(
- timer_t timer);
-
-/* Update a saved timer value and return delta to current value */
-extern uint64_t timer_delta(
- timer_t timer,
- uint64_t *save);
-
-/* Advance a timer by a 64 bit value */
-extern void timer_advance(
- timer_t timer,
- uint64_t delta);
+/*
+ * Start the `timer` at time `tstamp`.
+ */
+void timer_start(timer_t timer, uint64_t tstamp);
+
+/*
+ * Stop the `timer` and update it with time `tstamp`.
+ */
+void timer_stop(timer_t timer, uint64_t tstamp);