Index: kernel/genarch/src/mm/page_ht.c
===================================================================
--- kernel/genarch/src/mm/page_ht.c	(revision 702536882b248833b02d3693809a7bb0f21bcbd1)
+++ kernel/genarch/src/mm/page_ht.c	(revision 3b8a9907a4d66e672bf96c07661354131bae092f)
@@ -209,4 +209,8 @@
 		pte->frame = ALIGN_DOWN(frame, FRAME_SIZE);
 
+		/*
+		 * Make sure that a concurrent ht_mapping_find() will see the
+		 * new entry only after it is fully initialized.
+		 */
 		write_barrier();
 		
Index: kernel/genarch/src/mm/page_pt.c
===================================================================
--- kernel/genarch/src/mm/page_pt.c	(revision 702536882b248833b02d3693809a7bb0f21bcbd1)
+++ kernel/genarch/src/mm/page_pt.c	(revision 3b8a9907a4d66e672bf96c07661354131bae092f)
@@ -89,4 +89,9 @@
 		    PAGE_NOT_PRESENT | PAGE_USER | PAGE_EXEC | PAGE_CACHEABLE |
 		    PAGE_WRITE);
+		/*
+		 * Make sure that a concurrent hardware page table walk or
+		 * pt_mapping_find() will see the new PTL1 only after it is
+		 * fully initialized.
+		 */
 		write_barrier();
 		SET_PTL1_PRESENT(ptl0, PTL0_INDEX(page));
@@ -103,4 +108,7 @@
 		    PAGE_NOT_PRESENT | PAGE_USER | PAGE_EXEC | PAGE_CACHEABLE |
 		    PAGE_WRITE);
+		/*
+		 * Make the new PTL2 visible only after it is fully initialized.
+		 */
 		write_barrier();
 		SET_PTL2_PRESENT(ptl1, PTL1_INDEX(page));	
@@ -117,4 +125,7 @@
 		    PAGE_NOT_PRESENT | PAGE_USER | PAGE_EXEC | PAGE_CACHEABLE |
 		    PAGE_WRITE);
+		/*
+		 * Make the new PTL3 visible only after it is fully initialized.
+		 */
 		write_barrier();
 		SET_PTL3_PRESENT(ptl2, PTL2_INDEX(page));
@@ -125,4 +136,7 @@
 	SET_FRAME_ADDRESS(ptl3, PTL3_INDEX(page), frame);
 	SET_FRAME_FLAGS(ptl3, PTL3_INDEX(page), flags | PAGE_NOT_PRESENT);
+	/*
+	 * Make the new mapping visible only after it is fully initialized.
+	 */
 	write_barrier();
 	SET_FRAME_PRESENT(ptl3, PTL3_INDEX(page));
@@ -296,4 +310,7 @@
 
 #if (PTL1_ENTRIES != 0)
+	/*
+	 * Always read ptl2 only after we are sure it is present.
+	 */
 	read_barrier();
 #endif
@@ -304,4 +321,7 @@
 
 #if (PTL2_ENTRIES != 0)
+	/*
+	 * Always read ptl3 only after we are sure it is present.
+	 */
 	read_barrier();
 #endif