diff --git a/include/kernel/boot.h b/include/kernel/boot.h index 8ed8d07f0..cbaaf7012 100644 --- a/include/kernel/boot.h +++ b/include/kernel/boot.h @@ -51,7 +51,8 @@ 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); + word_t n_reserved, region_t *reserved, + v_region_t it_v_reg, word_t extra_bi_size_bits); bool_t insert_region(region_t reg); void write_slot(slot_ptr_t slot_ptr, cap_t cap); cap_t create_root_cnode(void); @@ -142,7 +143,6 @@ static inline BOOT_CODE pptr_t it_alloc_paging(void) word_t arch_get_n_paging(v_region_t it_veg); /* Create pptrs for all root server objects, starting at pptr, to cover the - * virtual memory region v_reg, and any extra boot info. - * Return the region occupied by those objects.*/ -region_t create_rootserver_objects(pptr_t start, v_region_t v_reg, word_t extra_bi_size_bits); + * virtual memory region v_reg, and any extra boot info. */ +void create_rootserver_objects(pptr_t start, v_region_t v_reg, word_t extra_bi_size_bits); #endif diff --git a/src/arch/arm/kernel/boot.c b/src/arch/arm/kernel/boot.c index 73c61cdaa..9426b8885 100644 --- a/src/arch/arm/kernel/boot.c +++ b/src/arch/arm/kernel/boot.c @@ -39,7 +39,7 @@ extern char ki_end[1]; BOOT_DATA static volatile int node_boot_lock = 0; #endif /* ENABLE_SMP_SUPPORT */ -#define ARCH_RESERVED 4 // kernel + user image + dtb + rootserver objects +#define ARCH_RESERVED 3 // kernel + user image + dtb #define MAX_RESERVED (ARCH_RESERVED + MODE_RESERVED) BOOT_DATA static region_t reserved[MAX_RESERVED]; @@ -56,11 +56,6 @@ BOOT_CODE static void arch_init_freemem(region_t ui_reg, region_t dtb_reg, v_reg reserved[index].end = dtb_reg.end; index++; } - reserved[index].start = ui_reg.start; - reserved[index].end = ui_reg.end; - index++; - reserved[index] = create_rootserver_objects(ui_reg.end, it_v_reg, extra_bi_size_bits); - index++; if (MODE_RESERVED == 1) { @@ -83,9 +78,7 @@ BOOT_CODE static void arch_init_freemem(region_t ui_reg, region_t dtb_reg, v_reg index++; } - reserved[index] = create_rootserver_objects(ui_reg.start, it_v_reg, extra_bi_size_bits); - index++; - init_freemem(get_num_avail_p_regs(), get_avail_p_regs(), index, reserved); + init_freemem(get_num_avail_p_regs(), get_avail_p_regs(), index, reserved, it_v_reg, extra_bi_size_bits); } BOOT_CODE static void init_irqs(cap_t root_cnode_cap) diff --git a/src/arch/riscv/kernel/boot.c b/src/arch/riscv/kernel/boot.c index ecf3c29ff..723883d65 100644 --- a/src/arch/riscv/kernel/boot.c +++ b/src/arch/riscv/kernel/boot.c @@ -35,7 +35,7 @@ extern char ki_boot_end[1]; /* pointer to end of kernel image */ extern char ki_end[1]; -#define MAX_RESERVED 3 +#define MAX_RESERVED 2 BOOT_DATA static region_t res_reg[MAX_RESERVED]; BOOT_CODE static bool_t create_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg) @@ -99,9 +99,8 @@ BOOT_CODE static void arch_init_freemem(region_t ui_reg, v_region_t ui_v_reg) res_reg[0].end = (pptr_t)paddr_to_pptr(kpptr_to_paddr((void *)ki_end)); res_reg[1].start = ui_reg.start; res_reg[1].end = ui_reg.end; - res_reg[2] = create_rootserver_objects(ui_reg.end, ui_v_reg, 0); - init_freemem(get_num_avail_p_regs(), get_avail_p_regs(), MAX_RESERVED, res_reg); + init_freemem(get_num_avail_p_regs(), get_avail_p_regs(), MAX_RESERVED, res_reg, ui_v_reg, 0); } BOOT_CODE static void init_irqs(cap_t root_cnode_cap) diff --git a/src/arch/x86/kernel/boot.c b/src/arch/x86/kernel/boot.c index 912183405..a355ad877 100644 --- a/src/arch/x86/kernel/boot.c +++ b/src/arch/x86/kernel/boot.c @@ -27,7 +27,7 @@ #include -#define MAX_RESERVED 2 +#define MAX_RESERVED 1 BOOT_DATA static region_t reserved[MAX_RESERVED]; /* functions exactly corresponding to abstract specification */ @@ -217,8 +217,7 @@ BOOT_CODE static void arch_init_freemem(p_region_t ui_p_reg, v_region_t v_reg, { ui_p_reg.start = 0; reserved[0] = paddr_to_pptr_reg(ui_p_reg); - reserved[1] = create_rootserver_objects(reserved[0].end, v_reg, extra_bi_size_bits); - init_freemem(mem_p_regs->count, mem_p_regs->list, MAX_RESERVED, reserved); + init_freemem(mem_p_regs->count, mem_p_regs->list, MAX_RESERVED, reserved, v_reg, extra_bi_size_bits); } /* This function initialises a node's kernel state. It does NOT initialise the CPU. */ diff --git a/src/kernel/boot.c b/src/kernel/boot.c index eb254abf5..7d6be53db 100644 --- a/src/kernel/boot.c +++ b/src/kernel/boot.c @@ -69,6 +69,13 @@ BOOT_CODE static pptr_t alloc_rootserver_obj(word_t size_bits, word_t n) return allocated; } +BOOT_CODE static word_t rootserver_max_size_bits(word_t extra_bi_size_bits) +{ + word_t cnode_size_bits = CONFIG_ROOT_CNODE_SIZE_BITS + seL4_SlotBits; + word_t max = MAX(cnode_size_bits, seL4_VSpaceBits); + return MAX(max, extra_bi_size_bits); +} + BOOT_CODE static word_t calculate_rootserver_size(v_region_t v_reg, word_t extra_bi_size_bits) { /* work out how much memory we need for root server objects */ @@ -89,16 +96,15 @@ BOOT_CODE static void maybe_alloc_extra_bi(word_t cmp_size_bits, word_t extra_bi } } -BOOT_CODE region_t create_rootserver_objects(pptr_t start, v_region_t v_reg, word_t extra_bi_size_bits) +BOOT_CODE void create_rootserver_objects(pptr_t start, v_region_t v_reg, word_t extra_bi_size_bits) { /* the largest object the PD, the root cnode, or the extra boot info */ word_t cnode_size_bits = CONFIG_ROOT_CNODE_SIZE_BITS + seL4_SlotBits; - word_t max = MAX(cnode_size_bits, seL4_VSpaceBits); - max = MAX(max, extra_bi_size_bits); + word_t max = rootserver_max_size_bits(extra_bi_size_bits); - start = ROUND_UP(start, max); + word_t size = calculate_rootserver_size(v_reg, extra_bi_size_bits); rootserver_mem.start = start; - rootserver_mem.end = start + calculate_rootserver_size(v_reg, extra_bi_size_bits); + rootserver_mem.end = start + size; maybe_alloc_extra_bi(max, extra_bi_size_bits); @@ -136,10 +142,6 @@ BOOT_CODE region_t create_rootserver_objects(pptr_t start, v_region_t v_reg, wor #endif /* we should have allocated all our memory */ assert(rootserver_mem.start == rootserver_mem.end); - return (region_t) { - .start = start, - .end = rootserver_mem.end - }; } BOOT_CODE void write_slot(slot_ptr_t slot_ptr, cap_t cap) @@ -524,7 +526,8 @@ static BOOT_DATA region_t avail_reg[MAX_NUM_FREEMEM_REG]; * A region represents an area of memory. */ BOOT_CODE void init_freemem(word_t n_available, const p_region_t *available, - word_t n_reserved, region_t *reserved) + word_t n_reserved, region_t *reserved, + v_region_t it_v_reg, word_t extra_bi_size_bits) { /* Force ordering and exclusivity of reserved regions */ for (word_t i = 0; n_reserved > 0 && i < n_reserved - 1; i++) { @@ -597,4 +600,33 @@ BOOT_CODE void init_freemem(word_t n_available, const p_region_t *available, insert_region(avail_reg[a]); } } + + /* now try to fit the root server objects into a region */ + word_t i = MAX_NUM_FREEMEM_REG - 1; + if (!is_reg_empty(ndks_boot.freemem[i])) { + printf("Insufficient MAX_NUM_FREEMEM_REG"); + halt(); + } + /* skip any empty regions */ + for (; is_reg_empty(ndks_boot.freemem[i]) && i >= 0; i--); + + /* try to grab the last available p region to create the root server objects + * from. If possible, retain any left over memory as an extra p region */ + word_t size = calculate_rootserver_size(it_v_reg, extra_bi_size_bits); + word_t max = rootserver_max_size_bits(extra_bi_size_bits); + for (; i >= 0; i--) { + word_t next = i + 1; + pptr_t start = ROUND_DOWN(ndks_boot.freemem[i].end - size, max); + if (start >= ndks_boot.freemem[i].start) { + create_rootserver_objects(start, it_v_reg, extra_bi_size_bits); + if (i < MAX_NUM_FREEMEM_REG) { + ndks_boot.freemem[next].end = ndks_boot.freemem[i].end; + ndks_boot.freemem[next].start = start + size; + } + ndks_boot.freemem[i].end = start; + break; + } else if (i < MAX_NUM_FREEMEM_REG) { + ndks_boot.freemem[next] = ndks_boot.freemem[i]; + } + } }