unsigned long long rdtsc(void);