1 
2 #include <stdbool.h>
3 #include <stdint.h>
4 
5 #include <sys/kassert.h>
6 #include <sys/kdebug.h>
7 #include <sys/ktime.h>
8 
9 #include <machine/amd64.h>
10 #include <machine/amd64op.h>
11 
12 uint64_t
Time_GetTSC()13 Time_GetTSC()
14 {
15     return rdtsc();
16 }
17 
18 static void
Debug_ReadTSC(int argc,const char * argv[])19 Debug_ReadTSC(int argc, const char *argv[])
20 {
21     kprintf("RDTSC: %lld\n", Time_GetTSC());
22 }
23 
24 REGISTER_DBGCMD(readtsc, "Print current timestamp", Debug_ReadTSC);
25 
26