1/*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 */
6
7#include <assert.h>
8#include <kernel/boot.h>
9#include <kernel/thread.h>
10#include <machine/io.h>
11#include <machine/registerset.h>
12#include <model/statedata.h>
13#include <arch/machine.h>
14#include <arch/kernel/boot.h>
15#include <arch/kernel/vspace.h>
16#include <linker.h>
17#include <hardware.h>
18#include <util.h>
19
20/* (node-local) state accessed only during bootstrapping */
21ndks_boot_t ndks_boot BOOT_BSS;
22
23rootserver_mem_t rootserver BOOT_BSS;
24static region_t rootserver_mem BOOT_BSS;
25
26BOOT_CODE static void merge_regions(void)
27{
28    /* Walk through reserved regions and see if any can be merged */
29    for (word_t i = 1; i < ndks_boot.resv_count;) {
30        if (ndks_boot.reserved[i - 1].end == ndks_boot.reserved[i].start) {
31            /* extend earlier region */
32            ndks_boot.reserved[i - 1].end = ndks_boot.reserved[i].end;
33            /* move everything else down */
34            for (word_t j = i + 1; j < ndks_boot.resv_count; j++) {
35                ndks_boot.reserved[j - 1] = ndks_boot.reserved[j];
36            }
37
38            ndks_boot.resv_count--;
39            /* don't increment i in case there are multiple adjacent regions */
40        } else {
41            i++;
42        }
43    }
44}
45
46BOOT_CODE bool_t reserve_region(p_region_t reg)
47{
48    word_t i;
49    assert(reg.start <= reg.end);
50    if (reg.start == reg.end) {
51        return true;
52    }
53
54    /* keep the regions in order */
55    for (i = 0; i < ndks_boot.resv_count; i++) {
56        /* Try and merge the region to an existing one, if possible */
57        if (ndks_boot.reserved[i].start == reg.end) {
58            ndks_boot.reserved[i].start = reg.start;
59            merge_regions();
60            return true;
61        }
62        if (ndks_boot.reserved[i].end == reg.start) {
63            ndks_boot.reserved[i].end = reg.end;
64            merge_regions();
65            return true;
66        }
67        /* Otherwise figure out where it should go. */
68        if (ndks_boot.reserved[i].start > reg.end) {
69            /* move regions down, making sure there's enough room */
70            if (ndks_boot.resv_count + 1 >= MAX_NUM_RESV_REG) {
71                printf("Can't mark region 0x%lx-0x%lx as reserved, try increasing MAX_NUM_RESV_REG (currently %d)\n",
72                       reg.start, reg.end, (int)MAX_NUM_RESV_REG);
73                return false;
74            }
75            for (word_t j = ndks_boot.resv_count; j > i; j--) {
76                ndks_boot.reserved[j] = ndks_boot.reserved[j - 1];
77            }
78            /* insert the new region */
79            ndks_boot.reserved[i] = reg;
80            ndks_boot.resv_count++;
81            return true;
82        }
83    }
84
85    if (i + 1 == MAX_NUM_RESV_REG) {
86        printf("Can't mark region 0x%lx-0x%lx as reserved, try increasing MAX_NUM_RESV_REG (currently %d)\n",
87               reg.start, reg.end, (int)MAX_NUM_RESV_REG);
88        return false;
89    }
90
91    ndks_boot.reserved[i] = reg;
92    ndks_boot.resv_count++;
93
94    return true;
95}
96
97BOOT_CODE bool_t insert_region(region_t reg)
98{
99    word_t i;
100
101    assert(reg.start <= reg.end);
102    if (is_reg_empty(reg)) {
103        return true;
104    }
105    for (i = 0; i < MAX_NUM_FREEMEM_REG; i++) {
106        if (is_reg_empty(ndks_boot.freemem[i])) {
107            reserve_region(pptr_to_paddr_reg(reg));
108            ndks_boot.freemem[i] = reg;
109            return true;
110        }
111    }
112#ifdef CONFIG_ARCH_ARM
113    /* boot.h should have calculated MAX_NUM_FREEMEM_REG correctly.
114     * If we've run out, then something is wrong.
115     * Note that the capDL allocation toolchain does not know about
116     * MAX_NUM_FREEMEM_REG, so throwing away regions may prevent
117     * capDL applications from being loaded! */
118    printf("Can't fit memory region 0x%lx-0x%lx, try increasing MAX_NUM_FREEMEM_REG (currently %d)\n",
119           reg.start, reg.end, (int)MAX_NUM_FREEMEM_REG);
120    assert(!"Ran out of freemem slots");
121#else
122    printf("Dropping memory region 0x%lx-0x%lx, try increasing MAX_NUM_FREEMEM_REG (currently %d)\n",
123           reg.start, reg.end, (int)MAX_NUM_FREEMEM_REG);
124#endif
125    return false;
126}
127
128BOOT_CODE static pptr_t alloc_rootserver_obj(word_t size_bits, word_t n)
129{
130    pptr_t allocated = rootserver_mem.start;
131    /* allocated memory must be aligned */
132    assert(allocated % BIT(size_bits) == 0);
133    rootserver_mem.start += (n * BIT(size_bits));
134    /* we must not have run out of memory */
135    assert(rootserver_mem.start <= rootserver_mem.end);
136    memzero((void *) allocated, n * BIT(size_bits));
137    return allocated;
138}
139
140BOOT_CODE static word_t rootserver_max_size_bits(word_t extra_bi_size_bits)
141{
142    word_t cnode_size_bits = CONFIG_ROOT_CNODE_SIZE_BITS + seL4_SlotBits;
143    word_t max = MAX(cnode_size_bits, seL4_VSpaceBits);
144    return MAX(max, extra_bi_size_bits);
145}
146
147BOOT_CODE static word_t calculate_rootserver_size(v_region_t v_reg, word_t extra_bi_size_bits)
148{
149    /* work out how much memory we need for root server objects */
150    word_t size = BIT(CONFIG_ROOT_CNODE_SIZE_BITS + seL4_SlotBits);
151    size += BIT(seL4_TCBBits); // root thread tcb
152    size += 2 * BIT(seL4_PageBits); // boot info + ipc buf
153    size += BIT(seL4_ASIDPoolBits);
154    size += extra_bi_size_bits > 0 ? BIT(extra_bi_size_bits) : 0;
155    size += BIT(seL4_VSpaceBits); // root vspace
156#ifdef CONFIG_KERNEL_MCS
157    size += BIT(seL4_MinSchedContextBits); // root sched context
158#endif
159    /* for all archs, seL4_PageTable Bits is the size of all non top-level paging structures */
160    return size + arch_get_n_paging(v_reg) * BIT(seL4_PageTableBits);
161}
162
163BOOT_CODE static void maybe_alloc_extra_bi(word_t cmp_size_bits, word_t extra_bi_size_bits)
164{
165    if (extra_bi_size_bits >= cmp_size_bits && rootserver.extra_bi == 0) {
166        rootserver.extra_bi = alloc_rootserver_obj(extra_bi_size_bits, 1);
167    }
168}
169
170BOOT_CODE void create_rootserver_objects(pptr_t start, v_region_t v_reg, word_t extra_bi_size_bits)
171{
172    /* the largest object the PD, the root cnode, or the extra boot info */
173    word_t cnode_size_bits = CONFIG_ROOT_CNODE_SIZE_BITS + seL4_SlotBits;
174    word_t max = rootserver_max_size_bits(extra_bi_size_bits);
175
176    word_t size = calculate_rootserver_size(v_reg, extra_bi_size_bits);
177    rootserver_mem.start = start;
178    rootserver_mem.end = start + size;
179
180    maybe_alloc_extra_bi(max, extra_bi_size_bits);
181
182    /* the root cnode is at least 4k, so it could be larger or smaller than a pd. */
183#if (CONFIG_ROOT_CNODE_SIZE_BITS + seL4_SlotBits) > seL4_VSpaceBits
184    rootserver.cnode = alloc_rootserver_obj(cnode_size_bits, 1);
185    maybe_alloc_extra_bi(seL4_VSpaceBits, extra_bi_size_bits);
186    rootserver.vspace = alloc_rootserver_obj(seL4_VSpaceBits, 1);
187#else
188    rootserver.vspace = alloc_rootserver_obj(seL4_VSpaceBits, 1);
189    maybe_alloc_extra_bi(cnode_size_bits, extra_bi_size_bits);
190    rootserver.cnode = alloc_rootserver_obj(cnode_size_bits, 1);
191#endif
192
193    /* at this point we are up to creating 4k objects - which is the min size of
194     * extra_bi so this is the last chance to allocate it */
195    maybe_alloc_extra_bi(seL4_PageBits, extra_bi_size_bits);
196    rootserver.asid_pool = alloc_rootserver_obj(seL4_ASIDPoolBits, 1);
197    rootserver.ipc_buf = alloc_rootserver_obj(seL4_PageBits, 1);
198    rootserver.boot_info = alloc_rootserver_obj(seL4_PageBits, 1);
199
200    /* TCBs on aarch32 can be larger than page tables in certain configs */
201#if seL4_TCBBits >= seL4_PageTableBits
202    rootserver.tcb = alloc_rootserver_obj(seL4_TCBBits, 1);
203#endif
204
205    /* paging structures are 4k on every arch except aarch32 (1k) */
206    word_t n = arch_get_n_paging(v_reg);
207    rootserver.paging.start = alloc_rootserver_obj(seL4_PageTableBits, n);
208    rootserver.paging.end = rootserver.paging.start + n * BIT(seL4_PageTableBits);
209
210    /* for most archs, TCBs are smaller than page tables */
211#if seL4_TCBBits < seL4_PageTableBits
212    rootserver.tcb = alloc_rootserver_obj(seL4_TCBBits, 1);
213#endif
214
215#ifdef CONFIG_KERNEL_MCS
216    rootserver.sc = alloc_rootserver_obj(seL4_MinSchedContextBits, 1);
217#endif
218    /* we should have allocated all our memory */
219    assert(rootserver_mem.start == rootserver_mem.end);
220}
221
222BOOT_CODE void write_slot(slot_ptr_t slot_ptr, cap_t cap)
223{
224    slot_ptr->cap = cap;
225
226    slot_ptr->cteMDBNode = nullMDBNode;
227    mdb_node_ptr_set_mdbRevocable(&slot_ptr->cteMDBNode, true);
228    mdb_node_ptr_set_mdbFirstBadged(&slot_ptr->cteMDBNode, true);
229}
230
231/* Our root CNode needs to be able to fit all the initial caps and not
232 * cover all of memory.
233 */
234compile_assert(root_cnode_size_valid,
235               CONFIG_ROOT_CNODE_SIZE_BITS < 32 - seL4_SlotBits &&
236               BIT(CONFIG_ROOT_CNODE_SIZE_BITS) >= seL4_NumInitialCaps &&
237               BIT(CONFIG_ROOT_CNODE_SIZE_BITS) >= (seL4_PageBits - seL4_SlotBits))
238
239BOOT_CODE cap_t
240create_root_cnode(void)
241{
242    /* write the number of root CNode slots to global state */
243    ndks_boot.slot_pos_max = BIT(CONFIG_ROOT_CNODE_SIZE_BITS);
244
245    cap_t cap =
246        cap_cnode_cap_new(
247            CONFIG_ROOT_CNODE_SIZE_BITS,      /* radix      */
248            wordBits - CONFIG_ROOT_CNODE_SIZE_BITS, /* guard size */
249            0,                                /* guard      */
250            rootserver.cnode              /* pptr       */
251        );
252
253    /* write the root CNode cap into the root CNode */
254    write_slot(SLOT_PTR(rootserver.cnode, seL4_CapInitThreadCNode), cap);
255
256    return cap;
257}
258
259/* Check domain scheduler assumptions. */
260compile_assert(num_domains_valid,
261               CONFIG_NUM_DOMAINS >= 1 && CONFIG_NUM_DOMAINS <= 256)
262compile_assert(num_priorities_valid,
263               CONFIG_NUM_PRIORITIES >= 1 && CONFIG_NUM_PRIORITIES <= 256)
264
265BOOT_CODE void
266create_domain_cap(cap_t root_cnode_cap)
267{
268    /* Check domain scheduler assumptions. */
269    assert(ksDomScheduleLength > 0);
270    for (word_t i = 0; i < ksDomScheduleLength; i++) {
271        assert(ksDomSchedule[i].domain < CONFIG_NUM_DOMAINS);
272        assert(ksDomSchedule[i].length > 0);
273    }
274
275    cap_t cap = cap_domain_cap_new();
276    write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapDomain), cap);
277}
278
279
280BOOT_CODE cap_t create_ipcbuf_frame_cap(cap_t root_cnode_cap, cap_t pd_cap, vptr_t vptr)
281{
282    clearMemory((void *)rootserver.ipc_buf, PAGE_BITS);
283
284    /* create a cap of it and write it into the root CNode */
285    cap_t cap = create_mapped_it_frame_cap(pd_cap, rootserver.ipc_buf, vptr, IT_ASID, false, false);
286    write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadIPCBuffer), cap);
287
288    return cap;
289}
290
291BOOT_CODE void create_bi_frame_cap(cap_t root_cnode_cap, cap_t pd_cap, vptr_t vptr)
292{
293    /* create a cap of it and write it into the root CNode */
294    cap_t cap = create_mapped_it_frame_cap(pd_cap, rootserver.boot_info, vptr, IT_ASID, false, false);
295    write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapBootInfoFrame), cap);
296}
297
298BOOT_CODE word_t calculate_extra_bi_size_bits(word_t extra_size)
299{
300    if (extra_size == 0) {
301        return 0;
302    }
303
304    word_t clzl_ret = clzl(ROUND_UP(extra_size, seL4_PageBits));
305    word_t msb = seL4_WordBits - 1 - clzl_ret;
306    /* If region is bigger than a page, make sure we overallocate rather than underallocate */
307    if (extra_size > BIT(msb)) {
308        msb++;
309    }
310    return msb;
311}
312
313BOOT_CODE void populate_bi_frame(node_id_t node_id, word_t num_nodes, vptr_t ipcbuf_vptr,
314                                 word_t extra_bi_size)
315{
316    clearMemory((void *) rootserver.boot_info, BI_FRAME_SIZE_BITS);
317    if (extra_bi_size) {
318        clearMemory((void *) rootserver.extra_bi, calculate_extra_bi_size_bits(extra_bi_size));
319    }
320
321    /* initialise bootinfo-related global state */
322    ndks_boot.bi_frame = BI_PTR(rootserver.boot_info);
323    ndks_boot.slot_pos_cur = seL4_NumInitialCaps;
324    BI_PTR(rootserver.boot_info)->nodeID = node_id;
325    BI_PTR(rootserver.boot_info)->numNodes = num_nodes;
326    BI_PTR(rootserver.boot_info)->numIOPTLevels = 0;
327    BI_PTR(rootserver.boot_info)->ipcBuffer = (seL4_IPCBuffer *) ipcbuf_vptr;
328    BI_PTR(rootserver.boot_info)->initThreadCNodeSizeBits = CONFIG_ROOT_CNODE_SIZE_BITS;
329    BI_PTR(rootserver.boot_info)->initThreadDomain = ksDomSchedule[ksDomScheduleIdx].domain;
330    BI_PTR(rootserver.boot_info)->extraLen = extra_bi_size;
331}
332
333BOOT_CODE bool_t provide_cap(cap_t root_cnode_cap, cap_t cap)
334{
335    if (ndks_boot.slot_pos_cur >= ndks_boot.slot_pos_max) {
336        printf("Kernel init failed: ran out of cap slots\n");
337        return false;
338    }
339    write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), ndks_boot.slot_pos_cur), cap);
340    ndks_boot.slot_pos_cur++;
341    return true;
342}
343
344BOOT_CODE create_frames_of_region_ret_t create_frames_of_region(
345    cap_t    root_cnode_cap,
346    cap_t    pd_cap,
347    region_t reg,
348    bool_t   do_map,
349    sword_t  pv_offset
350)
351{
352    pptr_t     f;
353    cap_t      frame_cap;
354    seL4_SlotPos slot_pos_before;
355    seL4_SlotPos slot_pos_after;
356
357    slot_pos_before = ndks_boot.slot_pos_cur;
358
359    for (f = reg.start; f < reg.end; f += BIT(PAGE_BITS)) {
360        if (do_map) {
361            frame_cap = create_mapped_it_frame_cap(pd_cap, f, pptr_to_paddr((void *)(f - pv_offset)), IT_ASID, false, true);
362        } else {
363            frame_cap = create_unmapped_it_frame_cap(f, false);
364        }
365        if (!provide_cap(root_cnode_cap, frame_cap))
366            return (create_frames_of_region_ret_t) {
367            S_REG_EMPTY, false
368        };
369    }
370
371    slot_pos_after = ndks_boot.slot_pos_cur;
372
373    return (create_frames_of_region_ret_t) {
374        (seL4_SlotRegion) { slot_pos_before, slot_pos_after }, true
375    };
376}
377
378BOOT_CODE cap_t create_it_asid_pool(cap_t root_cnode_cap)
379{
380    cap_t ap_cap = cap_asid_pool_cap_new(IT_ASID >> asidLowBits, rootserver.asid_pool);
381    write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadASIDPool), ap_cap);
382
383    /* create ASID control cap */
384    write_slot(
385        SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapASIDControl),
386        cap_asid_control_cap_new()
387    );
388
389    return ap_cap;
390}
391
392#ifdef CONFIG_KERNEL_MCS
393BOOT_CODE static bool_t configure_sched_context(tcb_t *tcb, sched_context_t *sc_pptr, ticks_t timeslice, word_t core)
394{
395    tcb->tcbSchedContext = sc_pptr;
396    REFILL_NEW(tcb->tcbSchedContext, MIN_REFILLS, timeslice, 0, core);
397
398    tcb->tcbSchedContext->scTcb = tcb;
399    return true;
400}
401
402BOOT_CODE bool_t init_sched_control(cap_t root_cnode_cap, word_t num_nodes)
403{
404    bool_t ret = true;
405    seL4_SlotPos slot_pos_before = ndks_boot.slot_pos_cur;
406    /* create a sched control cap for each core */
407    for (int i = 0; i < num_nodes && ret; i++) {
408        ret = provide_cap(root_cnode_cap, cap_sched_control_cap_new(i));
409    }
410
411    if (!ret) {
412        return false;
413    }
414
415    /* update boot info with slot region for sched control caps */
416    ndks_boot.bi_frame->schedcontrol = (seL4_SlotRegion) {
417        .start = slot_pos_before,
418        .end = ndks_boot.slot_pos_cur
419    };
420
421    return true;
422}
423#endif
424
425BOOT_CODE bool_t create_idle_thread(void)
426{
427    pptr_t pptr;
428
429#ifdef ENABLE_SMP_SUPPORT
430    for (int i = 0; i < CONFIG_MAX_NUM_NODES; i++) {
431#endif /* ENABLE_SMP_SUPPORT */
432        pptr = (pptr_t) &ksIdleThreadTCB[SMP_TERNARY(i, 0)];
433        NODE_STATE_ON_CORE(ksIdleThread, i) = TCB_PTR(pptr + TCB_OFFSET);
434        configureIdleThread(NODE_STATE_ON_CORE(ksIdleThread, i));
435#ifdef CONFIG_DEBUG_BUILD
436        setThreadName(NODE_STATE_ON_CORE(ksIdleThread, i), "idle_thread");
437#endif
438        SMP_COND_STATEMENT(NODE_STATE_ON_CORE(ksIdleThread, i)->tcbAffinity = i);
439#ifdef CONFIG_KERNEL_MCS
440        bool_t result = configure_sched_context(NODE_STATE_ON_CORE(ksIdleThread, i), SC_PTR(&ksIdleThreadSC[SMP_TERNARY(i, 0)]),
441                                                usToTicks(CONFIG_BOOT_THREAD_TIME_SLICE * US_IN_MS), SMP_TERNARY(i, 0));
442        SMP_COND_STATEMENT(NODE_STATE_ON_CORE(ksIdleThread, i)->tcbSchedContext->scCore = i;)
443        if (!result) {
444            printf("Kernel init failed: Unable to allocate sc for idle thread\n");
445            return false;
446        }
447#endif
448#ifdef ENABLE_SMP_SUPPORT
449    }
450#endif /* ENABLE_SMP_SUPPORT */
451    return true;
452}
453
454BOOT_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,
455                                       vptr_t ipcbuf_vptr, cap_t ipcbuf_cap)
456{
457    tcb_t *tcb = TCB_PTR(rootserver.tcb + TCB_OFFSET);
458#ifndef CONFIG_KERNEL_MCS
459    tcb->tcbTimeSlice = CONFIG_TIME_SLICE;
460#endif
461
462    Arch_initContext(&tcb->tcbArch.tcbContext);
463
464    /* derive a copy of the IPC buffer cap for inserting */
465    deriveCap_ret_t dc_ret = deriveCap(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadIPCBuffer), ipcbuf_cap);
466    if (dc_ret.status != EXCEPTION_NONE) {
467        printf("Failed to derive copy of IPC Buffer\n");
468        return NULL;
469    }
470
471    /* initialise TCB (corresponds directly to abstract specification) */
472    cteInsert(
473        root_cnode_cap,
474        SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadCNode),
475        SLOT_PTR(rootserver.tcb, tcbCTable)
476    );
477    cteInsert(
478        it_pd_cap,
479        SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadVSpace),
480        SLOT_PTR(rootserver.tcb, tcbVTable)
481    );
482    cteInsert(
483        dc_ret.cap,
484        SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadIPCBuffer),
485        SLOT_PTR(rootserver.tcb, tcbBuffer)
486    );
487    tcb->tcbIPCBuffer = ipcbuf_vptr;
488
489    setRegister(tcb, capRegister, bi_frame_vptr);
490    setNextPC(tcb, ui_v_entry);
491
492    /* initialise TCB */
493#ifdef CONFIG_KERNEL_MCS
494    if (!configure_sched_context(tcb, SC_PTR(rootserver.sc), usToTicks(CONFIG_BOOT_THREAD_TIME_SLICE * US_IN_MS), 0)) {
495        return NULL;
496    }
497#endif
498
499    tcb->tcbPriority = seL4_MaxPrio;
500    tcb->tcbMCP = seL4_MaxPrio;
501    tcb->tcbDomain = ksDomSchedule[ksDomScheduleIdx].domain;
502#ifndef CONFIG_KERNEL_MCS
503    setupReplyMaster(tcb);
504#endif
505    setThreadState(tcb, ThreadState_Running);
506
507    ksCurDomain = ksDomSchedule[ksDomScheduleIdx].domain;
508#ifdef CONFIG_KERNEL_MCS
509    ksDomainTime = usToTicks(ksDomSchedule[ksDomScheduleIdx].length * US_IN_MS);
510#else
511    ksDomainTime = ksDomSchedule[ksDomScheduleIdx].length;
512#endif
513    assert(ksCurDomain < CONFIG_NUM_DOMAINS && ksDomainTime > 0);
514
515#ifndef CONFIG_KERNEL_MCS
516    SMP_COND_STATEMENT(tcb->tcbAffinity = 0);
517#endif
518
519    /* create initial thread's TCB cap */
520    cap_t cap = cap_thread_cap_new(TCB_REF(tcb));
521    write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadTCB), cap);
522
523#ifdef CONFIG_KERNEL_MCS
524    cap = cap_sched_context_cap_new(SC_REF(tcb->tcbSchedContext), seL4_MinSchedContextBits);
525    write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadSC), cap);
526#endif
527#ifdef CONFIG_DEBUG_BUILD
528    setThreadName(tcb, "rootserver");
529#endif
530
531    return tcb;
532}
533
534BOOT_CODE void init_core_state(tcb_t *scheduler_action)
535{
536#ifdef CONFIG_HAVE_FPU
537    NODE_STATE(ksActiveFPUState) = NULL;
538#endif
539#ifdef CONFIG_DEBUG_BUILD
540    /* add initial threads to the debug queue */
541    NODE_STATE(ksDebugTCBs) = NULL;
542    if (scheduler_action != SchedulerAction_ResumeCurrentThread &&
543        scheduler_action != SchedulerAction_ChooseNewThread) {
544        tcbDebugAppend(scheduler_action);
545    }
546    tcbDebugAppend(NODE_STATE(ksIdleThread));
547#endif
548    NODE_STATE(ksSchedulerAction) = scheduler_action;
549    NODE_STATE(ksCurThread) = NODE_STATE(ksIdleThread);
550#ifdef CONFIG_KERNEL_MCS
551    NODE_STATE(ksCurSC) = NODE_STATE(ksCurThread->tcbSchedContext);
552    NODE_STATE(ksConsumed) = 0;
553    NODE_STATE(ksReprogram) = true;
554    NODE_STATE(ksReleaseHead) = NULL;
555    NODE_STATE(ksCurTime) = getCurrentTime();
556#endif
557}
558
559BOOT_CODE static bool_t provide_untyped_cap(
560    cap_t      root_cnode_cap,
561    bool_t     device_memory,
562    pptr_t     pptr,
563    word_t     size_bits,
564    seL4_SlotPos first_untyped_slot
565)
566{
567    bool_t ret;
568    cap_t ut_cap;
569    word_t i = ndks_boot.slot_pos_cur - first_untyped_slot;
570    if (i < CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS) {
571        ndks_boot.bi_frame->untypedList[i] = (seL4_UntypedDesc) {
572            pptr_to_paddr((void *)pptr), size_bits, device_memory, {0}
573        };
574        ut_cap = cap_untyped_cap_new(MAX_FREE_INDEX(size_bits),
575                                     device_memory, size_bits, pptr);
576        ret = provide_cap(root_cnode_cap, ut_cap);
577    } else {
578        printf("Kernel init: Too many untyped regions for boot info\n");
579        ret = true;
580    }
581    return ret;
582}
583
584BOOT_CODE bool_t create_untypeds_for_region(
585    cap_t      root_cnode_cap,
586    bool_t     device_memory,
587    region_t   reg,
588    seL4_SlotPos first_untyped_slot
589)
590{
591    word_t align_bits;
592    word_t size_bits;
593
594    while (!is_reg_empty(reg)) {
595        /* Determine the maximum size of the region */
596        size_bits = seL4_WordBits - 1 - clzl(reg.end - reg.start);
597
598        /* Determine the alignment of the region */
599        if (reg.start != 0) {
600            align_bits = ctzl(reg.start);
601        } else {
602            align_bits = size_bits;
603        }
604        /* Reduce size bits to align if needed */
605        if (align_bits < size_bits) {
606            size_bits = align_bits;
607        }
608        if (size_bits > seL4_MaxUntypedBits) {
609            size_bits = seL4_MaxUntypedBits;
610        }
611
612        if (size_bits >= seL4_MinUntypedBits) {
613            if (!provide_untyped_cap(root_cnode_cap, device_memory, reg.start, size_bits, first_untyped_slot)) {
614                return false;
615            }
616        }
617        reg.start += BIT(size_bits);
618    }
619    return true;
620}
621
622BOOT_CODE bool_t create_device_untypeds(cap_t root_cnode_cap, seL4_SlotPos slot_pos_before)
623{
624    paddr_t start = 0;
625    for (word_t i = 0; i < ndks_boot.resv_count; i++) {
626        if (start < ndks_boot.reserved[i].start) {
627            region_t reg = paddr_to_pptr_reg((p_region_t) {
628                start, ndks_boot.reserved[i].start
629            });
630            if (!create_untypeds_for_region(root_cnode_cap, true, reg, slot_pos_before)) {
631                return false;
632            }
633        }
634
635        start = ndks_boot.reserved[i].end;
636    }
637
638    if (start < CONFIG_PADDR_USER_DEVICE_TOP) {
639        region_t reg = paddr_to_pptr_reg((p_region_t) {
640            start, CONFIG_PADDR_USER_DEVICE_TOP
641        });
642        /*
643         * The auto-generated bitfield code will get upset if the
644         * end pptr is larger than the maximum pointer size for this architecture.
645         */
646        if (reg.end > PPTR_TOP) {
647            reg.end = PPTR_TOP;
648        }
649        if (!create_untypeds_for_region(root_cnode_cap, true, reg, slot_pos_before)) {
650            return false;
651        }
652    }
653    return true;
654}
655
656BOOT_CODE bool_t create_kernel_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg,
657                                        seL4_SlotPos first_untyped_slot)
658{
659    word_t     i;
660    region_t   reg;
661
662    /* if boot_mem_reuse_reg is not empty, we can create UT objs from boot code/data frames */
663    if (!create_untypeds_for_region(root_cnode_cap, false, boot_mem_reuse_reg, first_untyped_slot)) {
664        return false;
665    }
666
667    /* convert remaining freemem into UT objects and provide the caps */
668    for (i = 0; i < MAX_NUM_FREEMEM_REG; i++) {
669        reg = ndks_boot.freemem[i];
670        ndks_boot.freemem[i] = REG_EMPTY;
671        if (!create_untypeds_for_region(root_cnode_cap, false, reg, first_untyped_slot)) {
672            return false;
673        }
674    }
675
676    return true;
677}
678
679BOOT_CODE void bi_finalise(void)
680{
681    seL4_SlotPos slot_pos_start = ndks_boot.slot_pos_cur;
682    seL4_SlotPos slot_pos_end = ndks_boot.slot_pos_max;
683    ndks_boot.bi_frame->empty = (seL4_SlotRegion) {
684        slot_pos_start, slot_pos_end
685    };
686}
687
688static inline pptr_t ceiling_kernel_window(pptr_t p)
689{
690    /* Adjust address if it exceeds the kernel window
691     * Note that we compare physical address in case of overflow.
692     */
693    if (pptr_to_paddr((void *)p) > PADDR_TOP) {
694        p = PPTR_TOP;
695    }
696    return p;
697}
698
699/* we can't delcare arrays on the stack, so this is space for
700 * the below function to use. */
701static BOOT_DATA region_t avail_reg[MAX_NUM_FREEMEM_REG];
702/**
703 * Dynamically initialise the available memory on the platform.
704 * A region represents an area of memory.
705 */
706BOOT_CODE void init_freemem(word_t n_available, const p_region_t *available,
707                            word_t n_reserved, region_t *reserved,
708                            v_region_t it_v_reg, word_t extra_bi_size_bits)
709{
710    /* Force ordering and exclusivity of reserved regions */
711    for (word_t i = 0; n_reserved > 0 && i < n_reserved - 1; i++) {
712        assert(reserved[i].start <= reserved[i].end);
713        assert(reserved[i].end <= reserved[i + 1].start);
714    }
715
716    /* Force ordering and exclusivity of available regions */
717    assert(n_available > 0);
718    for (word_t i = 0; i < n_available - 1; i++) {
719        assert(available[i].start < available[i].end);
720        assert(available[i].end <= available[i + 1].start);
721    }
722
723    for (word_t i = 0; i < MAX_NUM_FREEMEM_REG; i++) {
724        ndks_boot.freemem[i] = REG_EMPTY;
725    }
726
727    /* convert the available regions to pptrs */
728    for (word_t i = 0; i < n_available; i++) {
729        avail_reg[i] = paddr_to_pptr_reg(available[i]);
730        avail_reg[i].end = ceiling_kernel_window(avail_reg[i].end);
731        avail_reg[i].start = ceiling_kernel_window(avail_reg[i].start);
732    }
733
734    word_t a = 0;
735    word_t r = 0;
736    /* Now iterate through the available regions, removing any reserved regions. */
737    while (a < n_available && r < n_reserved) {
738        if (reserved[r].start == reserved[r].end) {
739            /* reserved region is empty - skip it */
740            r++;
741        } else if (avail_reg[a].start >= avail_reg[a].end) {
742            /* skip the entire region - it's empty now after trimming */
743            a++;
744        } else if (reserved[r].end <= avail_reg[a].start) {
745            /* the reserved region is below the available region - skip it*/
746            reserve_region(pptr_to_paddr_reg(reserved[r]));
747            r++;
748        } else if (reserved[r].start >= avail_reg[a].end) {
749            /* the reserved region is above the available region - take the whole thing */
750            insert_region(avail_reg[a]);
751            a++;
752        } else {
753            /* the reserved region overlaps with the available region */
754            if (reserved[r].start <= avail_reg[a].start) {
755                /* the region overlaps with the start of the available region.
756                 * trim start of the available region */
757                avail_reg[a].start = MIN(avail_reg[a].end, reserved[r].end);
758                reserve_region(pptr_to_paddr_reg(reserved[r]));
759                r++;
760            } else {
761                assert(reserved[r].start < avail_reg[a].end);
762                /* take the first chunk of the available region and move
763                 * the start to the end of the reserved region */
764                region_t m = avail_reg[a];
765                m.end = reserved[r].start;
766                insert_region(m);
767                if (avail_reg[a].end > reserved[r].end) {
768                    avail_reg[a].start = reserved[r].end;
769                    reserve_region(pptr_to_paddr_reg(reserved[r]));
770                    r++;
771                } else {
772                    a++;
773                }
774            }
775        }
776    }
777
778    for (; r < n_reserved; r++) {
779        if (reserved[r].start < reserved[r].end) {
780            reserve_region(pptr_to_paddr_reg(reserved[r]));
781        }
782    }
783
784    /* no more reserved regions - add the rest */
785    for (; a < n_available; a++) {
786        if (avail_reg[a].start < avail_reg[a].end) {
787            insert_region(avail_reg[a]);
788        }
789    }
790
791    /* now try to fit the root server objects into a region */
792    word_t i = MAX_NUM_FREEMEM_REG - 1;
793    if (!is_reg_empty(ndks_boot.freemem[i])) {
794        printf("Insufficient MAX_NUM_FREEMEM_REG");
795        halt();
796    }
797    /* skip any empty regions */
798    for (; is_reg_empty(ndks_boot.freemem[i]) && i >= 0; i--);
799
800    /* try to grab the last available p region to create the root server objects
801     * from. If possible, retain any left over memory as an extra p region */
802    word_t size = calculate_rootserver_size(it_v_reg, extra_bi_size_bits);
803    word_t max = rootserver_max_size_bits(extra_bi_size_bits);
804    for (; i >= 0; i--) {
805        word_t next = i + 1;
806        pptr_t start = ROUND_DOWN(ndks_boot.freemem[i].end - size, max);
807        if (start >= ndks_boot.freemem[i].start) {
808            create_rootserver_objects(start, it_v_reg, extra_bi_size_bits);
809            if (i < MAX_NUM_FREEMEM_REG) {
810                ndks_boot.freemem[next].end = ndks_boot.freemem[i].end;
811                ndks_boot.freemem[next].start = start + size;
812            }
813            ndks_boot.freemem[i].end = start;
814            break;
815        } else if (i < MAX_NUM_FREEMEM_REG) {
816            ndks_boot.freemem[next] = ndks_boot.freemem[i];
817        }
818    }
819}
820