diff --git a/xen/common/dom0_ops.c b/xen/common/dom0_ops.c
index 829eb1de2e..09b9d5d2d5 100644
--- a/xen/common/dom0_ops.c
+++ b/xen/common/dom0_ops.c
@@ -271,7 +271,8 @@ long do_dom0_op(dom0_op_t *u_dom0_op)
         else
         {
             domain_pause(d);
-            if(d->processor != cpu % smp_num_cpus)
+            synchronise_pagetables(~0UL);
+            if ( d->processor != (cpu % smp_num_cpus) )
                 set_bit(DF_MIGRATED, &d->flags);
             set_bit(DF_CPUPINNED, &d->flags);
             d->processor = cpu % smp_num_cpus;