diff --git a/hypervisor/arch/x86/cpu.c b/hypervisor/arch/x86/cpu.c
index 42c50642e..53c221953 100644
--- a/hypervisor/arch/x86/cpu.c
+++ b/hypervisor/arch/x86/cpu.c
@@ -423,21 +423,29 @@ static void print_hv_banner(void)
 	printf(boot_msg);
 }
 
+static
+inline void asm_monitor(volatile const uint64_t *addr, uint64_t ecx, uint64_t edx)
+{
+	asm volatile("monitor\n" : : "a" (addr), "c" (ecx), "d" (edx));
+}
+
+static
+inline void asm_mwait(uint64_t eax, uint64_t ecx)
+{
+	asm volatile("mwait\n" : : "a" (eax), "c" (ecx));
+}
+
 /* wait until *sync == wake_sync */
-void wait_sync_change(uint64_t *sync, uint64_t wake_sync)
+void wait_sync_change(volatile const uint64_t *sync, uint64_t wake_sync)
 {
 	if (has_monitor_cap()) {
 		/* Wait for the event to be set using monitor/mwait */
-		asm volatile ("1: cmpq      %%rbx,(%%rax)\n"
-			      "   je        2f\n"
-			      "   monitor\n"
-			      "   mwait\n"
-			      "   jmp       1b\n"
-			      "2:\n"
-			      :
-			      : "a" (sync), "d"(0), "c"(0),
-			      "b"(wake_sync)
-			      : "cc");
+		while ((*sync) != wake_sync) {
+			asm_monitor(sync, 0UL, 0UL);
+			if ((*sync) != wake_sync) {
+				asm_mwait(0UL, 0UL);
+			}
+		}
 	} else {
 		/* Wait for the event to be set using pause */
 		asm volatile ("1: cmpq      %%rbx,(%%rax)\n"
diff --git a/hypervisor/include/arch/x86/cpu.h b/hypervisor/include/arch/x86/cpu.h
index 04d2ac78e..8ad203706 100644
--- a/hypervisor/include/arch/x86/cpu.h
+++ b/hypervisor/include/arch/x86/cpu.h
@@ -270,7 +270,7 @@ void init_pcpu_post(uint16_t pcpu_id);
 bool start_pcpus(uint64_t mask);
 void wait_pcpus_offline(uint64_t mask);
 void stop_pcpus(void);
-void wait_sync_change(uint64_t *sync, uint64_t wake_sync);
+void wait_sync_change(volatile const uint64_t *sync, uint64_t wake_sync);
 
 #define CPU_SEG_READ(seg, result_ptr)						\
 {										\