Index: kernel/genarch/src/mm/page_pt.c
===================================================================
--- kernel/genarch/src/mm/page_pt.c	(revision 1b478f661c486eaaf171a6561c652459502ed22f)
+++ kernel/genarch/src/mm/page_pt.c	(revision c72dc15e1268838fa6c71bd50186bc53b39ee999)
@@ -39,4 +39,5 @@
 #include <mm/page.h>
 #include <mm/frame.h>
+#include <mm/km.h>
 #include <mm/as.h>
 #include <arch/mm/page.h>
@@ -153,6 +154,6 @@
 	
 	/*
-	 * Second, free all empty tables along the way from PTL3 down to PTL0.
-	 *
+	 * Second, free all empty tables along the way from PTL3 down to PTL0
+	 * except those needed for sharing the kernel non-identity mappings.
 	 */
 	
@@ -171,8 +172,7 @@
 		/*
 		 * PTL3 is empty.
-		 * Release the frame and remove PTL3 pointer from preceding table.
-		 *
-		 */
-		frame_free(KA2PA((uintptr_t) ptl3));
+		 * Release the frame and remove PTL3 pointer from the parent
+		 * table.
+		 */
 #if (PTL2_ENTRIES != 0)
 		memsetb(&ptl2[PTL2_INDEX(page)], sizeof(pte_t), 0);
@@ -180,6 +180,10 @@
 		memsetb(&ptl1[PTL1_INDEX(page)], sizeof(pte_t), 0);
 #else
+		if (km_is_non_identity(page))
+			return;
+
 		memsetb(&ptl0[PTL0_INDEX(page)], sizeof(pte_t), 0);
 #endif
+		frame_free(KA2PA((uintptr_t) ptl3));
 	} else {
 		/*
@@ -204,13 +208,16 @@
 		/*
 		 * PTL2 is empty.
-		 * Release the frame and remove PTL2 pointer from preceding table.
-		 *
-		 */
-		frame_free(KA2PA((uintptr_t) ptl2));
+		 * Release the frame and remove PTL2 pointer from the parent
+		 * table.
+		 */
 #if (PTL1_ENTRIES != 0)
 		memsetb(&ptl1[PTL1_INDEX(page)], sizeof(pte_t), 0);
 #else
+		if (km_is_non_identity(page))
+			return;
+
 		memsetb(&ptl0[PTL0_INDEX(page)], sizeof(pte_t), 0);
 #endif
+		frame_free(KA2PA((uintptr_t) ptl2));
 	} else {
 		/*
@@ -236,9 +243,12 @@
 		/*
 		 * PTL1 is empty.
-		 * Release the frame and remove PTL1 pointer from preceding table.
-		 *
-		 */
+		 * Release the frame and remove PTL1 pointer from the parent
+		 * table.
+		 */
+		if (km_is_non_identity(page))
+			return;
+
+		memsetb(&ptl0[PTL0_INDEX(page)], sizeof(pte_t), 0);
 		frame_free(KA2PA((uintptr_t) ptl1));
-		memsetb(&ptl0[PTL0_INDEX(page)], sizeof(pte_t), 0);
 	}
 #endif /* PTL1_ENTRIES != 0 */