Index: kernel/arch/arm32/include/arch/mm/page_armv6.h
===================================================================
--- kernel/arch/arm32/include/arch/mm/page_armv6.h	(revision 67d02bb8fda469f70542624619590e4d5c41b6a4)
+++ kernel/arch/arm32/include/arch/mm/page_armv6.h	(revision 186b9195d64d41f1b30ec34912623fe11231a18a)
@@ -233,20 +233,25 @@
 			p->descriptor_type = PTE_DESCRIPTOR_SMALL_PAGE_NX;
 	}
-	
-	/* tex=0 buf=1 and cache=1 => normal memory
-	 * tex=0 buf=1 and cache=0 => shareable device mmio
-	 */
 
 	if (flags & PAGE_CACHEABLE) {
+		/*
+		 * Write-back, write-allocate memory, see ch. B3.8.2
+		 * (p. B3-1358) of ARM Architecture reference manual.
+		 */
 		p->tex = 1;
 		p->cacheable = 1;
+		p->bufferable = 1;
 	} else {
+		/*
+		 * Shareable device memory, see ch. B3.8.2 (p. B3-1358) of
+		 * ARM Architecture reference manual.
+		 */
 		p->tex = 0;
 		p->cacheable = 0;
+		p->bufferable = 1;
 	}
-	p->bufferable = 1;
 	
 	/* Shareable is ignored for devices (non-cacheable),
-	 * turn it on for normal memory. */
+	 * turn it off for normal memory. */
 	p->shareable = 0;