diff --git a/xen/arch/x86/domain.c b/xen/arch/x86/domain.c
index 25746ab4f1..759bbadb21 100644
--- a/xen/arch/x86/domain.c
+++ b/xen/arch/x86/domain.c
@@ -738,9 +738,6 @@ void context_switch(struct vcpu *prev, struct vcpu *next)
     ASSERT(cpus_weight(dirty_mask) <= 1);
     if ( unlikely(!cpu_isset(cpu, dirty_mask) && !cpus_empty(dirty_mask)) )
     {
-        /* Make sure the next VCPU is not in a scheduling tail. */
-        while ( test_bit(_VCPUF_running, &next->vcpu_flags) )
-            cpu_relax();
         /* Other cpus call __sync_lazy_execstate from flush ipi handler. */
         if ( !cpus_empty(next->vcpu_dirty_cpumask) )
             flush_tlb_mask(next->vcpu_dirty_cpumask);
diff --git a/xen/common/schedule.c b/xen/common/schedule.c
index 94b40559da..0ffa53a8fa 100644
--- a/xen/common/schedule.c
+++ b/xen/common/schedule.c
@@ -420,6 +420,7 @@ static void __enter_scheduler(void)
     }
 #endif
 
+    ASSERT(!test_bit(_VCPUF_running, &next->vcpu_flags));
     set_bit(_VCPUF_running, &next->vcpu_flags);
 
     spin_unlock_irq(&schedule_data[cpu].schedule_lock);