diff --git a/tools/libxc/xc_dom_arm.c b/tools/libxc/xc_dom_arm.c
index 61f9ba6..7216d2a 100644
--- a/tools/libxc/xc_dom_arm.c
+++ b/tools/libxc/xc_dom_arm.c
@@ -286,12 +286,18 @@ int arch_setup_meminit(struct xc_dom_image *dom)
     uint64_t modbase;
 
     /* Convenient */
-    const uint64_t ramsize = dom->total_pages << XC_PAGE_SHIFT;
+    const uint64_t ramsize = (uint64_t)dom->total_pages << XC_PAGE_SHIFT;
 
-    const uint64_t ram0size = ramsize;
+    const uint64_t ram0size =
+        ramsize > GUEST_RAM0_SIZE ? GUEST_RAM0_SIZE : ramsize;
     const uint64_t ram0end = GUEST_RAM0_BASE + ram0size;
+    const uint64_t ram1size =
+        ramsize > ram0size ? ramsize - ram0size : 0;
+    const uint64_t ram1end = GUEST_RAM1_BASE + ram1size;
 
-    const xen_pfn_t p2m_size = (ram0end - GUEST_RAM0_BASE) >> XC_PAGE_SHIFT;
+    const xen_pfn_t p2m_size = ram1size ?
+        (ram1end - GUEST_RAM0_BASE) >> XC_PAGE_SHIFT :
+        (ram0end - GUEST_RAM0_BASE) >> XC_PAGE_SHIFT;
 
     const uint64_t kernbase = dom->kernel_seg.vstart;
     const uint64_t kernend = ROUNDUP(dom->kernel_seg.vend, 21/*2MB*/);
@@ -337,6 +343,10 @@ int arch_setup_meminit(struct xc_dom_image *dom)
                                     GUEST_RAM0_BASE >> XC_PAGE_SHIFT,
                                     ram0size >> XC_PAGE_SHIFT)))
         return rc;
+    if ((rc = populate_guest_memory(dom,
+                                    GUEST_RAM1_BASE >> XC_PAGE_SHIFT,
+                                    ram1size >> XC_PAGE_SHIFT)))
+        return rc;
 
     /*
      * We try to place dtb+initrd at 128MB or if we have less RAM
diff --git a/tools/libxl/libxl_arm.c b/tools/libxl/libxl_arm.c
index 215ef9e..1af6b4a 100644
--- a/tools/libxl/libxl_arm.c
+++ b/tools/libxl/libxl_arm.c
@@ -255,8 +255,8 @@ static int make_psci_node(libxl__gc *gc, void *fdt)
     return 0;
 }
 
-static int make_memory_node(libxl__gc *gc, void *fdt,
-                            uint64_t base, uint64_t size)
+static int make_one_memory_node(libxl__gc *gc, void *fdt,
+                                uint64_t base, uint64_t size)
 {
     int res;
     const char *name = GCSPRINTF("memory@%"PRIx64, base);
@@ -277,6 +277,23 @@ static int make_memory_node(libxl__gc *gc, void *fdt,
     return 0;
 }
 
+static int make_memory_node(libxl__gc *gc, void *fdt, uint64_t size)
+{
+    int res;
+    /* This had better match libxc's arch_setup_meminit... */
+    const uint64_t size0 = size > GUEST_RAM0_SIZE ? GUEST_RAM0_SIZE : size;
+    const uint64_t size1 = size > GUEST_RAM0_SIZE ? size - size0 : 0;
+
+    res = make_one_memory_node(gc, fdt, GUEST_RAM0_BASE, size0);
+    if (res) return res;
+    if (size1) {
+        res = make_one_memory_node(gc, fdt, GUEST_RAM1_BASE, size1);
+        if (res) return res;
+    }
+
+    return 0;
+}
+
 static int make_intc_node(libxl__gc *gc, void *fdt,
                           uint64_t gicd_base, uint64_t gicd_size,
                           uint64_t gicc_base, uint64_t gicc_size)
@@ -490,7 +507,6 @@ next_resize:
         FDT( make_psci_node(gc, fdt) );
 
         FDT( make_memory_node(gc, fdt,
-                              dom->rambase_pfn << XC_PAGE_SHIFT,
                               info->target_memkb * 1024) );
         FDT( make_intc_node(gc, fdt,
                             GUEST_GICD_BASE, GUEST_GICD_SIZE,
diff --git a/xen/include/public/arch-arm.h b/xen/include/public/arch-arm.h
index c4f4990..3f457f1 100644
--- a/xen/include/public/arch-arm.h
+++ b/xen/include/public/arch-arm.h
@@ -374,12 +374,15 @@ typedef uint64_t xen_callback_t;
 
 #define GUEST_MAGIC_BASE  0x39000000ULL
 
-#define GUEST_RAM0_BASE   0x40000000ULL /* 3GB of RAM @ 1GB */
+#define GUEST_RAM0_BASE   0x40000000ULL /* 3GB of low RAM @ 1GB */
 #define GUEST_RAM0_SIZE   0xc0000000ULL
 
+#define GUEST_RAM1_BASE   0x0200000000ULL /* 1016GB of RAM @ 8GB */
+#define GUEST_RAM1_SIZE   0xfe00000000ULL
+
 #define GUEST_RAM_BASE    GUEST_RAM0_BASE /* Lowest RAM address */
-/* Largest amount of actual RAM, not including holes */
-#define GUEST_RAM_MAX     (GUEST_RAM0_SIZE)
+ /* Largest amount of actual RAM, not including holes */
+#define GUEST_RAM_MAX     (GUEST_RAM0_SIZE + GUEST_RAM1_SIZE)
 
 /* Interrupts */
 #define GUEST_TIMER_VIRT_PPI    27
