Index: kernel/arch/arm32/src/mm/tlb.c
===================================================================
--- kernel/arch/arm32/src/mm/tlb.c	(revision 612edcab380c7fc950cf3a91c5d8a7f8d6f6a23b)
+++ kernel/arch/arm32/src/mm/tlb.c	(revision f3386d746b4f2e3d741eb9009428dbd331e2b6b1)
@@ -37,4 +37,5 @@
 #include <arch/mm/asid.h>
 #include <arch/asm.h>
+#include <arch/cp15.h>
 #include <typedefs.h>
 #include <arch/mm/page.h>
@@ -46,9 +47,5 @@
 void tlb_invalidate_all(void)
 {
-	asm volatile (
-		"eor r1, r1\n"
-		"mcr p15, 0, r1, c8, c7, 0\n"
-		::: "r1"
-	);
+	TLBIALL_write(0);
 }
 
@@ -60,4 +57,5 @@
 {
 	tlb_invalidate_all();
+	// TODO: why not TLBIASID_write(asid) ?
 }
 
@@ -65,11 +63,9 @@
  *
  * @param page Virtual adress of the page
- */ 
+ */
 static inline void invalidate_page(uintptr_t page)
 {
-	asm volatile (
-		"mcr p15, 0, %[page], c8, c7, 1\n"
-		:: [page] "r" (page)
-	);
+	TLBIMVA_write(page);
+	//TODO: What about TLBIMVAA?
 }