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 + +/* 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);