Index: kernel/arch/arm32/src/mm/tlb.c
===================================================================
--- kernel/arch/arm32/src/mm/tlb.c	(revision 8abcf4e7f08fa2a990c4bde86e31ad7865a13354)
+++ kernel/arch/arm32/src/mm/tlb.c	(revision bb75646c1e184874a4e6c6e604d37c3bc9608420)
@@ -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);
 }