Print statistics at power off.
[pintos-anon] / src / devices / timer.h
1 #ifndef DEVICES_TIMER_H
2 #define DEVICES_TIMER_H
3
4 #include <round.h>
5 #include <stdint.h>
6
7 /* Number of timer interrupts per second. */
8 #define TIMER_FREQ 100
9
10 void timer_init (void);
11 int64_t timer_ticks (void);
12 int64_t timer_elapsed (int64_t);
13
14 void timer_sleep (int64_t ticks);
15
16 int64_t timer_ms2ticks (int64_t ms);
17 int64_t timer_us2ticks (int64_t us);
18 int64_t timer_ns2ticks (int64_t ns);
19
20 void timer_print_stats (void);
21
22 #endif /* devices/timer.h */