/* * Copyright 2014, General Dynamics C4 Systems * * SPDX-License-Identifier: GPL-2.0-only */ #include #include #include #include #include #include #include #include #include #include #include #include /* (node-local) state accessed only during bootstrapping */ BOOT_BSS ndks_boot_t ndks_boot; BOOT_BSS rootserver_mem_t rootserver; BOOT_BSS static region_t rootserver_mem; 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%"SEL4_PRIx_word"-0x%"SEL4_PRIx_word " 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%"SEL4_PRIx_word"-0x%"SEL4_PRIx_word " 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 static bool_t insert_region(region_t reg) { assert(reg.start <= reg.end); if (is_reg_empty(reg)) { return true; } for (word_t i = 0; i < ARRAY_SIZE(ndks_boot.freemem); i++) { if (is_reg_empty(ndks_boot.freemem[i])) { reserve_region(pptr_to_paddr_reg(reg)); ndks_boot.freemem[i] = reg; return true; } } /* We don't know if a platform or architecture picked MAX_NUM_FREEMEM_REG * arbitrarily or carefully calculated it to be big enough. Running out of * slots here is not really fatal, eventually memory allocation may fail * if there is not enough free memory. However, allocations should never * blindly assume to work, some error handling must always be in place even * if the environment has been crafted carefully to support them. Thus, we * don't stop the boot process here, but return an error. The caller should * decide how bad this is. */ printf("no free memory slot left for [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"]," " consider increasing MAX_NUM_FREEMEM_REG (%u)\n", reg.start, reg.end, (unsigned int)MAX_NUM_FREEMEM_REG); /* For debug builds we consider this a fatal error. Rationale is, that the * caller does not check the error code at the moment, but just ignores any * failures silently. */ assert(0); return false; } BOOT_CODE static pptr_t alloc_rootserver_obj(word_t size_bits, word_t n) { pptr_t allocated = rootserver_mem.start; /* allocated memory must be aligned */ assert(allocated % BIT(size_bits) == 0); rootserver_mem.start += (n * BIT(size_bits)); /* we must not have run out of memory */ assert(rootserver_mem.start <= rootserver_mem.end); memzero((void *) allocated, n * BIT(size_bits)); 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 it_v_reg, word_t extra_bi_size_bits) { /* work out how much memory we need for root server objects */ word_t size = BIT(CONFIG_ROOT_CNODE_SIZE_BITS + seL4_SlotBits); size += BIT(seL4_TCBBits); // root thread tcb size += BIT(seL4_PageBits); // ipc buf size += BIT(BI_FRAME_SIZE_BITS); // boot info size += BIT(seL4_ASIDPoolBits); size += extra_bi_size_bits > 0 ? BIT(extra_bi_size_bits) : 0; size += BIT(seL4_VSpaceBits); // root vspace #ifdef CONFIG_KERNEL_MCS size += BIT(seL4_MinSchedContextBits); // root sched context #endif /* for all archs, seL4_PageTable Bits is the size of all non top-level paging structures */ return size + arch_get_n_paging(it_v_reg) * BIT(seL4_PageTableBits); } BOOT_CODE static void maybe_alloc_extra_bi(word_t cmp_size_bits, word_t extra_bi_size_bits) { if (extra_bi_size_bits >= cmp_size_bits && rootserver.extra_bi == 0) { rootserver.extra_bi = alloc_rootserver_obj(extra_bi_size_bits, 1); } } /* Create pptrs for all root server objects, starting at a give start address, * to cover the virtual memory region v_reg, and any extra boot info. */ BOOT_CODE static void create_rootserver_objects(pptr_t start, v_region_t it_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 = rootserver_max_size_bits(extra_bi_size_bits); word_t size = calculate_rootserver_size(it_v_reg, extra_bi_size_bits); rootserver_mem.start = start; rootserver_mem.end = start + size; maybe_alloc_extra_bi(max, extra_bi_size_bits); /* the root cnode is at least 4k, so it could be larger or smaller than a pd. */ #if (CONFIG_ROOT_CNODE_SIZE_BITS + seL4_SlotBits) > seL4_VSpaceBits rootserver.cnode = alloc_rootserver_obj(cnode_size_bits, 1); maybe_alloc_extra_bi(seL4_VSpaceBits, extra_bi_size_bits); rootserver.vspace = alloc_rootserver_obj(seL4_VSpaceBits, 1); #else rootserver.vspace = alloc_rootserver_obj(seL4_VSpaceBits, 1); maybe_alloc_extra_bi(cnode_size_bits, extra_bi_size_bits); rootserver.cnode = alloc_rootserver_obj(cnode_size_bits, 1); #endif /* at this point we are up to creating 4k objects - which is the min size of * extra_bi so this is the last chance to allocate it */ maybe_alloc_extra_bi(seL4_PageBits, extra_bi_size_bits); rootserver.asid_pool = alloc_rootserver_obj(seL4_ASIDPoolBits, 1); rootserver.ipc_buf = alloc_rootserver_obj(seL4_PageBits, 1); rootserver.boot_info = alloc_rootserver_obj(BI_FRAME_SIZE_BITS, 1); /* TCBs on aarch32 can be larger than page tables in certain configs */ #if seL4_TCBBits >= seL4_PageTableBits rootserver.tcb = alloc_rootserver_obj(seL4_TCBBits, 1); #endif /* paging structures are 4k on every arch except aarch32 (1k) */ word_t n = arch_get_n_paging(it_v_reg); rootserver.paging.start = alloc_rootserver_obj(seL4_PageTableBits, n); rootserver.paging.end = rootserver.paging.start + n * BIT(seL4_PageTableBits); /* for most archs, TCBs are smaller than page tables */ #if seL4_TCBBits < seL4_PageTableBits rootserver.tcb = alloc_rootserver_obj(seL4_TCBBits, 1); #endif #ifdef CONFIG_KERNEL_MCS rootserver.sc = alloc_rootserver_obj(seL4_MinSchedContextBits, 1); #endif /* we should have allocated all our memory */ assert(rootserver_mem.start == rootserver_mem.end); } BOOT_CODE void write_slot(slot_ptr_t slot_ptr, cap_t cap) { slot_ptr->cap = cap; slot_ptr->cteMDBNode = nullMDBNode; mdb_node_ptr_set_mdbRevocable(&slot_ptr->cteMDBNode, true); mdb_node_ptr_set_mdbFirstBadged(&slot_ptr->cteMDBNode, true); } /* Our root CNode needs to be able to fit all the initial caps and not * cover all of memory. */ compile_assert(root_cnode_size_valid, CONFIG_ROOT_CNODE_SIZE_BITS < 32 - seL4_SlotBits && BIT(CONFIG_ROOT_CNODE_SIZE_BITS) >= seL4_NumInitialCaps && BIT(CONFIG_ROOT_CNODE_SIZE_BITS) >= (seL4_PageBits - seL4_SlotBits)) BOOT_CODE cap_t create_root_cnode(void) { cap_t cap = cap_cnode_cap_new( CONFIG_ROOT_CNODE_SIZE_BITS, /* radix */ wordBits - CONFIG_ROOT_CNODE_SIZE_BITS, /* guard size */ 0, /* guard */ rootserver.cnode); /* pptr */ /* write the root CNode cap into the root CNode */ write_slot(SLOT_PTR(rootserver.cnode, seL4_CapInitThreadCNode), cap); return cap; } /* Check domain scheduler assumptions. */ compile_assert(num_domains_valid, CONFIG_NUM_DOMAINS >= 1 && CONFIG_NUM_DOMAINS <= 256) compile_assert(num_priorities_valid, CONFIG_NUM_PRIORITIES >= 1 && CONFIG_NUM_PRIORITIES <= 256) BOOT_CODE void create_domain_cap(cap_t root_cnode_cap) { /* Check domain scheduler assumptions. */ assert(ksDomScheduleLength > 0); for (word_t i = 0; i < ksDomScheduleLength; i++) { assert(ksDomSchedule[i].domain < CONFIG_NUM_DOMAINS); assert(ksDomSchedule[i].length > 0); } cap_t cap = cap_domain_cap_new(); write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapDomain), cap); } BOOT_CODE cap_t create_ipcbuf_frame_cap(cap_t root_cnode_cap, cap_t pd_cap, vptr_t vptr) { clearMemory((void *)rootserver.ipc_buf, PAGE_BITS); /* create a cap of it and write it into the root CNode */ cap_t cap = create_mapped_it_frame_cap(pd_cap, rootserver.ipc_buf, vptr, IT_ASID, false, false); write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadIPCBuffer), cap); return cap; } BOOT_CODE void create_bi_frame_cap(cap_t root_cnode_cap, cap_t pd_cap, vptr_t vptr) { /* create a cap of it and write it into the root CNode */ cap_t cap = create_mapped_it_frame_cap(pd_cap, rootserver.boot_info, vptr, IT_ASID, false, false); write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapBootInfoFrame), cap); } BOOT_CODE word_t calculate_extra_bi_size_bits(word_t extra_size) { if (extra_size == 0) { return 0; } word_t clzl_ret = clzl(ROUND_UP(extra_size, seL4_PageBits)); word_t msb = seL4_WordBits - 1 - clzl_ret; /* If region is bigger than a page, make sure we overallocate rather than * underallocate */ if (extra_size > BIT(msb)) { msb++; } return msb; } BOOT_CODE void populate_bi_frame(node_id_t node_id, word_t num_nodes, vptr_t ipcbuf_vptr, word_t extra_bi_size) { /* clear boot info memory */ clearMemory((void *)rootserver.boot_info, BI_FRAME_SIZE_BITS); if (extra_bi_size) { clearMemory((void *)rootserver.extra_bi, calculate_extra_bi_size_bits(extra_bi_size)); } /* initialise bootinfo-related global state */ seL4_BootInfo *bi = BI_PTR(rootserver.boot_info); bi->nodeID = node_id; bi->numNodes = num_nodes; bi->numIOPTLevels = 0; bi->ipcBuffer = (seL4_IPCBuffer *)ipcbuf_vptr; bi->initThreadCNodeSizeBits = CONFIG_ROOT_CNODE_SIZE_BITS; bi->initThreadDomain = ksDomSchedule[ksDomScheduleIdx].domain; bi->extraLen = extra_bi_size; ndks_boot.bi_frame = bi; ndks_boot.slot_pos_cur = seL4_NumInitialCaps; } BOOT_CODE bool_t provide_cap(cap_t root_cnode_cap, cap_t cap) { if (ndks_boot.slot_pos_cur >= BIT(CONFIG_ROOT_CNODE_SIZE_BITS)) { printf("ERROR: can't add another cap, all %"SEL4_PRIu_word " (=2^CONFIG_ROOT_CNODE_SIZE_BITS) slots used\n", BIT(CONFIG_ROOT_CNODE_SIZE_BITS)); return false; } write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), ndks_boot.slot_pos_cur), cap); ndks_boot.slot_pos_cur++; return true; } BOOT_CODE create_frames_of_region_ret_t create_frames_of_region( cap_t root_cnode_cap, cap_t pd_cap, region_t reg, bool_t do_map, sword_t pv_offset ) { pptr_t f; cap_t frame_cap; seL4_SlotPos slot_pos_before; seL4_SlotPos slot_pos_after; slot_pos_before = ndks_boot.slot_pos_cur; for (f = reg.start; f < reg.end; f += BIT(PAGE_BITS)) { if (do_map) { frame_cap = create_mapped_it_frame_cap(pd_cap, f, pptr_to_paddr((void *)(f - pv_offset)), IT_ASID, false, true); } else { frame_cap = create_unmapped_it_frame_cap(f, false); } if (!provide_cap(root_cnode_cap, frame_cap)) return (create_frames_of_region_ret_t) { S_REG_EMPTY, false }; } slot_pos_after = ndks_boot.slot_pos_cur; return (create_frames_of_region_ret_t) { (seL4_SlotRegion) { slot_pos_before, slot_pos_after }, true }; } BOOT_CODE cap_t create_it_asid_pool(cap_t root_cnode_cap) { cap_t ap_cap = cap_asid_pool_cap_new(IT_ASID >> asidLowBits, rootserver.asid_pool); write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadASIDPool), ap_cap); /* create ASID control cap */ write_slot( SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapASIDControl), cap_asid_control_cap_new() ); return ap_cap; } #ifdef CONFIG_KERNEL_MCS BOOT_CODE static bool_t configure_sched_context(tcb_t *tcb, sched_context_t *sc_pptr, ticks_t timeslice, word_t core) { tcb->tcbSchedContext = sc_pptr; REFILL_NEW(tcb->tcbSchedContext, MIN_REFILLS, timeslice, 0, core); tcb->tcbSchedContext->scTcb = tcb; return true; } BOOT_CODE bool_t init_sched_control(cap_t root_cnode_cap, word_t num_nodes) { seL4_SlotPos slot_pos_before = ndks_boot.slot_pos_cur; /* create a sched control cap for each core */ for (unsigned int i = 0; i < num_nodes; i++) { if (!provide_cap(root_cnode_cap, cap_sched_control_cap_new(i))) { printf("can't init sched_control for node %u, provide_cap() failed\n", i); return false; } } /* update boot info with slot region for sched control caps */ ndks_boot.bi_frame->schedcontrol = (seL4_SlotRegion) { .start = slot_pos_before, .end = ndks_boot.slot_pos_cur }; return true; } #endif BOOT_CODE bool_t create_idle_thread(void) { pptr_t pptr; #ifdef ENABLE_SMP_SUPPORT for (unsigned int i = 0; i < CONFIG_MAX_NUM_NODES; i++) { #endif /* ENABLE_SMP_SUPPORT */ pptr = (pptr_t) &ksIdleThreadTCB[SMP_TERNARY(i, 0)]; NODE_STATE_ON_CORE(ksIdleThread, i) = TCB_PTR(pptr + TCB_OFFSET); configureIdleThread(NODE_STATE_ON_CORE(ksIdleThread, i)); #ifdef CONFIG_DEBUG_BUILD setThreadName(NODE_STATE_ON_CORE(ksIdleThread, i), "idle_thread"); #endif SMP_COND_STATEMENT(NODE_STATE_ON_CORE(ksIdleThread, i)->tcbAffinity = i); #ifdef CONFIG_KERNEL_MCS bool_t result = configure_sched_context(NODE_STATE_ON_CORE(ksIdleThread, i), SC_PTR(&ksIdleThreadSC[SMP_TERNARY(i, 0)]), usToTicks(CONFIG_BOOT_THREAD_TIME_SLICE * US_IN_MS), SMP_TERNARY(i, 0)); SMP_COND_STATEMENT(NODE_STATE_ON_CORE(ksIdleThread, i)->tcbSchedContext->scCore = i;) if (!result) { printf("Kernel init failed: Unable to allocate sc for idle thread\n"); return false; } #endif #ifdef ENABLE_SMP_SUPPORT } #endif /* ENABLE_SMP_SUPPORT */ return true; } BOOT_CODE tcb_t *create_initial_thread(cap_t root_cnode_cap, cap_t it_pd_cap, vptr_t ui_v_entry, vptr_t bi_frame_vptr, vptr_t ipcbuf_vptr, cap_t ipcbuf_cap) { tcb_t *tcb = TCB_PTR(rootserver.tcb + TCB_OFFSET); #ifndef CONFIG_KERNEL_MCS tcb->tcbTimeSlice = CONFIG_TIME_SLICE; #endif Arch_initContext(&tcb->tcbArch.tcbContext); /* derive a copy of the IPC buffer cap for inserting */ deriveCap_ret_t dc_ret = deriveCap(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadIPCBuffer), ipcbuf_cap); if (dc_ret.status != EXCEPTION_NONE) { printf("Failed to derive copy of IPC Buffer\n"); return NULL; } /* initialise TCB (corresponds directly to abstract specification) */ cteInsert( root_cnode_cap, SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadCNode), SLOT_PTR(rootserver.tcb, tcbCTable) ); cteInsert( it_pd_cap, SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadVSpace), SLOT_PTR(rootserver.tcb, tcbVTable) ); cteInsert( dc_ret.cap, SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadIPCBuffer), SLOT_PTR(rootserver.tcb, tcbBuffer) ); tcb->tcbIPCBuffer = ipcbuf_vptr; setRegister(tcb, capRegister, bi_frame_vptr); setNextPC(tcb, ui_v_entry); /* initialise TCB */ #ifdef CONFIG_KERNEL_MCS if (!configure_sched_context(tcb, SC_PTR(rootserver.sc), usToTicks(CONFIG_BOOT_THREAD_TIME_SLICE * US_IN_MS), 0)) { return NULL; } #endif tcb->tcbPriority = seL4_MaxPrio; tcb->tcbMCP = seL4_MaxPrio; tcb->tcbDomain = ksDomSchedule[ksDomScheduleIdx].domain; #ifndef CONFIG_KERNEL_MCS setupReplyMaster(tcb); #endif setThreadState(tcb, ThreadState_Running); ksCurDomain = ksDomSchedule[ksDomScheduleIdx].domain; #ifdef CONFIG_KERNEL_MCS ksDomainTime = usToTicks(ksDomSchedule[ksDomScheduleIdx].length * US_IN_MS); #else ksDomainTime = ksDomSchedule[ksDomScheduleIdx].length; #endif assert(ksCurDomain < CONFIG_NUM_DOMAINS && ksDomainTime > 0); #ifndef CONFIG_KERNEL_MCS SMP_COND_STATEMENT(tcb->tcbAffinity = 0); #endif /* create initial thread's TCB cap */ cap_t cap = cap_thread_cap_new(TCB_REF(tcb)); write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadTCB), cap); #ifdef CONFIG_KERNEL_MCS cap = cap_sched_context_cap_new(SC_REF(tcb->tcbSchedContext), seL4_MinSchedContextBits); write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadSC), cap); #endif #ifdef CONFIG_DEBUG_BUILD setThreadName(tcb, "rootserver"); #endif return tcb; } BOOT_CODE void init_core_state(tcb_t *scheduler_action) { #ifdef CONFIG_HAVE_FPU NODE_STATE(ksActiveFPUState) = NULL; #endif #ifdef CONFIG_DEBUG_BUILD /* add initial threads to the debug queue */ NODE_STATE(ksDebugTCBs) = NULL; if (scheduler_action != SchedulerAction_ResumeCurrentThread && scheduler_action != SchedulerAction_ChooseNewThread) { tcbDebugAppend(scheduler_action); } tcbDebugAppend(NODE_STATE(ksIdleThread)); #endif NODE_STATE(ksSchedulerAction) = scheduler_action; NODE_STATE(ksCurThread) = NODE_STATE(ksIdleThread); #ifdef CONFIG_KERNEL_MCS NODE_STATE(ksCurSC) = NODE_STATE(ksCurThread->tcbSchedContext); NODE_STATE(ksConsumed) = 0; NODE_STATE(ksReprogram) = true; NODE_STATE(ksReleaseHead) = NULL; NODE_STATE(ksCurTime) = getCurrentTime(); #endif } BOOT_CODE static bool_t provide_untyped_cap( cap_t root_cnode_cap, bool_t device_memory, pptr_t pptr, word_t size_bits, seL4_SlotPos first_untyped_slot ) { bool_t ret; cap_t ut_cap; word_t i = ndks_boot.slot_pos_cur - first_untyped_slot; if (i < CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS) { ndks_boot.bi_frame->untypedList[i] = (seL4_UntypedDesc) { pptr_to_paddr((void *)pptr), size_bits, device_memory, {0} }; ut_cap = cap_untyped_cap_new(MAX_FREE_INDEX(size_bits), device_memory, size_bits, pptr); ret = provide_cap(root_cnode_cap, ut_cap); } else { printf("Kernel init: Too many untyped regions for boot info\n"); ret = true; } return ret; } BOOT_CODE static bool_t create_untypeds_for_region( cap_t root_cnode_cap, bool_t device_memory, region_t reg, seL4_SlotPos first_untyped_slot ) { while (!is_reg_empty(reg)) { /* Calculate the bit size of the region. */ unsigned int size_bits = seL4_WordBits - 1 - clzl(reg.end - reg.start); /* The size can't exceed the largest possible untyped size. */ if (size_bits > seL4_MaxUntypedBits) { size_bits = seL4_MaxUntypedBits; } /* The start address 0 satisfies any alignment needs, otherwise ensure * the region's bit size does not exceed the alignment of the region. */ if (0 != reg.start) { unsigned int align_bits = ctzl(reg.start); if (size_bits > align_bits) { size_bits = align_bits; } } /* Provide an untyped capability for the region only if it is large * enough to be retyped into objects later. Otherwise the region can't * be used anyway. */ if (size_bits >= seL4_MinUntypedBits) { if (!provide_untyped_cap(root_cnode_cap, device_memory, reg.start, size_bits, first_untyped_slot)) { return false; } } reg.start += BIT(size_bits); } return true; } BOOT_CODE bool_t create_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg) { seL4_SlotPos first_untyped_slot = ndks_boot.slot_pos_cur; 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, first_untyped_slot)) { printf("ERROR: creation of untypeds for device region #%u at" " [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"] failed\n", (unsigned int)i, reg.start, reg.end); 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 }); if (!create_untypeds_for_region(root_cnode_cap, true, reg, first_untyped_slot)) { printf("ERROR: creation of untypeds for top device region" " [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"] failed\n", reg.start, reg.end); return false; } } /* if boot_mem_reuse_reg is not empty, we can create UT objs from boot code/data frames */ if (!create_untypeds_for_region(root_cnode_cap, false, boot_mem_reuse_reg, first_untyped_slot)) { printf("ERROR: creation of untypeds for recycled boot memory" " [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"] failed\n", boot_mem_reuse_reg.start, boot_mem_reuse_reg.end); return false; } /* convert remaining freemem into UT objects and provide the caps */ for (word_t i = 0; i < ARRAY_SIZE(ndks_boot.freemem); i++) { region_t reg = ndks_boot.freemem[i]; ndks_boot.freemem[i] = REG_EMPTY; if (!create_untypeds_for_region(root_cnode_cap, false, reg, first_untyped_slot)) { printf("ERROR: creation of untypeds for free memory region #%u at" " [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"] failed\n", (unsigned int)i, reg.start, reg.end); return false; } } ndks_boot.bi_frame->untyped = (seL4_SlotRegion) { .start = first_untyped_slot, .end = ndks_boot.slot_pos_cur }; return true; } BOOT_CODE void bi_finalise(void) { ndks_boot.bi_frame->empty = (seL4_SlotRegion) { .start = ndks_boot.slot_pos_cur, .end = BIT(CONFIG_ROOT_CNODE_SIZE_BITS) }; } BOOT_CODE static inline pptr_t ceiling_kernel_window(pptr_t p) { /* Adjust address if it exceeds the kernel window * Note that we compare physical address in case of overflow. */ if (pptr_to_paddr((void *)p) > PADDR_TOP) { p = PPTR_TOP; } return p; } BOOT_CODE static bool_t check_available_memory(word_t n_available, const p_region_t *available) { /* The system configuration is broken if no region is available. */ if (0 == n_available) { printf("ERROR: no memory regions available\n"); return false; } printf("available phys memory regions: %"SEL4_PRIu_word"\n", n_available); /* Force ordering and exclusivity of available regions. */ for (word_t i = 0; i < n_available; i++) { const p_region_t *r = &available[i]; printf(" [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"]\n", r->start, r->end); /* Available regions must be sane */ if (r->start > r->end) { printf("ERROR: memory region %"SEL4_PRIu_word" has start > end\n", i); return false; } /* Available regions can't be empty. */ if (r->start == r->end) { printf("ERROR: memory region %"SEL4_PRIu_word" empty\n", i); return false; } /* Regions must be ordered and must not overlap. */ if ((i > 0) && (r->start < available[i - 1].end)) { printf("ERROR: memory region %d in wrong order\n", (int)i); return false; } } return true; } BOOT_CODE static bool_t check_reserved_memory(word_t n_reserved, const region_t *reserved) { printf("reserved virt address space regions: %"SEL4_PRIu_word"\n", n_reserved); /* Force ordering and exclusivity of reserved regions. */ for (word_t i = 0; i < n_reserved; i++) { const region_t *r = &reserved[i]; printf(" [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"]\n", r->start, r->end); /* Reserved regions must be sane, the size is allowed to be zero. */ if (r->start > r->end) { printf("ERROR: reserved region %"SEL4_PRIu_word" has start > end\n", i); return false; } /* Regions must be ordered and must not overlap. */ if ((i > 0) && (r->start < reserved[i - 1].end)) { printf("ERROR: reserved region %"SEL4_PRIu_word" in wrong order\n", i); return false; } } return true; } /* we can't declare arrays on the stack, so this is space for * the function below to use. */ BOOT_BSS static region_t avail_reg[MAX_NUM_FREEMEM_REG]; /** * Dynamically initialise the available memory on the platform. * A region represents an area of memory. */ BOOT_CODE bool_t init_freemem(word_t n_available, const p_region_t *available, word_t n_reserved, const region_t *reserved, v_region_t it_v_reg, word_t extra_bi_size_bits) { if (!check_available_memory(n_available, available)) { return false; } if (!check_reserved_memory(n_reserved, reserved)) { return false; } for (word_t i = 0; i < ARRAY_SIZE(ndks_boot.freemem); i++) { ndks_boot.freemem[i] = REG_EMPTY; } /* convert the available regions to pptrs */ for (word_t i = 0; i < n_available; i++) { avail_reg[i] = paddr_to_pptr_reg(available[i]); avail_reg[i].end = ceiling_kernel_window(avail_reg[i].end); avail_reg[i].start = ceiling_kernel_window(avail_reg[i].start); } word_t a = 0; word_t r = 0; /* Now iterate through the available regions, removing any reserved regions. */ while (a < n_available && r < n_reserved) { if (reserved[r].start == reserved[r].end) { /* reserved region is empty - skip it */ r++; } else if (avail_reg[a].start >= avail_reg[a].end) { /* skip the entire region - it's empty now after trimming */ 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 */ insert_region(avail_reg[a]); a++; } else { /* the reserved region overlaps with the available region */ if (reserved[r].start <= avail_reg[a].start) { /* 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); /* take the first chunk of the available region and move * the start to the end of the reserved region */ region_t m = avail_reg[a]; m.end = reserved[r].start; 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++; } } } } 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) { insert_region(avail_reg[a]); } } /* now try to fit the root server objects into a region */ int i = ARRAY_SIZE(ndks_boot.freemem) - 1; if (!is_reg_empty(ndks_boot.freemem[i])) { printf("ERROR: insufficient MAX_NUM_FREEMEM_REG (%u)\n", (unsigned int)MAX_NUM_FREEMEM_REG); return false; } /* 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--) { /* Invariant: both i and (i + 1) are valid indices in ndks_boot.freemem. */ assert(i < ARRAY_SIZE(ndks_boot.freemem) - 1); /* Invariant; the region at index i is the current candidate. * Invariant: regions 0 up to (i - 1), if any, are additional candidates. * Invariant: region (i + 1) is empty. */ assert(is_reg_empty(ndks_boot.freemem[i + 1])); /* Invariant: regions above (i + 1), if any, are empty or too small to use. * Invariant: all non-empty regions are ordered, disjoint and unallocated. */ /* We make a fresh variable to index the known-empty region, because the * SimplExportAndRefine verification test has poor support for array * indices that are sums of variables and small constants. */ int empty_index = i + 1; /* Try to take the top-most suitably sized and aligned chunk. */ pptr_t unaligned_start = ndks_boot.freemem[i].end - size; pptr_t start = ROUND_DOWN(unaligned_start, max); /* if unaligned_start didn't underflow, and start fits in the region, * then we've found a region that fits the root server objects. */ if (unaligned_start <= ndks_boot.freemem[i].end && start >= ndks_boot.freemem[i].start) { create_rootserver_objects(start, it_v_reg, extra_bi_size_bits); /* There may be leftovers before and after the memory we used. */ /* Shuffle the after leftover up to the empty slot (i + 1). */ ndks_boot.freemem[empty_index] = (region_t) { .start = start + size, .end = ndks_boot.freemem[i].end }; /* Leave the before leftover in current slot i. */ ndks_boot.freemem[i].end = start; /* Regions i and (i + 1) are now well defined, ordered, disjoint, * and unallocated, so we can return successfully. */ return true; } /* Region i isn't big enough, so shuffle it up to slot (i + 1), * which we know is unused. */ ndks_boot.freemem[empty_index] = ndks_boot.freemem[i]; /* Now region i is unused, so make it empty to reestablish the invariant * for the next iteration (when it will be slot i + 1). */ ndks_boot.freemem[i] = REG_EMPTY; } /* We didn't find a big enough region. */ printf("ERROR: no free memory region is big enough for root server " "objects, need size/alignment of 2^%"SEL4_PRIu_word"\n", max); return false; }