diff --git a/arch/x86/kernel/include/arch/mm.h b/arch/x86/kernel/include/arch/mm.h
new file mode 100644
index 00000000..8b3c4d8a
--- /dev/null
+++ b/arch/x86/kernel/include/arch/mm.h
@@ -0,0 +1,16 @@
+#ifndef __ARCH_MM_H
+#define __ARCH_MM_H
+
+struct process_vm;
+
+static inline void
+flush_nfo_tlb()
+{
+}
+
+static inline void
+flush_nfo_tlb_mm(struct process_vm *vm)
+{
+}
+
+#endif
diff --git a/kernel/process.c b/kernel/process.c
index 70f9d3d1..5eb29e80 100644
--- a/kernel/process.c
+++ b/kernel/process.c
@@ -2083,6 +2083,7 @@ release_process_vm(struct process_vm *vm)
 	if(vm->free_cb)
 		vm->free_cb(vm, vm->opt);
 
+	flush_nfo_tlb_mm(vm);
 	free_all_process_memory_range(vm);
 
 	detach_address_space(vm->address_space, vm->proc->pid);
diff --git a/kernel/syscall.c b/kernel/syscall.c
index ba1d0d19..ba03d427 100644
--- a/kernel/syscall.c
+++ b/kernel/syscall.c
@@ -973,6 +973,8 @@ do_mmap(const intptr_t addr0, const size_t len0, const int prot,
 		}
 	}
 
+	flush_nfo_tlb();
+
 	ihk_mc_spinlock_lock_noirq(&thread->vm->memory_range_lock);
 
 	if (flags & MAP_FIXED) {
@@ -1258,6 +1260,8 @@ SYSCALL_DECLARE(mprotect)
 		return 0;
 	}
 
+	flush_nfo_tlb();
+
 	ihk_mc_spinlock_lock_noirq(&thread->vm->memory_range_lock);
 
 	first = lookup_process_memory_range(thread->vm, start, start+PAGE_SIZE);
@@ -1364,6 +1368,8 @@ SYSCALL_DECLARE(brk)
 	dkprintf("SC(%d)[sys_brk] brk_start=%lx,end=%lx\n",
 			ihk_mc_get_processor_id(), region->brk_start, region->brk_end);
 
+	flush_nfo_tlb();
+
 	/* brk change fail, including glibc trick brk(0) to obtain current brk */
 	if(address < region->brk_start) {
 		r = region->brk_end;
@@ -6354,6 +6360,8 @@ SYSCALL_DECLARE(remap_file_pages)
 		goto out;
 	}
 
+	flush_nfo_tlb();
+
 	range->flag |= VR_FILEOFF;
 	error = remap_process_memory_range(thread->vm, range, start, end, off);
 	if (error) {
diff --git a/lib/include/ihk/mm.h b/lib/include/ihk/mm.h
index 39d114f9..d17b4375 100644
--- a/lib/include/ihk/mm.h
+++ b/lib/include/ihk/mm.h
@@ -18,6 +18,7 @@
 #include <memory.h>
 #include <ihk/lock.h>
 #include <ihk/atomic.h>
+#include <arch/mm.h>
 
 struct memobj;
 struct process_vm;