Improve comments.
[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 void timer_calibrate (void);
12
13 int64_t timer_ticks (void);
14 int64_t timer_elapsed (int64_t);
15
16 void timer_sleep (int64_t ticks);
17 void timer_msleep (int64_t milliseconds);
18 void timer_usleep (int64_t microseconds);
19 void timer_nsleep (int64_t nanoseconds);
20
21 void timer_print_stats (void);
22
23 #endif /* devices/timer.h */