diff --git a/core/cpu.c b/core/cpu.c
index 050cc169..fb7d93c2 100644
--- a/core/cpu.c
+++ b/core/cpu.c
@@ -367,6 +367,11 @@ int cpu_vmx_execute(struct vcpu_t *vcpu, struct hax_tunnel *htun)
             hax_panic_log(vcpu);
             return 0;
         }
+        if( vcpu->check_pae_pdpt ) {
+          vcpu->check_pae_pdpt = 0;
+          if( !vcpu_check_pae_pdpte(vcpu) )
+            return 0;
+        }
         vcpu_handle_vmcs_pending(vcpu);
         vcpu_inject_intr(vcpu, htun);
 
diff --git a/core/include/vcpu.h b/core/include/vcpu.h
index c81349b7..7fc3ec02 100644
--- a/core/include/vcpu.h
+++ b/core/include/vcpu.h
@@ -200,7 +200,8 @@ struct vcpu_t {
         uint64_t interruptibility_dirty          : 1;
         uint64_t pcpu_ctls_dirty                 : 1;
         uint64_t pae_pdpt_dirty                  : 1;
-        uint64_t padding                         : 45;
+        uint64_t check_pae_pdpt                  : 1;
+        uint64_t padding                         : 44;
     };
 
     /* For TSC offseting feature*/
@@ -290,5 +291,5 @@ static inline bool valid_vcpu_id(int vcpu_id)
 
 bool vcpu_is_panic(struct vcpu_t *vcpu);
 void vcpu_set_panic(struct vcpu_t *vcpu);
-
+int vcpu_check_pae_pdpte(struct vcpu_t *vcpu);
 #endif  // HAX_CORE_VCPU_H_
diff --git a/core/vcpu.c b/core/vcpu.c
index d0a145bc..18ad42dd 100644
--- a/core/vcpu.c
+++ b/core/vcpu.c
@@ -608,6 +608,7 @@ static void vcpu_init(struct vcpu_t *vcpu)
     state->_dr6 = DR6_SETBITS;
     state->_dr7 = DR7_SETBITS;
     vcpu->dr_dirty = 1;
+    vcpu->check_pae_pdpt = 0;
 
     // Initialize guest MSR state, i.e. a list of MSRs and their initial values.
     // Note that all zeros is not a valid state (see below). At the first VM
@@ -3699,6 +3700,7 @@ static int handle_msr_write(struct vcpu_t *vcpu, uint32_t msr, uint64_t val,
             } else {
                 vmwrite_efer(vcpu);
             }
+            vcpu->check_pae_pdpt = 1;
             break;
         }
         case IA32_STAR:
@@ -4131,6 +4133,7 @@ int vcpu_set_regs(struct vcpu_t *vcpu, struct vcpu_state_t *ustate)
         hax_panic_log(vcpu);
     }
 
+    vcpu->check_pae_pdpt = 1;
     return 0;
 }
 
@@ -4432,3 +4435,31 @@ static bool vcpu_is_bsp(struct vcpu_t *vcpu)
     // TODO: add an API to set bootstrap processor
     return (vcpu->vm->bsp_vcpu_id == vcpu->vcpu_id);
 }
+int vcpu_check_pae_pdpte(struct vcpu_t *vcpu)
+{
+    struct vcpu_state_t *state = vcpu->state;
+    if ((state->_cr0 & CR0_PG) && (state->_cr4 & CR4_PAE) &&
+        !(state->_efer & IA32_EFER_LME) && !vtlb_active(vcpu) ) {
+        // The vCPU is either about to enter PAE paging mode (see IASDM
+        // Vol. 3A 4.1.2, Figure 4-1) and needs to load its PDPTE
+        // registers, or already in PAE mode and needs to reload those
+        // registers
+        int ret = vcpu_prepare_pae_pdpt(vcpu);
+        if (ret) {
+            vcpu_set_panic(vcpu);
+            hax_log(HAX_LOGPANIC, "vCPU #%u failed to (re)load PDPT for"
+                    " EPT+PAE mode: ret=%d\n", vcpu->vcpu_id, ret);
+            dump_vmcs(vcpu);
+            return 0;
+        }
+
+        if (vcpu->pae_pdpt_dirty) {
+            vmwrite(vcpu, GUEST_PDPTE0, vcpu->pae_pdptes[0]);
+            vmwrite(vcpu, GUEST_PDPTE1, vcpu->pae_pdptes[1]);
+            vmwrite(vcpu, GUEST_PDPTE2, vcpu->pae_pdptes[2]);
+            vmwrite(vcpu, GUEST_PDPTE3, vcpu->pae_pdptes[3]);
+            vcpu->pae_pdpt_dirty = 0;
+        }
+    }
+    return 1;
+}