From 381baed8da4c261131358b3bd985bfbea53e8e98 Mon Sep 17 00:00:00 2001
From: Lourens Willekes <lourens.willekes@dornerworks.com>
Date: Wed, 22 Mar 2023 10:09:13 -0700
Subject: [PATCH] init: dynamically set ALLOCMAN_VIRTUAL_SIZE

The value of 72000 (used to scale guest_ram_mb to ALLOCMAN_VIRTUAL_SIZE
bytes) was found by increasing ALLOCMAN_VIRTUAL_SIZE by 500000000 bytes
and finding the difference in allocated RAM. Each 50000000 increased,
the guest was able to allocate an additional 6960 MiBs. This allows
64-bit x86 VMs to allocate large amounts of memory.

Signed-off-by: Chris Guikema <chris.guikema@dornerworks.com>
---
 camkes_vm_helpers.cmake                      |  3 +++
 components/Init/src/main.c                   |  7 +++----
 templates/seL4AllocmanVirtualSize.template.c | 20 ++++++++++++++++++++
 templates/seL4AllocmanVirtualSize.template.h |  7 +++++++
 4 files changed, 33 insertions(+), 4 deletions(-)
 create mode 100644 templates/seL4AllocmanVirtualSize.template.c
 create mode 100644 templates/seL4AllocmanVirtualSize.template.h

diff --git a/camkes_vm_helpers.cmake b/camkes_vm_helpers.cmake
index 5aac4647..e79e876d 100644
--- a/camkes_vm_helpers.cmake
+++ b/camkes_vm_helpers.cmake
@@ -57,6 +57,9 @@ function(DeclareCAmkESVM init_component)
         seL4GuestMaps.template.c
         seL4VMIRQs.template.c
         seL4VMPCIDevices.template.c
+        seL4AllocmanVirtualSize.template.c
+        TEMPLATE_HEADERS
+        seL4AllocmanVirtualSize.template.h
     )
 endfunction(DeclareCAmkESVM)
 
diff --git a/components/Init/src/main.c b/components/Init/src/main.c
index 1e726e26..638c384b 100644
--- a/components/Init/src/main.c
+++ b/components/Init/src/main.c
@@ -57,7 +57,6 @@
 #include "virtio_vsock.h"
 
 #define BRK_VIRTUAL_SIZE 400000000
-#define ALLOCMAN_VIRTUAL_SIZE 400000000
 #define CROSS_VM_EVENT_IRQ_NUM 12
 #define CROSS_VM_BASE_ADDRESS 0xa0000000
 
@@ -174,12 +173,12 @@ void pre_init(void)
         ZF_LOGF("Failed to allocate reservation");
     }
     error = sel4utils_reserve_range_no_alloc(&vspace, pool_reservation.res,
-                                             ALLOCMAN_VIRTUAL_SIZE, seL4_AllRights, 1, &vaddr);
+                                             allocman_virtual_size(), seL4_AllRights, 1, &vaddr);
     if (error) {
         ZF_LOGF("Failed to provide virtual memory allocator");
     }
-    bootstrap_configure_virtual_pool(allocman, vaddr, ALLOCMAN_VIRTUAL_SIZE, simple_get_init_cap(&camkes_simple,
-                                                                                                 seL4_CapInitThreadPD));
+    bootstrap_configure_virtual_pool(allocman, vaddr, allocman_virtual_size(), simple_get_init_cap(&camkes_simple,
+                                                                                                   seL4_CapInitThreadPD));
 
     /* Add additional untypeds that make up extra RAM */
     int num = ram_num_untypeds();
diff --git a/templates/seL4AllocmanVirtualSize.template.c b/templates/seL4AllocmanVirtualSize.template.c
new file mode 100644
index 00000000..7cd3c882
--- /dev/null
+++ b/templates/seL4AllocmanVirtualSize.template.c
@@ -0,0 +1,20 @@
+/*
+ * Copyright 2023, DornerWorks
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#include <camkes.h>
+
+/* For every 500000000 bytes added to ALLOCMAN_VIRTUAL_SIZE,
+ * the guest can map an additional 6960 MiBs. Dividing the two
+ * values gives a scale of 71839, which we round up to 72000
+ */
+
+/*- set guest_ram_mb = configuration[me.name].get('guest_ram_mb', 4096) -*/
+/*- set allocman_virtual_size = guest_ram_mb * 72000 -*/
+
+size_t allocman_virtual_size(void)
+{
+    return /*? allocman_virtual_size ?*/;
+}
diff --git a/templates/seL4AllocmanVirtualSize.template.h b/templates/seL4AllocmanVirtualSize.template.h
new file mode 100644
index 00000000..f3ffb59d
--- /dev/null
+++ b/templates/seL4AllocmanVirtualSize.template.h
@@ -0,0 +1,7 @@
+/*
+ * Copyright 2023, DornerWorks
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+size_t allocman_virtual_size(void);