diff --git a/config.cmake b/config.cmake
index 07a298c91..2a5a0518c 100644
--- a/config.cmake
+++ b/config.cmake
@@ -198,6 +198,7 @@ endif()
 
 # Enshrine common variables in the config
 config_set(KernelHaveFPU HAVE_FPU "${KernelHaveFPU}")
+config_set(KernelPaddrUserTop PADDR_USER_DEVICE_TOP "${KernelPaddrUserTop}")
 
 # System parameters
 config_string(
diff --git a/include/arch/arm/arch/bootinfo.h b/include/arch/arm/arch/bootinfo.h
new file mode 100644
index 000000000..a8832585d
--- /dev/null
+++ b/include/arch/arm/arch/bootinfo.h
@@ -0,0 +1,30 @@
+/*
+ * Copyright 2019, Data61
+ * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+ * ABN 41 687 119 230.
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(DATA61_GPL)
+ */
+
+#ifndef __ARCH_BOOTINFO_H
+#define __ARCH_BOOTINFO_H
+
+/* Modifiers:
+ *  + 1: allow the kernel to release its own boot data region
+ *  + 1: possible gap between ELF images and rootserver objects;
+ *       see arm/arch_init_freemem */
+#define MAX_NUM_FREEMEM_REG (ARRAY_SIZE(avail_p_regs) + MODE_RESERVED + 1 + 1)
+
+/* The maximum number of reserved regions is:
+ * - 1 for each physical memory region (MAX_NUM_FREEMEM_REG)
+ * - 1 for each kernel device (ARRAY_SIZE(kernel_devices))
+ * - 1 for each mode-reserved region. (MODE_RESERVED)
+ * - 1 each for kernel, dtb, and user image. (3)
+ */
+#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + ARRAY_SIZE(kernel_devices) + MODE_RESERVED + 3)
+
+#endif
diff --git a/include/arch/arm/arch/types.h b/include/arch/arm/arch/types.h
index f6565e326..678d24ac2 100644
--- a/include/arch/arm/arch/types.h
+++ b/include/arch/arm/arch/types.h
@@ -52,6 +52,7 @@ typedef struct kernel_frame {
     paddr_t paddr;
     pptr_t pptr;
     int armExecuteNever;
+    int userAvailable;
 } kernel_frame_t;
 
 #endif
diff --git a/include/arch/riscv/arch/bootinfo.h b/include/arch/riscv/arch/bootinfo.h
new file mode 100644
index 000000000..bb1ba5f35
--- /dev/null
+++ b/include/arch/riscv/arch/bootinfo.h
@@ -0,0 +1,31 @@
+/*
+ * Copyright 2019, Data61
+ * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+ * ABN 41 687 119 230.
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(DATA61_GPL)
+ */
+
+#ifndef __ARCH_BOOTINFO_H
+#define __ARCH_BOOTINFO_H
+
+#define MAX_NUM_FREEMEM_REG 16
+
+/* The maximum number of reserved regions is:
+ * - 1 for each physical memory region (MAX_NUM_FREEMEM_REG)
+ * - 1 for each kernel device (ARRAY_SIZE(kernel_devices))
+ * - 1 for each mode-reserved region. (MODE_RESERVED)
+ * - 1 each for kernel, dtb, and user image. (3)
+ */
+#ifndef CONFIG_PLAT_SPIKE
+#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + ARRAY_SIZE(kernel_devices) + MODE_RESERVED + 3)
+#else
+/* spike has no devices, and ARRAY_SIZE(NULL) is invalid. */
+#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + MODE_RESERVED + 3)
+#endif
+
+#endif
diff --git a/include/arch/riscv/arch/machine/hardware.h b/include/arch/riscv/arch/machine/hardware.h
index 6a126d4cc..c5371f79e 100644
--- a/include/arch/riscv/arch/machine/hardware.h
+++ b/include/arch/riscv/arch/machine/hardware.h
@@ -54,6 +54,8 @@
 
 #define PAGE_BITS seL4_PageBits
 
+#define MODE_RESERVED 0
+
 /* MMU RISC-V related definitions. See RISC-V manual priv-1.10 */
 
 /* Extract the n-level PT index from a virtual address. This works for any
diff --git a/include/arch/riscv/arch/types.h b/include/arch/riscv/arch/types.h
index ed6d00ebe..86ea52c3d 100644
--- a/include/arch/riscv/arch/types.h
+++ b/include/arch/riscv/arch/types.h
@@ -49,6 +49,7 @@ typedef dom_t seL4_Domain;
 typedef struct kernel_frame {
     paddr_t paddr;
     pptr_t pptr;
+    int userAvailable;
 } kernel_frame_t;
 
 #endif
diff --git a/include/arch/x86/arch/bootinfo.h b/include/arch/x86/arch/bootinfo.h
new file mode 100644
index 000000000..847c6feb6
--- /dev/null
+++ b/include/arch/x86/arch/bootinfo.h
@@ -0,0 +1,29 @@
+/*
+ * Copyright 2019, Data61
+ * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+ * ABN 41 687 119 230.
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(DATA61_GPL)
+ */
+
+#ifndef __ARCH_BOOTINFO_H
+#define __ARCH_BOOTINFO_H
+
+#define MAX_NUM_FREEMEM_REG 16
+
+/*
+ * The maximum number of reserved regions we have is:
+ * - 1 for each physical memory region (MAX_NUM_FREEMEM_REG)
+ * - 1 for each kernel device:
+ *      - ioapics (CONFIG_MAX_NUM_IOAPIC)
+ *      - iommus (MAX_NUM_DRHU)
+ *      - apic (1)
+ *      - the reserved MSI region (1)
+ */
+#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + CONFIG_MAX_NUM_IOAPIC + MAX_NUM_DRHU + 2)
+
+#endif
diff --git a/include/kernel/boot.h b/include/kernel/boot.h
index f1680ced3..228f6ac3c 100644
--- a/include/kernel/boot.h
+++ b/include/kernel/boot.h
@@ -12,6 +12,7 @@
 #define __KERNEL_BOOT_H
 
 #include <bootinfo.h>
+#include <arch/bootinfo.h>
 
 #ifndef CONFIG_ARCH_ARM
 #define MAX_NUM_FREEMEM_REG 16
@@ -23,6 +24,23 @@
 #define MAX_NUM_FREEMEM_REG (ARRAY_SIZE(avail_p_regs) + MODE_RESERVED + 1 + 1)
 #endif
 
+#ifdef CONFIG_ARCH_X86
+#else
+/* The maximum number of reserved regions is:
+ * - 1 for each physical memory region (MAX_NUM_FREEMEM_REG)
+ * - 1 for each kernel device (ARRAY_SIZE(kernel_devices))
+ * - 1 for each mode-reserved region. (MODE_RESERVED)
+ * - 1 each for kernel, dtb, and user image. (3)
+ */
+#ifndef CONFIG_PLAT_SPIKE
+#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + ARRAY_SIZE(kernel_devices) + MODE_RESERVED + 3)
+#else
+/* spike has no devices */
+#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + MODE_RESERVED + 3)
+#endif
+
+#endif
+
 /*
  * Resolve naming differences between the abstract specifications
  * of the bootstrapping phase and the runtime phase of the kernel.
@@ -35,6 +53,8 @@ typedef cte_t *slot_ptr_t;
 /* (node-local) state accessed only during bootstrapping */
 
 typedef struct ndks_boot {
+    p_region_t reserved[MAX_NUM_RESV_REG];
+    word_t resv_count;
     region_t   freemem[MAX_NUM_FREEMEM_REG];
     seL4_BootInfo      *bi_frame;
     seL4_SlotPos slot_pos_cur;
@@ -53,6 +73,7 @@ static inline bool_t is_reg_empty(region_t reg)
 void init_freemem(word_t n_available, const p_region_t *available,
                   word_t n_reserved, region_t *reserved,
                   v_region_t it_v_reg, word_t extra_bi_size_bits);
+bool_t reserve_region(p_region_t reg);
 bool_t insert_region(region_t reg);
 void write_slot(slot_ptr_t slot_ptr, cap_t cap);
 cap_t create_root_cnode(void);
@@ -62,6 +83,7 @@ void write_it_pd_pts(cap_t root_cnode_cap, cap_t it_pd_cap);
 bool_t create_idle_thread(void);
 bool_t create_untypeds_for_region(cap_t root_cnode_cap, bool_t device_memory, region_t reg,
                                   seL4_SlotPos first_untyped_slot);
+bool_t create_device_untypeds(cap_t root_cnode_cap, seL4_SlotPos slot_pos_before);
 bool_t create_kernel_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg, seL4_SlotPos first_untyped_slot);
 void bi_finalise(void);
 void create_domain_cap(cap_t root_cnode_cap);
diff --git a/include/plat/pc99/plat/32/plat_mode/machine/hardware.h b/include/plat/pc99/plat/32/plat_mode/machine/hardware.h
index 05a8ab692..89a1b1c06 100644
--- a/include/plat/pc99/plat/32/plat_mode/machine/hardware.h
+++ b/include/plat/pc99/plat/32/plat_mode/machine/hardware.h
@@ -49,10 +49,6 @@
 
 #define PADDR_TOP   (PPTR_TOP - BASE_OFFSET)
 
-/* The maximum physical address for device untypeds that we export to
- * the user */
-#define PADDR_USER_DEVICE_TOP 0xffff0000
-
 /* The kernel base offset is a way to translate the kernel image segment
  * from virtual to physical. This translation must be a single offset for
  * for the entire segment (i.e. the kernel image must be contiguous both
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 0d1feb0c2..38a4ca034 100644
--- a/include/plat/pc99/plat/64/plat_mode/machine/hardware.h
+++ b/include/plat/pc99/plat/64/plat_mode/machine/hardware.h
@@ -62,10 +62,6 @@
 #define KERNEL_BASE_OFFSET (KERNEL_BASE - PADDR_BASE)
 #define kernelBase KERNEL_BASE
 
-/* The maximum physical address for device untypeds that we export to
- * the user */
-#define PADDR_USER_DEVICE_TOP BIT(47)
-
 #define BASE_OFFSET PPTR_BASE
 
 #ifndef __ASSEMBLER__
diff --git a/src/arch/arm/kernel/boot.c b/src/arch/arm/kernel/boot.c
index 5d52f86a4..972461c03 100644
--- a/src/arch/arm/kernel/boot.c
+++ b/src/arch/arm/kernel/boot.c
@@ -130,25 +130,10 @@ BOOT_CODE static bool_t create_untypeds(cap_t root_cnode_cap, region_t boot_mem_
 {
     seL4_SlotPos   slot_pos_before;
     seL4_SlotPos   slot_pos_after;
-    region_t       dev_reg;
-    word_t         i;
 
     slot_pos_before = ndks_boot.slot_pos_cur;
+    create_device_untypeds(root_cnode_cap, slot_pos_before);
     create_kernel_untypeds(root_cnode_cap, boot_mem_reuse_reg, slot_pos_before);
-    UNUSED paddr_t current_region_pos = 0;
-    for (i = 0; i < get_num_dev_p_regs(); i++) {
-        /* It is required that untyped regions are non-overlapping.
-         * We assume that hardware regions are defined in ascending order to make
-         * overlapping checks simpler
-         */
-        assert(get_dev_p_reg(i).start >= current_region_pos);
-        current_region_pos = get_dev_p_reg(i).end;
-        dev_reg = paddr_to_pptr_reg(get_dev_p_reg(i));
-        if (!create_untypeds_for_region(root_cnode_cap, true,
-                                        dev_reg, slot_pos_before)) {
-            return false;
-        }
-    }
 
     slot_pos_after = ndks_boot.slot_pos_cur;
     ndks_boot.bi_frame->untyped = (seL4_SlotRegion) {
diff --git a/src/arch/arm/machine/hardware.c b/src/arch/arm/machine/hardware.c
index 2c9e8d211..a2605f83c 100644
--- a/src/arch/arm/machine/hardware.c
+++ b/src/arch/arm/machine/hardware.c
@@ -28,16 +28,6 @@ BOOT_CODE int get_num_avail_p_regs(void)
     return sizeof(avail_p_regs) / sizeof(p_region_t);
 }
 
-BOOT_CODE int get_num_dev_p_regs(void)
-{
-    return sizeof(dev_p_regs) / sizeof(p_region_t);
-}
-
-BOOT_CODE p_region_t get_dev_p_reg(word_t i)
-{
-    return dev_p_regs[i];
-}
-
 BOOT_CODE const p_region_t *get_avail_p_regs(void)
 {
     return (const p_region_t *) avail_p_regs;
@@ -51,6 +41,13 @@ BOOT_CODE void map_kernel_devices(void)
                          VMKernelOnly,
                          vm_attributes_new(kernel_devices[i].armExecuteNever,
                                            false, false));
+        if (!kernel_devices[i].userAvailable) {
+            p_region_t reg = {
+                .start = kernel_devices[i].paddr,
+                .end = kernel_devices[i].paddr + (1 << PAGE_BITS),
+            };
+            reserve_region(reg);
+        }
     }
 }
 
diff --git a/src/arch/riscv/kernel/boot.c b/src/arch/riscv/kernel/boot.c
index 49b290333..d5eb080cc 100644
--- a/src/arch/riscv/kernel/boot.c
+++ b/src/arch/riscv/kernel/boot.c
@@ -46,22 +46,11 @@ BOOT_CODE static bool_t create_untypeds(cap_t root_cnode_cap, region_t boot_mem_
 {
     seL4_SlotPos   slot_pos_before;
     seL4_SlotPos   slot_pos_after;
-    region_t       dev_reg;
 
     slot_pos_before = ndks_boot.slot_pos_cur;
+    create_device_untypeds(root_cnode_cap, slot_pos_before);
     bool_t res = create_kernel_untypeds(root_cnode_cap, boot_mem_reuse_reg, slot_pos_before);
 
-    UNUSED paddr_t current_region_pos = 0;
-    for (int i = 0; i < get_num_dev_p_regs(); i++) {
-        assert(get_dev_p_reg(i).start >= current_region_pos);
-        current_region_pos = get_dev_p_reg(i).end;
-        dev_reg = paddr_to_pptr_reg(get_dev_p_reg(i));
-        if (!create_untypeds_for_region(root_cnode_cap, true,
-                                        dev_reg, slot_pos_before)) {
-            return false;
-        }
-    }
-
     slot_pos_after = ndks_boot.slot_pos_cur;
     ndks_boot.bi_frame->untyped = (seL4_SlotRegion) {
         slot_pos_before, slot_pos_after
diff --git a/src/arch/riscv/machine/hardware.c b/src/arch/riscv/machine/hardware.c
index 5bddc2af3..d8d0e39a4 100644
--- a/src/arch/riscv/machine/hardware.c
+++ b/src/arch/riscv/machine/hardware.c
@@ -58,29 +58,6 @@ BOOT_CODE p_region_t *get_avail_p_regs(void)
     return (p_region_t *) avail_p_regs;
 }
 
-BOOT_CODE int get_num_dev_p_regs(void)
-{
-    if (dev_p_regs != NULL) {
-        return (sizeof(dev_p_regs) / sizeof(p_region_t));
-    } else {
-        return 0;
-    }
-}
-
-BOOT_CODE p_region_t get_dev_p_reg(word_t i)
-{
-    /* We need this if guard as some RISC-V configurations don't declare any
-     * device regions and some compilers complain about indexing an empty array
-     * due to not being able to infer that get_dev_p_reg is only called if
-     * dev_p_regs contains entries.
-     */
-    if (get_num_dev_p_regs() == 0) {
-        printf("%s: No devices present.\n", __func__);
-        halt();
-    }
-    return dev_p_regs[i];
-}
-
 BOOT_CODE void map_kernel_devices(void)
 {
     if (kernel_devices == NULL) {
@@ -90,6 +67,13 @@ BOOT_CODE void map_kernel_devices(void)
     for (int i = 0; i < (sizeof(kernel_devices) / sizeof(kernel_frame_t)); i++) {
         map_kernel_frame(kernel_devices[i].paddr, KDEV_PPTR,
                          VMKernelOnly);
+        if (!kernel_devices[i].userAvailable) {
+            p_region_t reg = {
+                .start = kernel_devices[i].paddr,
+                .end = kernel_devices[i].paddr + (1 << PAGE_BITS),
+            };
+            reserve_region(reg);
+        }
     }
 }
 
diff --git a/src/arch/x86/kernel/boot.c b/src/arch/x86/kernel/boot.c
index e7001c1b0..55894725c 100644
--- a/src/arch/x86/kernel/boot.c
+++ b/src/arch/x86/kernel/boot.c
@@ -71,140 +71,17 @@ BOOT_CODE static void init_irqs(cap_t root_cnode_cap)
     write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapIRQControl), cap_irq_control_cap_new());
 }
 
-/* The maximum number of reserved regions we have is 1 for each physical memory region (+ MAX_NUM_FREEMEM_REG)
- * plus 1 for each kernel device. For kernel devices we have the ioapics (+ CONFIG_MAX_NUM_IOAPIC),
- * iommus (+ MAX_NUM_DRHU), apic (+ 1) and the reserved MSI region (+ 1) */
-#define NUM_RESERVED_REGIONS    (MAX_NUM_FREEMEM_REG + CONFIG_MAX_NUM_IOAPIC + MAX_NUM_DRHU + 2)
-typedef struct allocated_p_region {
-    p_region_t  regs[NUM_RESERVED_REGIONS];
-    word_t      cur_pos;
-} allocated_p_region_t;
-
-BOOT_BSS static allocated_p_region_t allocated_p_regions;
-
-BOOT_CODE static void merge_regions(void)
-{
-    unsigned int i, j;
-    /* Walk through all the regions and see if any can get merged */
-    for (i = 1; i < allocated_p_regions.cur_pos;) {
-        if (allocated_p_regions.regs[i - 1].end == allocated_p_regions.regs[i].start) {
-            /* move this down */
-            allocated_p_regions.regs[i - 1].end = allocated_p_regions.regs[i].end;
-            /* fill the rest down */
-            for (j = i; j < allocated_p_regions.cur_pos - 1; j++) {
-                allocated_p_regions.regs[j] = allocated_p_regions.regs[j + 1];
-            }
-            allocated_p_regions.cur_pos--;
-            /* don't increment 'i' since we want to recheck that the
-             * region we just moved to this slot doesn't also need merging */
-        } else {
-            i++;
-        }
-    }
-}
-
-static UNUSED BOOT_CODE bool_t p_region_overlaps(p_region_t reg)
-{
-    unsigned int i;
-    for (i = 0; i < allocated_p_regions.cur_pos; i++) {
-        if (allocated_p_regions.regs[i].start < reg.end &&
-            allocated_p_regions.regs[i].end > reg.start) {
-            return true;
-        }
-    }
-    return false;
-}
-
-BOOT_CODE bool_t add_allocated_p_region(p_region_t reg)
-{
-    unsigned int i, j;
-
-    assert(reg.start <= reg.end);
-    assert(!p_region_overlaps(reg));
-
-    /* Walk the existing regions and see if we can merge with an existing
-     * region, or insert in order */
-    for (i = 0; i < allocated_p_regions.cur_pos; i++) {
-        /* see if we can merge before or after this region */
-        if (allocated_p_regions.regs[i].end == reg.start) {
-            allocated_p_regions.regs[i].end = reg.end;
-            merge_regions();
-            return true;
-        }
-        if (allocated_p_regions.regs[i].start == reg.end) {
-            allocated_p_regions.regs[i].start = reg.start;
-            merge_regions();
-            return true;
-        }
-        /* see if this new one should be inserted before */
-        if (reg.end < allocated_p_regions.regs[i].start) {
-            /* ensure there's space to bump the regions up */
-            if (allocated_p_regions.cur_pos + 1 == NUM_RESERVED_REGIONS) {
-                printf("Ran out of reserved physical regions\n");
-                return false;
-            }
-            /* Copy the regions up to make a gap */
-            for (j = allocated_p_regions.cur_pos; j != i; j--) {
-                allocated_p_regions.regs[j] = allocated_p_regions.regs[j - 1];
-            }
-            /* Put this region in the gap */
-            allocated_p_regions.regs[i] = reg;
-            allocated_p_regions.cur_pos++;
-            return true;
-        }
-    }
-
-    /* nothing else matched, put this one at the end */
-    if (i + 1 == NUM_RESERVED_REGIONS) {
-        printf("Ran out of reserved physical regions\n");
-        return false;
-    }
-    allocated_p_regions.regs[i] = reg;
-    allocated_p_regions.cur_pos = i + 1;
-    return true;
-}
-
-BOOT_CODE void init_allocated_p_regions(void)
-{
-    allocated_p_regions.cur_pos = 0;
-}
-
 BOOT_CODE static bool_t create_untypeds(
     cap_t root_cnode_cap,
     region_t boot_mem_reuse_reg)
 {
     seL4_SlotPos     slot_pos_before;
     seL4_SlotPos     slot_pos_after;
-    word_t      i;
-
-    paddr_t     start = 0;
 
     slot_pos_before = ndks_boot.slot_pos_cur;
+    create_device_untypeds(root_cnode_cap, slot_pos_before);
     create_kernel_untypeds(root_cnode_cap, boot_mem_reuse_reg, slot_pos_before);
 
-    for (i = 0; i < allocated_p_regions.cur_pos; i++) {
-        if (start != allocated_p_regions.regs[i].start) {
-            if (!create_untypeds_for_region(root_cnode_cap, true,
-            paddr_to_pptr_reg((p_region_t) {
-            start, allocated_p_regions.regs[i].start
-            }),
-            slot_pos_before)) {
-                return false;
-            }
-        }
-        start = allocated_p_regions.regs[i].end;
-    }
-
-    if (start != PADDR_USER_DEVICE_TOP) {
-        if (!create_untypeds_for_region(root_cnode_cap, true,
-        paddr_to_pptr_reg((p_region_t) {
-        start, PADDR_USER_DEVICE_TOP
-    }),
-    slot_pos_before)) {
-            return false;
-        }
-    }
-
     slot_pos_after = ndks_boot.slot_pos_cur;
     ndks_boot.bi_frame->untyped = (seL4_SlotRegion) {
         slot_pos_before, slot_pos_after
diff --git a/src/arch/x86/kernel/boot_sys.c b/src/arch/x86/kernel/boot_sys.c
index bb8598d84..c01a0f446 100644
--- a/src/arch/x86/kernel/boot_sys.c
+++ b/src/arch/x86/kernel/boot_sys.c
@@ -218,7 +218,7 @@ static BOOT_CODE bool_t add_mem_p_regs(p_region_t reg)
     printf("Adding physical memory region 0x%lx-0x%lx\n", reg.start, reg.end);
     boot_state.mem_p_regs.list[boot_state.mem_p_regs.count] = reg;
     boot_state.mem_p_regs.count++;
-    return add_allocated_p_region(reg);
+    return reserve_region(reg);
 }
 
 /*
@@ -562,7 +562,6 @@ static BOOT_CODE bool_t try_boot_sys_mbi1(
      * include all the physical memory in the kernel window, but also includes any
      * important or kernel devices. */
     boot_state.mem_p_regs.count = 0;
-    init_allocated_p_regions();
     if (mbi->part1.flags & MULTIBOOT_INFO_MMAP_FLAG) {
         if (!parse_mem_map(mbi->part2.mmap_length, mbi->part2.mmap_addr)) {
             return false;
@@ -626,7 +625,6 @@ static BOOT_CODE bool_t try_boot_sys_mbi2(
      * include all the physical memory in the kernel window, but also includes any
      * important or kernel devices. */
     boot_state.mem_p_regs.count = 0;
-    init_allocated_p_regions();
     boot_state.mb_mmap_info.mmap_length = 0;
     boot_state.vbe_info.vbeMode = -1;
 
diff --git a/src/arch/x86/kernel/vspace.c b/src/arch/x86/kernel/vspace.c
index 3b5b83c78..e5376d487 100644
--- a/src/arch/x86/kernel/vspace.c
+++ b/src/arch/x86/kernel/vspace.c
@@ -140,7 +140,7 @@ BOOT_CODE bool_t map_kernel_window_devices(pte_t *pt, uint32_t num_ioapic, paddr
     if (!phys) {
         return false;
     }
-    if (!add_allocated_p_region((p_region_t) {
+    if (!reserve_region((p_region_t) {
     phys, phys + 0x1000
 })) {
         return false;
@@ -152,7 +152,7 @@ BOOT_CODE bool_t map_kernel_window_devices(pte_t *pt, uint32_t num_ioapic, paddr
     idx++;
     for (i = 0; i < num_ioapic; i++) {
         phys = ioapic_paddrs[i];
-        if (!add_allocated_p_region((p_region_t) {
+        if (!reserve_region((p_region_t) {
         phys, phys + 0x1000
     })) {
             return false;
@@ -176,7 +176,7 @@ BOOT_CODE bool_t map_kernel_window_devices(pte_t *pt, uint32_t num_ioapic, paddr
     /* map kernel devices: IOMMUs */
     for (i = 0; i < num_drhu; i++) {
         phys = (paddr_t)drhu_list[i];
-        if (!add_allocated_p_region((p_region_t) {
+        if (!reserve_region((p_region_t) {
         phys, phys + 0x1000
     })) {
             return false;
diff --git a/src/kernel/boot.c b/src/kernel/boot.c
index 6966eb555..6cbe29a45 100644
--- a/src/kernel/boot.c
+++ b/src/kernel/boot.c
@@ -27,6 +27,77 @@ ndks_boot_t ndks_boot BOOT_DATA;
 rootserver_mem_t rootserver BOOT_DATA;
 static region_t rootserver_mem BOOT_DATA;
 
+BOOT_CODE static void merge_regions(void)
+{
+    /* Walk through reserved regions and see if any can be merged */
+    for (word_t i = 1; i < ndks_boot.resv_count;) {
+        if (ndks_boot.reserved[i - 1].end == ndks_boot.reserved[i].start) {
+            /* extend earlier region */
+            ndks_boot.reserved[i - 1].end = ndks_boot.reserved[i].end;
+            /* move everything else down */
+            for (word_t j = i + 1; j < ndks_boot.resv_count; j++) {
+                ndks_boot.reserved[j - 1] = ndks_boot.reserved[j];
+            }
+
+            ndks_boot.resv_count--;
+            /* don't increment i in case there are multiple adjacent regions */
+        } else {
+            i++;
+        }
+    }
+}
+
+BOOT_CODE bool_t reserve_region(p_region_t reg)
+{
+    word_t i;
+    assert(reg.start <= reg.end);
+    if (reg.start == reg.end) {
+        return true;
+    }
+
+    /* keep the regions in order */
+    for (i = 0; i < ndks_boot.resv_count; i++) {
+        /* Try and merge the region to an existing one, if possible */
+        if (ndks_boot.reserved[i].start == reg.end) {
+            ndks_boot.reserved[i].start = reg.start;
+            merge_regions();
+            return true;
+        }
+        if (ndks_boot.reserved[i].end == reg.start) {
+            ndks_boot.reserved[i].end = reg.end;
+            merge_regions();
+            return true;
+        }
+        /* Otherwise figure out where it should go. */
+        if (ndks_boot.reserved[i].start > reg.end) {
+            /* move regions down, making sure there's enough room */
+            if (ndks_boot.resv_count + 1 >= MAX_NUM_RESV_REG) {
+                printf("Can't mark region 0x%lx-0x%lx as reserved, try increasing MAX_NUM_RESV_REG (currently %d)\n",
+                       reg.start, reg.end, (int)MAX_NUM_RESV_REG);
+                return false;
+            }
+            for (word_t j = ndks_boot.resv_count; j > i; j--) {
+                ndks_boot.reserved[j] = ndks_boot.reserved[j - 1];
+            }
+            /* insert the new region */
+            ndks_boot.reserved[i] = reg;
+            ndks_boot.resv_count++;
+            return true;
+        }
+    }
+
+    if (i + 1 == MAX_NUM_RESV_REG) {
+        printf("Can't mark region 0x%lx-0x%lx as reserved, try increasing MAX_NUM_RESV_REG (currently %d)\n",
+               reg.start, reg.end, (int)MAX_NUM_RESV_REG);
+        return false;
+    }
+
+    ndks_boot.reserved[i] = reg;
+    ndks_boot.resv_count++;
+
+    return true;
+}
+
 BOOT_CODE bool_t insert_region(region_t reg)
 {
     word_t i;
@@ -37,6 +108,7 @@ BOOT_CODE bool_t insert_region(region_t reg)
     }
     for (i = 0; i < MAX_NUM_FREEMEM_REG; i++) {
         if (is_reg_empty(ndks_boot.freemem[i])) {
+            reserve_region(pptr_to_paddr_reg(reg));
             ndks_boot.freemem[i] = reg;
             return true;
         }
@@ -550,6 +622,40 @@ BOOT_CODE bool_t create_untypeds_for_region(
     return true;
 }
 
+BOOT_CODE bool_t create_device_untypeds(cap_t root_cnode_cap, seL4_SlotPos slot_pos_before)
+{
+    paddr_t start = 0;
+    for (word_t i = 0; i < ndks_boot.resv_count; i++) {
+        if (start < ndks_boot.reserved[i].start) {
+            region_t reg = paddr_to_pptr_reg((p_region_t) {
+                start, ndks_boot.reserved[i].start
+            });
+            if (!create_untypeds_for_region(root_cnode_cap, true, reg, slot_pos_before)) {
+                return false;
+            }
+        }
+
+        start = ndks_boot.reserved[i].end;
+    }
+
+    if (start < CONFIG_PADDR_USER_DEVICE_TOP) {
+        region_t reg = paddr_to_pptr_reg((p_region_t) {
+            start, CONFIG_PADDR_USER_DEVICE_TOP
+        });
+        /*
+         * The auto-generated bitfield code will get upset if the
+         * end pptr is larger than the maximum pointer size for this architecture.
+         */
+        if (reg.end > PPTR_TOP) {
+            reg.end = PPTR_TOP;
+        }
+        if (!create_untypeds_for_region(root_cnode_cap, true, reg, slot_pos_before)) {
+            return false;
+        }
+    }
+    return true;
+}
+
 BOOT_CODE bool_t create_kernel_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg,
                                         seL4_SlotPos first_untyped_slot)
 {
@@ -640,6 +746,7 @@ BOOT_CODE void init_freemem(word_t n_available, const p_region_t *available,
             a++;
         } else if (reserved[r].end <= avail_reg[a].start) {
             /* the reserved region is below the available region - skip it*/
+            reserve_region(pptr_to_paddr_reg(reserved[r]));
             r++;
         } else if (reserved[r].start >= avail_reg[a].end) {
             /* the reserved region is above the available region - take the whole thing */
@@ -651,6 +758,7 @@ BOOT_CODE void init_freemem(word_t n_available, const p_region_t *available,
                 /* the region overlaps with the start of the available region.
                  * trim start of the available region */
                 avail_reg[a].start = MIN(avail_reg[a].end, reserved[r].end);
+                reserve_region(pptr_to_paddr_reg(reserved[r]));
                 r++;
             } else {
                 assert(reserved[r].start < avail_reg[a].end);
@@ -661,6 +769,7 @@ BOOT_CODE void init_freemem(word_t n_available, const p_region_t *available,
                 insert_region(m);
                 if (avail_reg[a].end > reserved[r].end) {
                     avail_reg[a].start = reserved[r].end;
+                    reserve_region(pptr_to_paddr_reg(reserved[r]));
                     r++;
                 } else {
                     a++;
@@ -669,6 +778,12 @@ BOOT_CODE void init_freemem(word_t n_available, const p_region_t *available,
         }
     }
 
+    for (; r < n_reserved; r++) {
+        if (reserved[r].start < reserved[r].end) {
+            reserve_region(pptr_to_paddr_reg(reserved[r]));
+        }
+    }
+
     /* no more reserved regions - add the rest */
     for (; a < n_available; a++) {
         if (avail_reg[a].start < avail_reg[a].end) {
diff --git a/src/plat/pc99/machine/hardware.c b/src/plat/pc99/machine/hardware.c
index aca16050e..10528c9cd 100644
--- a/src/plat/pc99/machine/hardware.c
+++ b/src/plat/pc99/machine/hardware.c
@@ -24,8 +24,8 @@ BOOT_CODE bool_t platAddDevices(void)
     /* remove the MSI region as poking at this is undefined and may allow for
      * the user to generate arbitrary MSI interrupts. Only need to consider
      * this if it would actually be in the user device region */
-    if (PADDR_USER_DEVICE_TOP > 0xFFFFFFF8) {
-        if (!add_allocated_p_region((p_region_t) {
+    if (CONFIG_PADDR_USER_DEVICE_TOP > 0xFFFFFFF8) {
+        if (!reserve_region((p_region_t) {
         (word_t)0xFFFFFFF8, (word_t)0xFFFFFFF8 + 8
         })) {
             return false;
diff --git a/tools/hardware/outputs/c_header.py b/tools/hardware/outputs/c_header.py
index 7478679ea..5d72eaf4a 100644
--- a/tools/hardware/outputs/c_header.py
+++ b/tools/hardware/outputs/c_header.py
@@ -91,6 +91,11 @@ static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
         {% if args.arch == 'arm' %}
         true, /* armExecuteNever */
         {% endif %}
+        {% if group.user_ok %}
+        true, /* userAvailable */
+        {% else %}
+        false, /* userAvailable */
+        {% endif %}
     },
     {% endfor %}
     {% if group.has_macro() %}
@@ -109,18 +114,6 @@ static const p_region_t BOOT_RODATA avail_p_regs[] = {
     {% endfor %}
 };
 
-/* DEVICE MEMORY */
-/* using {{ physBits }} bits of address space */
-/* excluded regions:
-{% for reg in excluded_regions %}
- * {{ "0x{:x}".format(reg.base) }} - {{ "0x{:x}".format(reg.base + reg.size) }} {{ reg.desc }} {{ reg.user_ok }}
-{% endfor %}
- */
-static const p_region_t BOOT_RODATA dev_p_regs[] = {
-    {% for reg in device_regions %}
-    { {{ "0x{:x}".format(reg.base) }}, {{ "0x{:x}".format(reg.base + reg.size) }} },
-    {% endfor %}
-};
 #endif /* !__ASSEMBLER__ */
 
 #endif /* __PLAT_DEVICES_GEN_H */
@@ -183,15 +176,11 @@ def run(tree: fdt.FdtParser, hardware: rule.HardwareYaml, config: config.Config,
     physical_memory, reserved, physBase = memory.get_physical_memory(tree, config)
     kernel_regions, kernel_macros = get_kernel_devices(tree, hardware)
     kernel_irqs = get_interrupts(tree, hardware)
-    device_regions = memory.get_addrspace_exclude(
-        list(reserved) + kernel_regions + physical_memory, config)
     template = Environment(loader=BaseLoader, trim_blocks=True,
                            lstrip_blocks=True).from_string(HEADER_TEMPLATE)
 
     template_args = dict(builtins.__dict__, **{
         'args': args,
-        'device_regions': device_regions,
-        'excluded_regions': list(reserved) + kernel_regions + physical_memory,
         'kernel_irqs': kernel_irqs,
         'kernel_macros': kernel_macros,
         'kernel_regions': kernel_regions,