273 	 * Get TSC frequency known at this moment.  in dtrace_gethrtime_init()
274 	 * This should be constant if TSC is invariant.  in dtrace_gethrtime_init()
276 	 * will preserve monotonic property of TSC.  in dtrace_gethrtime_init()
284 	 * Thus minimum supported TSC frequency is 62.5MHz.  in dtrace_gethrtime_init()
287 	    ("TSC frequency is too low"));  in dtrace_gethrtime_init()
294 	 * - it supports TSC frequencies as low as 62.5MHz (see above);  in dtrace_gethrtime_init()
335 	uint64_t tsc;  in dtrace_gethrtime()  local
340 	 * We split TSC value into lower and higher 32-bit halves and separately  in dtrace_gethrtime()
346 	tsc = rdtsc() - tsc_skew[curcpu];  in dtrace_gethrtime()
349 	lo = tsc;  in dtrace_gethrtime()
350 	hi = tsc >> 32;  in dtrace_gethrtime()