Index: kernel/arch/arm32/src/mm/tlb.c
===================================================================
--- kernel/arch/arm32/src/mm/tlb.c	(revision 74dcc07b9461a25cd636e0895ebb5da941fb869f)
+++ kernel/arch/arm32/src/mm/tlb.c	(revision 24bb3632111f42b0ff5312ef96963e972cd4ca9e)
@@ -40,4 +40,5 @@
 #include <typedefs.h>
 #include <arch/mm/page.h>
+#include <arch/cache.h>
 
 /** Invalidate all entries in TLB.
@@ -48,4 +49,16 @@
 {
 	TLBIALL_write(0);
+	/*
+	 * "A TLB maintenance operation is only guaranteed to be complete after
+	 * the execution of a DSB instruction."
+	 * "An ISB instruction, or a return from an exception, causes the
+	 * effect of all completed TLB maintenance operations that appear in
+	 * program order before the ISB or return from exception to be visible
+	 * to all subsequent instructions, including the instruction fetches
+	 * for those instructions."
+	 * ARM Architecture reference Manual ch. B3.10.1 p. B3-1374 B3-1375
+	 */
+	read_barrier();
+	inst_barrier();
 }
 
@@ -66,6 +79,18 @@
 static inline void invalidate_page(uintptr_t page)
 {
+	//TODO: What about TLBIMVAA?
 	TLBIMVA_write(page);
-	//TODO: What about TLBIMVAA?
+	/*
+	 * "A TLB maintenance operation is only guaranteed to be complete after
+	 * the execution of a DSB instruction."
+	 * "An ISB instruction, or a return from an exception, causes the
+	 * effect of all completed TLB maintenance operations that appear in
+	 * program order before the ISB or return from exception to be visible
+	 * to all subsequent instructions, including the instruction fetches
+	 * for those instructions."
+	 * ARM Architecture reference Manual ch. B3.10.1 p. B3-1374 B3-1375
+	 */
+	read_barrier();
+	inst_barrier();
 }
 
@@ -79,7 +104,5 @@
 void tlb_invalidate_pages(asid_t asid __attribute__((unused)), uintptr_t page, size_t cnt)
 {
-	unsigned int i;
-
-	for (i = 0; i < cnt; i++)
+	for (unsigned i = 0; i < cnt; i++)
 		invalidate_page(page + i * PAGE_SIZE);
 }