diff --git a/kern/arch/riscv/process.c b/kern/arch/riscv/process.c
index 7b72d2e..47d0f5d 100644
--- a/kern/arch/riscv/process.c
+++ b/kern/arch/riscv/process.c
@@ -65,3 +65,7 @@
 	proc_decref(pcpui->cur_proc);
 	pcpui->cur_proc = 0;
 }
+
+void __clear_owning_proc(uint32_t coreid)
+{
+}
diff --git a/kern/arch/x86/process64.c b/kern/arch/x86/process64.c
index 810d453..9ad7ba5 100644
--- a/kern/arch/x86/process64.c
+++ b/kern/arch/x86/process64.c
@@ -341,7 +341,11 @@
 	struct per_cpu_info *pcpui = &per_cpu_info[core_id()];
 
 	lcr3(boot_cr3);
-	vmx_clear_vmcs();
 	proc_decref(pcpui->cur_proc);
 	pcpui->cur_proc = 0;
 }
+
+void __clear_owning_proc(uint32_t coreid)
+{
+	vmx_clear_vmcs();
+}
diff --git a/kern/include/process.h b/kern/include/process.h
index 1ccab3b..b2d7bf1 100644
--- a/kern/include/process.h
+++ b/kern/include/process.h
@@ -175,6 +175,7 @@
                    uintptr_t stack_top, uintptr_t tls_desc);
 void proc_secure_ctx(struct user_context *ctx);
 void __abandon_core(void);
+void __clear_owning_proc(uint32_t coreid);
 
 /* Degubbing */
 void print_allpids(void);
diff --git a/kern/src/kthread.c b/kern/src/kthread.c
index 518f37a..59db13c 100644
--- a/kern/src/kthread.c
+++ b/kern/src/kthread.c
@@ -154,7 +154,13 @@
 			proc_decref(kthread->proc);
 			kthread->proc = 0;
 		} else {
-			/* Load our page tables before potentially decreffing cur_proc */
+			/* Load our page tables before potentially decreffing cur_proc.
+			 *
+			 * We don't need to do an EPT flush here.  The EPT is flushed and
+			 * managed in sync with the VMCS.  We won't run a different VM (and
+			 * thus *need* a different EPT) without first removing the old GPC,
+			 * which ultimately will result in a flushed EPT (on x86, this
+			 * actually happens when we clear_owning_proc()). */
 			lcr3(kthread->proc->env_cr3);
 			/* Might have to clear out an existing current.  If they need to be
 			 * set later (like in restartcore), it'll be done on demand. */
diff --git a/kern/src/process.c b/kern/src/process.c
index 43a18c0..5ef5ee3 100644
--- a/kern/src/process.c
+++ b/kern/src/process.c
@@ -1798,6 +1798,8 @@
 {
 	struct per_cpu_info *pcpui = &per_cpu_info[coreid];
 	struct proc *p = pcpui->owning_proc;
+
+	__clear_owning_proc(coreid);
 	pcpui->owning_proc = 0;
 	pcpui->owning_vcoreid = 0xdeadbeef;
 	pcpui->cur_ctx = 0;			/* catch bugs for now (may go away) */