Index: kernel/genarch/src/mm/page_pt.c
===================================================================
--- kernel/genarch/src/mm/page_pt.c	(revision f061e40457bcea583cf7b5dcf8f060bb2895c00f)
+++ kernel/genarch/src/mm/page_pt.c	(revision 375e501a4e8faac7fad7a1d019a8a778e97346e6)
@@ -48,4 +48,5 @@
 #include <align.h>
 #include <macros.h>
+#include <bitops.h>
 
 static void pt_mapping_insert(as_t *, uintptr_t, uintptr_t, unsigned int);
@@ -292,4 +293,18 @@
 }
 
+/** Return the size of the region mapped by a single PTL0 entry.
+ *
+ * @return Size of the region mapped by a single PTL0 entry.
+ */
+static uintptr_t ptl0_step_get(void)
+{
+	size_t va_bits;
+
+	va_bits = fnzb(PTL0_ENTRIES) + fnzb(PTL1_ENTRIES) + fnzb(PTL2_ENTRIES) +
+	    fnzb(PTL3_ENTRIES) + PAGE_WIDTH;
+
+	return 1UL << (va_bits - fnzb(PTL0_ENTRIES));
+}
+
 /** Make the mappings in the given range global accross all address spaces.
  *
@@ -309,5 +324,5 @@
 {
 	uintptr_t ptl0 = PA2KA((uintptr_t) AS_KERNEL->genarch.page_table);
-	uintptr_t ptl0step = (((uintptr_t) -1) / PTL0_ENTRIES) + 1;
+	uintptr_t ptl0_step = ptl0_step_get();
 	size_t order;
 	uintptr_t addr;
@@ -321,9 +336,8 @@
 #endif
 
-	ASSERT(ispwr2(ptl0step));
 	ASSERT(size > 0);
 
-	for (addr = ALIGN_DOWN(base, ptl0step); addr - 1 < base + size - 1;
-	    addr += ptl0step) {
+	for (addr = ALIGN_DOWN(base, ptl0_step); addr - 1 < base + size - 1;
+	    addr += ptl0_step) {
 		uintptr_t l1;