Index: head/sys/dev/hyperv/vmbus/hv_et.c
===================================================================
--- head/sys/dev/hyperv/vmbus/hv_et.c
+++ head/sys/dev/hyperv/vmbus/hv_et.c
@@ -61,40 +61,27 @@
 
 static struct eventtimer *et;
 
-static inline uint64_t
+static __inline uint64_t
 sbintime2tick(sbintime_t time)
 {
 	struct timespec val;
 
 	val = sbttots(time);
-	return val.tv_sec * HV_TIMER_FREQUENCY + val.tv_nsec / 100;
+	return (val.tv_sec * HV_TIMER_FREQUENCY) + (val.tv_nsec / 100);
 }
 
 static int
 hv_et_start(struct eventtimer *et, sbintime_t firsttime, sbintime_t periodtime)
 {
-	uint64_t current, config;
-
-	config = MSR_HV_STIMER_CFG_AUTOEN | MSR_HV_STIMER0_CFG_SINT;
+	uint64_t current;
 
 	current = rdmsr(MSR_HV_TIME_REF_COUNT);
 	current += sbintime2tick(firsttime);
-
-	wrmsr(MSR_HV_STIMER0_CONFIG, config);
 	wrmsr(MSR_HV_STIMER0_COUNT, current);
 
 	return (0);
 }
 
-static int
-hv_et_stop(struct eventtimer *et)
-{
-	wrmsr(MSR_HV_STIMER0_CONFIG, 0);
-	wrmsr(MSR_HV_STIMER0_COUNT, 0);
-
-	return (0);
-}
-
 void
 hv_et_intr(struct trapframe *frame)
 {
@@ -130,6 +117,31 @@
 	return (BUS_PROBE_NOWILDCARD);
 }
 
+static void
+vmbus_et_config(void *arg __unused)
+{
+	/*
+	 * Make sure that STIMER0 is really disabled before writing
+	 * to STIMER0_CONFIG.
+	 *
+	 * "Writing to the configuration register of a timer that
+	 *  is already enabled may result in undefined behaviour."
+	 */
+	for (;;) {
+		uint64_t val;
+
+		/* Stop counting, and this also implies disabling STIMER0 */
+		wrmsr(MSR_HV_STIMER0_COUNT, 0);
+
+		val = rdmsr(MSR_HV_STIMER0_CONFIG);
+		if ((val & MSR_HV_STIMER_CFG_ENABLE) == 0)
+			break;
+		cpu_spinwait();
+	}
+	wrmsr(MSR_HV_STIMER0_CONFIG,
+	    MSR_HV_STIMER_CFG_AUTOEN | MSR_HV_STIMER0_CFG_SINT);
+}
+
 static int
 hv_et_attach(device_t dev)
 {
@@ -143,9 +155,16 @@
 	et->et_min_period = HV_MIN_DELTA_TICKS * ((1LL << 32) / HV_TIMER_FREQUENCY);
 	et->et_max_period = HV_MAX_DELTA_TICKS * ((1LL << 32) / HV_TIMER_FREQUENCY);
 	et->et_start = hv_et_start;
-	et->et_stop = hv_et_stop;
 	et->et_priv = dev;
 
+	/*
+	 * Delay a bit to make sure that MSR_HV_TIME_REF_COUNT will
+	 * not return 0, since writing 0 to STIMER0_COUNT will disable
+	 * STIMER0.
+	 */
+	DELAY(100);
+	smp_rendezvous(NULL, vmbus_et_config, NULL, NULL);
+
 	return (et_register(et));
 }