295 	 * Get TSC frequency known at this moment.  in dtrace_gethrtime_init()
296 	 * This should be constant if TSC is invariant.  in dtrace_gethrtime_init()
298 	 * will preserve monotonic property of TSC.  in dtrace_gethrtime_init()
306 	 * Thus minimum supported TSC frequency is 62.5MHz.  in dtrace_gethrtime_init()
309 	    ("TSC frequency is too low"));  in dtrace_gethrtime_init()
316 	 * - it supports TSC frequencies as low as 62.5MHz (see above);  in dtrace_gethrtime_init()
357 	uint64_t tsc;  in dtrace_gethrtime()  local
362 	 * We split TSC value into lower and higher 32-bit halves and separately  in dtrace_gethrtime()
368 	tsc = rdtsc() - tsc_skew[curcpu];  in dtrace_gethrtime()
371 	lo = tsc;  in dtrace_gethrtime()
372 	hi = tsc >> 32;  in dtrace_gethrtime()