uint64_t inl_rdtscp(uint32_t *aux) {
  uint64_t time;
  asm volatile("rdtscp\n\t"
	       "shl $32, %%rdx\n\t"
	       "mov %%eax, %%edx\n\t"
	       "mov %%ecx, %0\n\t"
	       "mov %%rdx, %1\n\t"
	       : "=m"(aux), "=m"(time)
	       :
	       : "eax", "edx", "ecx", "rdx");

  return time;
}