diff --git a/sys/x86/x86/tsc.c b/sys/x86/x86/tsc.c
--- a/sys/x86/x86/tsc.c
+++ b/sys/x86/x86/tsc.c
@@ -240,7 +240,7 @@
 }
 
 static void
-tsc_freq_8254(uint64_t *res)
+tsc_freq_tc(uint64_t *res)
 {
 	uint64_t tsc1, tsc2;
 	int64_t overhead;
@@ -262,8 +262,15 @@
 	tsc_freq = (tsc2 - tsc1 - overhead) * 10;
 }
 
+/*
+ * Try to determine the TSC frequency using CPUID or hypercalls.  If successful,
+ * this lets use the TSC for early DELAY() calls instead of the 8254 timer,
+ * which may be unreliable or entirely absent on contemporary systems.  However,
+ * avoid calibrating using the 8254 here so as to give hypervisors a chance to
+ * register a timecounter that can be used instead.
+ */
 static void
-probe_tsc_freq(void)
+probe_tsc_freq_early(void)
 {
 #ifdef __i386__
 	/* The TSC is known to be broken on certain CPUs. */
@@ -364,7 +371,20 @@
 		if (bootverbose)
 			printf("Early TSC frequency %juHz derived from CPUID\n",
 			    (uintmax_t)tsc_freq);
-	} else if (tsc_skip_calibration) {
+	}
+}
+
+/*
+ * If we were unable to determine the TSC frequency via CPU registers, try
+ * to calibrate against a known clock.
+ */
+static void
+probe_tsc_freq_late(void)
+{
+	if (tsc_freq != 0)
+		return;
+
+	if (tsc_skip_calibration) {
 		/*
 		 * Try to parse the brand string to obtain the nominal TSC
 		 * frequency.
@@ -380,15 +400,24 @@
 		}
 	} else {
 		/*
-		 * Calibrate against the 8254 PIT.  This estimate will be
-		 * refined later in tsc_calib().
+		 * Calibrate against a timecounter or the 8254 PIT.  This
+		 * estimate will be refined later in tsc_calib().
 		 */
-		tsc_freq_8254(&tsc_freq);
+		tsc_freq_tc(&tsc_freq);
 		if (bootverbose)
 			printf(
 		    "Early TSC frequency %juHz calibrated from 8254 PIT\n",
 			    (uintmax_t)tsc_freq);
 	}
+}
+
+void
+start_TSC(void)
+{
+	if ((cpu_feature & CPUID_TSC) == 0 || tsc_disabled)
+		return;
+
+	probe_tsc_freq_late();
 
 	if (cpu_power_ecx & CPUID_PERF_STAT) {
 		/*
@@ -401,13 +430,6 @@
 		if (rdmsr(MSR_MPERF) > 0 && rdmsr(MSR_APERF) > 0)
 			tsc_perf_stat = 1;
 	}
-}
-
-void
-start_TSC(void)
-{
-	if ((cpu_feature & CPUID_TSC) == 0 || tsc_disabled)
-		return;
 
 	/*
 	 * Inform CPU accounting about our boot-time clock rate.  This will
@@ -718,7 +740,7 @@
 	if ((cpu_feature & CPUID_TSC) == 0 || tsc_disabled)
 		return;
 
-	probe_tsc_freq();
+	probe_tsc_freq_early();
 }
 
 /*