Index: kernel/arch/arm32/include/arch/mm/page.h
===================================================================
--- kernel/arch/arm32/include/arch/mm/page.h	(revision f9f758e8783cc8b9d957992e78eafdbed6d5584f)
+++ kernel/arch/arm32/include/arch/mm/page.h	(revision e13ba75c0bf5e01b37f70e52768e10b9d10c6d1b)
@@ -95,11 +95,11 @@
 /* Set PTE address accessors for each level. */
 #define SET_PTL0_ADDRESS_ARCH(ptl0) \
-        (set_ptl0_addr((pte_t *) (ptl0)))
+	set_ptl0_addr((pte_t *) (ptl0))
 #define SET_PTL1_ADDRESS_ARCH(ptl0, i, a) \
-        (((pte_t *) (ptl0))[(i)].l0.coarse_table_addr = (a) >> 10)
+	set_ptl1_addr((pte_t*) (ptl0), i, a)
 #define SET_PTL2_ADDRESS_ARCH(ptl1, i, a)
 #define SET_PTL3_ADDRESS_ARCH(ptl2, i, a)
 #define SET_FRAME_ADDRESS_ARCH(ptl3, i, a) \
-        (((pte_t *) (ptl3))[(i)].l1.frame_base_addr = (a) >> 12)
+	set_ptl3_addr((pte_t*) (ptl3), i, a)
 
 /* Get PTE flags accessors for each level. */
Index: kernel/arch/arm32/include/arch/mm/page_armv4.h
===================================================================
--- kernel/arch/arm32/include/arch/mm/page_armv4.h	(revision f9f758e8783cc8b9d957992e78eafdbed6d5584f)
+++ kernel/arch/arm32/include/arch/mm/page_armv4.h	(revision e13ba75c0bf5e01b37f70e52768e10b9d10c6d1b)
@@ -131,4 +131,14 @@
 {
 	TTBR0_write((uint32_t)pt);
+}
+
+NO_TRACE static inline void set_ptl1_addr(pte_t *pt, size_t i, uintptr_t address)
+{
+	pt[i].l0.coarse_table_addr = address >> 10;
+}
+
+NO_TRACE static inline void set_ptl3_addr(pte_t *pt, size_t i, uintptr_t address)
+{
+	pt[i].l1.frame_base_addr = address >> 12;
 }
 
Index: kernel/arch/arm32/include/arch/mm/page_armv6.h
===================================================================
--- kernel/arch/arm32/include/arch/mm/page_armv6.h	(revision f9f758e8783cc8b9d957992e78eafdbed6d5584f)
+++ kernel/arch/arm32/include/arch/mm/page_armv6.h	(revision e13ba75c0bf5e01b37f70e52768e10b9d10c6d1b)
@@ -127,4 +127,14 @@
 #define PTE_DESCRIPTOR_SMALL_PAGE_NX	3
 
+
+//TODO: DCCMVAU should be enough but it does not work.
+#define pt_coherence_m(pt, count) \
+do { \
+	for (unsigned i = 0; i < count; ++i) \
+		DCCMVAC_write((uintptr_t)(pt + i)); \
+	read_barrier(); \
+} while (0)
+#define pt_coherence(page) pt_coherence_m(page, 1)
+
 /** Sets the address of level 0 page table.
  *
@@ -135,4 +145,16 @@
 {
 	TTBR0_write((uint32_t)pt);
+}
+
+NO_TRACE static inline void set_ptl1_addr(pte_t *pt, size_t i, uintptr_t address)
+{
+	pt[i].l0.coarse_table_addr = address >> 10;
+	pt_coherence(&pt[i]);
+}
+
+NO_TRACE static inline void set_ptl3_addr(pte_t *pt, size_t i, uintptr_t address)
+{
+	pt[i].l1.frame_base_addr = address >> 12;
+	pt_coherence(&pt[i]);
 }
 
@@ -205,6 +227,5 @@
 		p->ns = 0;
 	}
-	DCCMVAC_write((uint32_t)p);
-	//TODO: DCCMVAU should be enough but it does not work.
+	pt_coherence(p);
 }
 
@@ -269,6 +290,5 @@
 			p->access_permission_1 = PTE_AP1_RO;
 	}
-	DCCMVAC_write((uint32_t)p);
-	//TODO: DCCMVAU should be enough but it does not work.
+	pt_coherence(p);
 }
 
@@ -281,6 +301,5 @@
 	write_barrier();
 	p->descriptor_type = PTE_DESCRIPTOR_COARSE_TABLE;
-	DCCMVAC_write((uint32_t)p);
-	//TODO: DCCMVAU should be enough but it does not work.
+	pt_coherence(p);
 }
 
@@ -290,6 +309,5 @@
 
 	p->descriptor_type = PTE_DESCRIPTOR_SMALL_PAGE;
-	DCCMVAC_write((uint32_t)p);
-	//TODO: DCCMVAU should be enough but it does not work.
+	pt_coherence(p);
 }