diff --git a/kernel/arch/i386/klib.S b/kernel/arch/i386/klib.S
index a2488d2fa..c60046c64 100644
--- a/kernel/arch/i386/klib.S
+++ b/kernel/arch/i386/klib.S
@@ -803,11 +803,9 @@ ENTRY(__switch_address_space)
 	 * test if the cr3 is loaded with the current value to avoid unnecessary
 	 * TLB flushes
 	 */
-#ifndef CONFIG_SMP
 	mov	%cr3, %ecx
 	cmp	%ecx, %eax
 	je	0f
-#endif
 	mov	%eax, %cr3
 	/* get ptproc */
 	mov	8(%esp), %eax
diff --git a/kernel/proc.c b/kernel/proc.c
index 438b43c39..80c7614c1 100644
--- a/kernel/proc.c
+++ b/kernel/proc.c
@@ -242,6 +242,9 @@ PUBLIC void switch_to_user(void)
 	 * to be scheduled again.
 	 */
 	struct proc * p;
+#ifdef CONFIG_SMP
+	int tlb_must_refresh = 0;
+#endif
 
 	p = get_cpulocal_var(proc_ptr);
 	/*
@@ -279,6 +282,10 @@ not_runnable_pick_new:
 	/* update the global variable */
 	get_cpulocal_var(proc_ptr) = p;
 
+#ifdef CONFIG_SMP
+	if (p->p_misc_flags & MF_FLUSH_TLB && get_cpulocal_var(ptproc) == p)
+		tlb_must_refresh = 1;
+#endif
 	switch_address_space(p);
 
 check_misc_flags:
@@ -385,7 +392,11 @@ check_misc_flags:
 
   	assert(!(p->p_misc_flags & MF_FULLVM) || p->p_seg.p_cr3 != 0);
 #ifdef CONFIG_SMP
-	refresh_tlb();
+	if (p->p_misc_flags & MF_FLUSH_TLB) {
+		if (tlb_must_refresh)
+			refresh_tlb();
+		p->p_misc_flags &= ~MF_FLUSH_TLB;
+	}
 #endif
 	
 	restart_local_timer();
diff --git a/kernel/proc.h b/kernel/proc.h
index 3055a0821..dfc332698 100644
--- a/kernel/proc.h
+++ b/kernel/proc.h
@@ -242,6 +242,9 @@ struct proc {
 #define MF_SENDING_FROM_KERNEL	0x2000 /* message of this process is from kernel */
 #define MF_CONTEXT_SET	0x4000 /* don't touch context */
 #define MF_SPROF_SEEN	0x8000 /* profiling has seen this process */
+#define MF_FLUSH_TLB	0x10000	/* if set, TLB must be flushed before letting
+				   this process run again. Currently it only
+				   applies to SMP */
 
 /* Magic process table addresses. */
 #define BEG_PROC_ADDR (&proc[0])
diff --git a/kernel/system/do_vmctl.c b/kernel/system/do_vmctl.c
index 37f85333d..2f10157cd 100644
--- a/kernel/system/do_vmctl.c
+++ b/kernel/system/do_vmctl.c
@@ -148,6 +148,9 @@ PUBLIC int do_vmctl(struct proc * caller, message * m_ptr)
 		} else
 #endif
 			RTS_SET(p, RTS_VMINHIBIT);
+#if CONFIG_SMP
+		p->p_misc_flags |= MF_FLUSH_TLB;
+#endif
 		return OK;
 	case VMCTL_VMINHIBIT_CLEAR:
 		assert(RTS_ISSET(p, RTS_VMINHIBIT));