diff --git a/xen/arch/x86/domain_page.c b/xen/arch/x86/domain_page.c
index 158a1645d7..9bdab61354 100644
--- a/xen/arch/x86/domain_page.c
+++ b/xen/arch/x86/domain_page.c
@@ -31,6 +31,14 @@ static inline struct vcpu *mapcache_current_vcpu(void)
     if ( v == (struct vcpu *)0xfffff000 )
         return NULL;
 
+    /*
+     * When using efi runtime page tables, we have the equivalent of the idle
+     * domain's page tables but current may point at another domain's VCPU.
+     * Return NULL as though current is not properly set up yet.
+     */
+    if ( efi_enabled && efi_rs_using_pgtables() )
+        return NULL;
+
     /*
      * If guest_table is NULL, and we are running a paravirtualised guest,
      * then it means we are running on the idle domain's page table and must
@@ -38,14 +46,11 @@ static inline struct vcpu *mapcache_current_vcpu(void)
      */
     if ( unlikely(pagetable_is_null(v->arch.guest_table)) && is_pv_vcpu(v) )
     {
-        unsigned long cr3;
-
         /* If we really are idling, perform lazy context switch now. */
         if ( (v = idle_vcpu[smp_processor_id()]) == current )
             sync_local_execstate();
         /* We must now be running on the idle page table. */
-        ASSERT((cr3 = read_cr3()) == __pa(idle_pg_table) ||
-               (efi_enabled && cr3 == efi_rs_page_table()));
+        ASSERT(read_cr3() == __pa(idle_pg_table));
     }
 
     return v;
diff --git a/xen/arch/x86/efi/stub.c b/xen/arch/x86/efi/stub.c
index 627009f430..07c2bd0c6e 100644
--- a/xen/arch/x86/efi/stub.c
+++ b/xen/arch/x86/efi/stub.c
@@ -12,7 +12,7 @@ void __init efi_init_memory(void) { }
 
 void efi_update_l4_pgtable(unsigned int l4idx, l4_pgentry_t l4e) { }
 
-paddr_t efi_rs_page_table(void)
+bool_t efi_rs_using_pgtables(void)
 {
     BUG();
     return 0;
diff --git a/xen/common/efi/runtime.c b/xen/common/efi/runtime.c
index f5df51e7c7..088f0cb12d 100644
--- a/xen/common/efi/runtime.c
+++ b/xen/common/efi/runtime.c
@@ -30,6 +30,7 @@ const CHAR16 *__read_mostly efi_fw_vendor;
 const EFI_RUNTIME_SERVICES *__read_mostly efi_rs;
 #ifndef CONFIG_ARM /* TODO - disabled until implemented on ARM */
 static DEFINE_SPINLOCK(efi_rs_lock);
+static unsigned int efi_rs_on_cpu = NR_CPUS;
 #endif
 
 UINTN __read_mostly efi_memmap_size;
@@ -65,6 +66,8 @@ unsigned long efi_rs_enter(void)
 
     spin_lock(&efi_rs_lock);
 
+    efi_rs_on_cpu = smp_processor_id();
+
     /* prevent fixup_page_fault() from doing anything */
     irq_enter();
 
@@ -99,13 +102,16 @@ void efi_rs_leave(unsigned long cr3)
         asm volatile ( "lgdt %0" : : "m" (gdt_desc) );
     }
     irq_exit();
+    efi_rs_on_cpu = NR_CPUS;
     spin_unlock(&efi_rs_lock);
     stts();
 }
 
-paddr_t efi_rs_page_table(void)
+bool_t efi_rs_using_pgtables(void)
 {
-    return efi_l4_pgtable ? virt_to_maddr(efi_l4_pgtable) : 0;
+    return efi_l4_pgtable &&
+           (smp_processor_id() == efi_rs_on_cpu) &&
+           (read_cr3() == virt_to_maddr(efi_l4_pgtable));
 }
 
 unsigned long efi_get_time(void)
diff --git a/xen/include/xen/efi.h b/xen/include/xen/efi.h
index 5e02724572..f2782ce3e4 100644
--- a/xen/include/xen/efi.h
+++ b/xen/include/xen/efi.h
@@ -28,7 +28,7 @@ struct xenpf_efi_runtime_call;
 struct compat_pf_efi_runtime_call;
 
 void efi_init_memory(void);
-paddr_t efi_rs_page_table(void);
+bool_t efi_rs_using_pgtables(void);
 unsigned long efi_get_time(void);
 void efi_halt_system(void);
 void efi_reset_system(bool_t warm);