diff --git a/lib/x86/processor.h b/lib/x86/processor.h
index 03242206..9db07346 100644
--- a/lib/x86/processor.h
+++ b/lib/x86/processor.h
@@ -720,13 +720,12 @@ static inline void irq_disable(void)
 	asm volatile("cli");
 }
 
-/* Note that irq_enable() does not ensure an interrupt shadow due
- * to the vagaries of compiler optimizations.  If you need the
- * shadow, use a single asm with "sti" and the instruction after it.
- */
 static inline void irq_enable(void)
 {
-	asm volatile("sti");
+	asm volatile(
+			"sti \n\t"
+			"nop\n\t"
+	);
 }
 
 static inline void invlpg(volatile void *va)
diff --git a/x86/apic.c b/x86/apic.c
index 23508ad5..a8964d88 100644
--- a/x86/apic.c
+++ b/x86/apic.c
@@ -36,7 +36,6 @@ static void __test_tsc_deadline_timer(void)
     irq_enable();
 
     wrmsr(MSR_IA32_TSCDEADLINE, rdmsr(MSR_IA32_TSC));
-    asm volatile ("nop");
     report(tdt_count == 1, "tsc deadline timer");
     report(rdmsr(MSR_IA32_TSCDEADLINE) == 0, "tsc deadline timer clearing");
 }
diff --git a/x86/ioapic.c b/x86/ioapic.c
index 4f578ce4..2e460a6d 100644
--- a/x86/ioapic.c
+++ b/x86/ioapic.c
@@ -129,7 +129,6 @@ static void test_ioapic_simultaneous(void)
 	toggle_irq_line(0x0f);
 	toggle_irq_line(0x0e);
 	irq_enable();
-	asm volatile ("nop");
 	report(g_66 && g_78 && g_66_after_78 && g_66_rip == g_78_rip,
 	       "ioapic simultaneous edge interrupts");
 }
diff --git a/x86/svm_tests.c b/x86/svm_tests.c
index e2ec9541..a6397821 100644
--- a/x86/svm_tests.c
+++ b/x86/svm_tests.c
@@ -1000,7 +1000,6 @@ static bool pending_event_finished(struct svm_test *test)
 		}
 
 		irq_enable();
-		asm volatile ("nop");
 		irq_disable();
 
 		if (!pending_event_ipi_fired) {
@@ -1056,7 +1055,6 @@ static void pending_event_cli_test(struct svm_test *test)
 
 	/* VINTR_MASKING is zero.  This should cause the IPI to fire.  */
 	irq_enable();
-	asm volatile ("nop");
 	irq_disable();
 
 	if (pending_event_ipi_fired != true) {
@@ -1072,7 +1070,6 @@ static void pending_event_cli_test(struct svm_test *test)
 	 * that L0 did not leave a stale VINTR in the VMCB.
 	 */
 	irq_enable();
-	asm volatile ("nop");
 	irq_disable();
 }
 
@@ -1105,7 +1102,6 @@ static bool pending_event_cli_finished(struct svm_test *test)
 		}
 
 		irq_enable();
-		asm volatile ("nop");
 		irq_disable();
 
 		if (pending_event_ipi_fired != true) {
@@ -1243,7 +1239,6 @@ static bool interrupt_finished(struct svm_test *test)
 		}
 
 		irq_enable();
-		asm volatile ("nop");
 		irq_disable();
 
 		vmcb->control.intercept &= ~(1ULL << INTERCEPT_INTR);
@@ -1540,7 +1535,6 @@ static void virq_inject_test(struct svm_test *test)
 	}
 
 	irq_enable();
-	asm volatile ("nop");
 	irq_disable();
 
 	if (!virq_fired) {
@@ -1557,7 +1551,6 @@ static void virq_inject_test(struct svm_test *test)
 	}
 
 	irq_enable();
-	asm volatile ("nop");
 	irq_disable();
 
 	if (!virq_fired) {
@@ -1568,7 +1561,6 @@ static void virq_inject_test(struct svm_test *test)
 	vmmcall();
 
 	irq_enable();
-	asm volatile ("nop");
 	irq_disable();
 
 	if (virq_fired) {
@@ -1739,7 +1731,6 @@ static bool reg_corruption_finished(struct svm_test *test)
 		void* guest_rip = (void*)vmcb->save.rip;
 
 		irq_enable();
-		asm volatile ("nop");
 		irq_disable();
 
 		if (guest_rip == insb_instruction_label && io_port_var != 0xAA) {
diff --git a/x86/tscdeadline_latency.c b/x86/tscdeadline_latency.c
index a3bc4ea4..c54530dd 100644
--- a/x86/tscdeadline_latency.c
+++ b/x86/tscdeadline_latency.c
@@ -73,7 +73,6 @@ static void start_tsc_deadline_timer(void)
     irq_enable();
 
     wrmsr(MSR_IA32_TSCDEADLINE, rdmsr(MSR_IA32_TSC)+delta);
-    asm volatile ("nop");
 }
 
 static int enable_tsc_deadline_timer(void)
diff --git a/x86/vmx_tests.c b/x86/vmx_tests.c
index aa2ecbbc..c8e68931 100644
--- a/x86/vmx_tests.c
+++ b/x86/vmx_tests.c
@@ -1625,7 +1625,6 @@ static void interrupt_main(void)
 	apic_write(APIC_TMICT, 1000000);
 
 	irq_enable();
-	asm volatile ("nop");
 	vmcall();
 
 	report(rdtsc() - start > 10000 && timer_fired,
@@ -1639,7 +1638,6 @@ static void interrupt_main(void)
 	apic_write(APIC_TMICT, 1000000);
 
 	irq_enable();
-	asm volatile ("nop");
 	vmcall();
 
 	report(rdtsc() - start > 10000 && timer_fired,
@@ -1709,7 +1707,6 @@ static int interrupt_exit_handler(union exit_reason exit_reason)
 			handle_external_interrupt(vector);
 		} else {
 			irq_enable();
-			asm volatile ("nop");
 			irq_disable();
 		}
 		if (vmx_get_test_stage() >= 2)
@@ -6792,7 +6789,6 @@ static void test_x2apic_wr(
 
 		/* Clear the external interrupt. */
 		irq_enable();
-		asm volatile ("nop");
 		irq_disable();
 		report(handle_x2apic_ipi_ran,
 		       "Got pending interrupt after IRQ enabled.");
@@ -8543,7 +8539,6 @@ static void vmx_pending_event_test_core(bool guest_hlt)
 	       "Guest did not run before host received IPI");
 
 	irq_enable();
-	asm volatile ("nop");
 	irq_disable();
 	report(vmx_pending_event_ipi_fired,
 	       "Got pending interrupt after IRQ enabled");
@@ -9526,8 +9521,6 @@ static void vmx_hlt_with_rvi_guest(void)
 	handle_irq(HLT_WITH_RVI_VECTOR, vmx_hlt_with_rvi_guest_isr);
 
 	irq_enable();
-	asm volatile ("nop");
-
 	vmcall();
 }
 
