diff --git a/include/plat/pc99/plat/64/plat_mode/machine/hardware.h b/include/plat/pc99/plat/64/plat_mode/machine/hardware.h
index 8ee5355b7..dc39eebaf 100644
--- a/include/plat/pc99/plat/64/plat_mode/machine/hardware.h
+++ b/include/plat/pc99/plat/64/plat_mode/machine/hardware.h
@@ -48,7 +48,12 @@
 /* Define the top of our static 'kernel window', which is the top 1GiB of memory */
 #define PADDR_HIGH_TOP (PPTR_KDEV - KERNEL_BASE)
 
-#define PPTR_USER_TOP KERNEL_BASE
+/* Below the main kernel window we have any slots for the TLB bitmap */
+#define TLBBITMAP_PML4_RESERVED (TLBBITMAP_ROOT_ENTRIES * BIT(PML4_INDEX_OFFSET))
+#define TLBBITMAP_PPTR (PPTR_BASE - TLBBITMAP_PML4_RESERVED)
+
+/* The start of the this TLB bitmap becomes the highest valid user address */
+#define PPTR_USER_TOP TLBBITMAP_PPTR
 #define KERNEL_BASE_OFFSET (KERNEL_BASE - PADDR_BASE)
 #define kernelBase KERNEL_BASE
 
diff --git a/src/arch/x86/64/kernel/vspace.c b/src/arch/x86/64/kernel/vspace.c
index 15b228e40..d75786c7e 100644
--- a/src/arch/x86/64/kernel/vspace.c
+++ b/src/arch/x86/64/kernel/vspace.c
@@ -19,6 +19,7 @@
 #include <arch/kernel/boot.h>
 #include <arch/api/invocation.h>
 #include <mode/kernel/tlb.h>
+#include <arch/kernel/tlb_bitmap.h>
 
 struct lookupPML4Slot_ret {
     exception_t status;
@@ -253,6 +254,11 @@ map_kernel_window(
         return false;
     }
 
+#if CONFIG_MAX_NUM_NODES > 1
+    /* initialize the TLB bitmap */
+    tlb_bitmap_init(x64KSGlobalPML4);
+#endif /* CONFIG_MAX_NUM_NODES */
+
     /* In boot code, so fine to just trash everything here */
     invalidateLocalTranslationAll();
     printf("Mapping kernel window is done\n");
@@ -724,7 +730,11 @@ void copyGlobalMappings(vspace_root_t *new_vspace)
     unsigned long i;
     pml4e_t *vspace = (pml4e_t *)new_vspace;
 
-    for (i = GET_PML4_INDEX(PPTR_BASE); i < BIT(PML4_INDEX_BITS); i++) {
+    /* Copy from the user top so that we copy the default entries of the
+     * tlb bitmap (if it exists). If it doesn't exist then this loop
+     * will be equivalent to copying from PPTR_BASE
+     */
+    for (i = GET_PML4_INDEX(PPTR_USER_TOP); i < BIT(PML4_INDEX_BITS); i++) {
         vspace[i] = x64KSGlobalPML4[i];
     }
 }