#include <typedefs.h>

u64 get_tsc();
u64 get_hz();