RTOS/seL4
1
0
Fork 0
forked from Imagelibrary/seL4
Code Pull Requests Activity

SELFOUR-114: remove bootinfo.h duplication

Browse Source
This commit is contained in:
Anna Lyons
2016-01-06 09:34:38 +11:00
parent bc457614f5
commit 289bf92bf0
14 changed files with 161 additions and 186 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
include/api/bootinfo_types.h Symbolic link
View File

@@ -0,0 +1 @@
../../libsel4/include/sel4/bootinfo_types.h

1
include/api/types.h
View File

@@ -23,7 +23,6 @@
/* cap_rights_t defined in api/types.bf */
typedef word_t prio_t;
typedef word_t dom_t;
enum domainConstants {
minDom = 0,

5
include/arch/arm/arch/types.h
View File

@@ -22,6 +22,7 @@ typedef word_t paddr_t;
typedef word_t pptr_t;
typedef word_t cptr_t;
typedef word_t node_id_t;
typedef word_t dom_t;
typedef uint8_t hw_asid_t;
@@ -34,5 +35,9 @@ enum hwASIDConstants {
typedef word_t seL4_Word;
typedef cptr_t seL4_CPtr;
typedef uint32_t seL4_Uint32;
typedef uint8_t seL4_Uint8;
typedef node_id_t seL4_NodeId;
typedef dom_t seL4_Domain;
typedef paddr_t seL4_PAddr;
#endif

6
include/arch/x86/arch/types.h
View File

@@ -24,10 +24,14 @@ typedef word_t cptr_t;
typedef word_t dev_id_t;
typedef word_t cpu_id_t;
typedef word_t node_id_t;
typedef word_t dom_t;
/* for libsel4 headers that the kernel shares */
typedef word_t seL4_Word;
typedef cptr_t seL4_CPtr;
typedef uint32_t seL4_Uint32;
typedef uint8_t seL4_Uint8;
typedef node_id_t seL4_NodeId;
typedef paddr_t seL4_PAddr;
typedef dom_t seL4_Domain;
#endif

59
include/bootinfo.h
View File

@@ -13,65 +13,14 @@
#include <config.h>
#include <types.h>
#include <api/bootinfo_types.h>
#define BI_PTR(r) ((bi_t*)(r))
#define BI_PTR(r) ((seL4_BootInfo*)(r))
#define BI_REF(p) ((word_t)(p))
/* bootinfo data structures (directly corresponding to abstract specification) */
#define BI_FRAME_SIZE_BITS PAGE_BITS
/* fixed cap positions in root CNode */
#define BI_CAP_NULL 0 /* null cap */
#define BI_CAP_IT_TCB 1 /* initial thread's TCB cap */
#define BI_CAP_IT_CNODE 2 /* initial thread's root CNode cap */
#define BI_CAP_IT_VSPACE 3 /* initial thread's vspace root cap */
#define BI_CAP_IRQ_CTRL 4 /* global IRQ controller cap */
#define BI_CAP_ASID_CTRL 5 /* global ASID controller cap */
#define BI_CAP_IT_ASID_POOL 6 /* initial thread's ASID pool cap */
#define BI_CAP_IO_PORT 7 /* global IO port cap (null cap if not supported) */
#define BI_CAP_IO_SPACE 8 /* global IO space cap (null cap if no IOMMU support) */
#define BI_CAP_BI_FRAME 9 /* bootinfo frame cap */
#define BI_CAP_IT_IPCBUF 10 /* initial thread's IPC buffer frame cap */
#define BI_CAP_DOM 11 /* domain cap */
#define BI_CAP_DYN_START 12 /* slot where dynamically allocated caps start */
/* type definitions */
typedef word_t slot_pos_t;
typedef struct slot_region {
slot_pos_t start;
slot_pos_t end;
} slot_region_t;
#define S_REG_EMPTY (slot_region_t){ .start = 0, .end = 0 }
typedef struct bi_dev_reg {
paddr_t base_paddr; /* base physical address of device region */
uint32_t frame_size_bits; /* size (2^n bytes) of a device-region frame */
slot_region_t frame_caps; /* device-region frame caps */
} bi_dev_reg_t;
typedef struct bi {
node_id_t node_id;
uint32_t num_nodes;
uint32_t num_iopt_levels; /* number of IOMMU PT levels (0 if no IOMMU support) */
vptr_t ipcbuf_vptr; /* vptr to initial thread's IPC buffer */
slot_region_t null_caps; /* null caps (empty slots) */
slot_region_t sh_frame_caps; /* shared-frame caps */
slot_region_t ui_frame_caps; /* userland-image frame caps */
slot_region_t ui_paging_caps; /* userland-image paging structure caps */
slot_region_t ut_obj_caps; /* untyped-object caps (UT caps) */
paddr_t ut_obj_paddr_list [CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* physical address of each UT cap */
uint8_t ut_obj_size_bits_list[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* size (2^n) bytes of each UT cap */
uint8_t it_cnode_size_bits; /* initial thread's root CNode size (2^n slots) */
uint32_t num_dev_regs; /* number of device regions */
bi_dev_reg_t dev_reg_list[CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS]; /* device regions */
dom_t it_domain; /* initial thread's domain ID */
} bi_t;
#define S_REG_EMPTY (seL4_SlotRegion){ .start = 0, .end = 0 }
/* adjust constants in config.h if this assert fails */
compile_assert(bi_size, sizeof(bi_t) <= BIT(BI_FRAME_SIZE_BITS))
compile_assert(bi_size, sizeof(seL4_BootInfo) <= BIT(BI_FRAME_SIZE_BITS))
#endif

8
include/kernel/boot.h
View File

@@ -32,9 +32,9 @@ typedef cte_t* slot_ptr_t;
typedef struct ndks_boot {
region_t freemem[MAX_NUM_FREEMEM_REG];
bi_t* bi_frame;
slot_pos_t slot_pos_cur;
slot_pos_t slot_pos_max;
seL4_BootInfo* bi_frame;
seL4_SlotPos slot_pos_cur;
seL4_SlotPos slot_pos_max;
} ndks_boot_t;
extern ndks_boot_t ndks_boot;
@@ -67,7 +67,7 @@ pptr_t allocate_bi_frame(node_id_t node_id, word_t num_nodes, vptr_t ipcbuf_vptr
void create_bi_frame_cap(cap_t root_cnode_cap, cap_t pd_cap, pptr_t pptr, vptr_t vptr);
typedef struct create_frames_of_region_ret {
slot_region_t region;
seL4_SlotRegion region;
bool_t success;
} create_frames_of_region_ret_t;

56
libsel4/include/sel4/bootinfo.h
View File

@@ -12,61 +12,7 @@
#define __LIBSEL4_BOOTINFO_H
#include <sel4/types.h>
/* caps with fixed slot potitions in the root CNode */
enum {
seL4_CapNull = 0, /* null cap */
seL4_CapInitThreadTCB = 1, /* initial thread's TCB cap */
seL4_CapInitThreadCNode = 2, /* initial thread's root CNode cap */
seL4_CapInitThreadVSpace = 3, /* initial thread's VSpace cap */
seL4_CapIRQControl = 4, /* global IRQ controller cap */
seL4_CapASIDControl = 5, /* global ASID controller cap */
seL4_CapInitThreadASIDPool = 6, /* initial thread's ASID pool cap */
seL4_CapIOPort = 7, /* global IO port cap (null cap if not supported) */
seL4_CapIOSpace = 8, /* global IO space cap (null cap if no IOMMU support) */
seL4_CapBootInfoFrame = 9, /* bootinfo frame cap */
seL4_CapInitThreadIPCBuffer = 10, /* initial thread's IPC buffer frame cap */
seL4_CapDomain = 11, /* global domain controller cap */
seL4_NumInitialCaps = 12
};
/* Legacy code will have assumptions on the vspace root being a Page Directory
* type, so for now we define one to the other */
#define seL4_CapInitThreadPD seL4_CapInitThreadVSpace
/* types */
typedef struct {
seL4_Word start; /* first CNode slot position OF region */
seL4_Word end; /* first CNode slot position AFTER region */
} seL4_SlotRegion;
typedef struct {
seL4_Word basePaddr; /* base physical address of device region */
seL4_Uint32 frameSizeBits; /* size (2^n bytes) of a device-region frame */
seL4_SlotRegion frames; /* device-region frame caps */
} seL4_DeviceRegion;
typedef struct {
seL4_Word nodeID; /* ID [0..numNodes-1] of the seL4 node (0 if uniprocessor) */
seL4_Uint32 numNodes; /* number of seL4 nodes (1 if uniprocessor) */
seL4_Uint32 numIOPTLevels; /* number of IOMMU PT levels (0 if no IOMMU support) */
seL4_IPCBuffer* ipcBuffer; /* pointer to initial thread's IPC buffer */
seL4_SlotRegion empty; /* empty slots (null caps) */
seL4_SlotRegion sharedFrames; /* shared-frame caps (shared between seL4 nodes) */
seL4_SlotRegion userImageFrames; /* userland-image frame caps */
seL4_SlotRegion userImagePaging; /* userland-image paging structure caps */
seL4_SlotRegion untyped; /* untyped-object caps (untyped caps) */
seL4_Word untypedPaddrList [CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* physical address of each untyped cap */
seL4_Uint8 untypedSizeBitsList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* size (2^n) bytes of each untyped cap */
seL4_Uint8 initThreadCNodeSizeBits; /* initial thread's root CNode size (2^n slots) */
seL4_Uint32 numDeviceRegions; /* number of device regions */
seL4_DeviceRegion deviceRegions[CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS]; /* device regions */
seL4_Uint32 initThreadDomain; /* Initial thread's domain ID */
} seL4_BootInfo;
/* function declarations */
#include <sel4/bootinfo_types.h>
void seL4_InitBootInfo(seL4_BootInfo* bi);
seL4_BootInfo* seL4_GetBootInfo(void);

69
libsel4/include/sel4/bootinfo_types.h Normal file
View File

@@ -0,0 +1,69 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_BOOTINFO_TYPES_H
#define __LIBSEL4_BOOTINFO_TYPES_H
/* caps with fixed slot potitions in the root CNode */
enum {
seL4_CapNull = 0, /* null cap */
seL4_CapInitThreadTCB = 1, /* initial thread's TCB cap */
seL4_CapInitThreadCNode = 2, /* initial thread's root CNode cap */
seL4_CapInitThreadVSpace = 3, /* initial thread's VSpace cap */
seL4_CapIRQControl = 4, /* global IRQ controller cap */
seL4_CapASIDControl = 5, /* global ASID controller cap */
seL4_CapInitThreadASIDPool = 6, /* initial thread's ASID pool cap */
seL4_CapIOPort = 7, /* global IO port cap (null cap if not supported) */
seL4_CapIOSpace = 8, /* global IO space cap (null cap if no IOMMU support) */
seL4_CapBootInfoFrame = 9, /* bootinfo frame cap */
seL4_CapInitThreadIPCBuffer = 10, /* initial thread's IPC buffer frame cap */
seL4_CapDomain = 11, /* global domain controller cap */
seL4_NumInitialCaps = 12
};
/* Legacy code will have assumptions on the vspace root being a Page Directory
* type, so for now we define one to the other */
#define seL4_CapInitThreadPD seL4_CapInitThreadVSpace
/* types */
typedef seL4_Word seL4_SlotPos;
typedef struct {
seL4_SlotPos start; /* first CNode slot position OF region */
seL4_SlotPos end; /* first CNode slot position AFTER region */
} seL4_SlotRegion;
typedef struct {
seL4_Word basePaddr; /* base physical address of device region */
seL4_Word frameSizeBits; /* size (2^n bytes) of a device-region frame */
seL4_SlotRegion frames; /* device-region frame caps */
} seL4_DeviceRegion;
typedef struct {
seL4_NodeId nodeID; /* ID [0..numNodes-1] of the seL4 node (0 if uniprocessor) */
seL4_Word numNodes; /* number of seL4 nodes (1 if uniprocessor) */
seL4_Word numIOPTLevels; /* number of IOMMU PT levels (0 if no IOMMU support) */
seL4_IPCBuffer* ipcBuffer; /* pointer to initial thread's IPC buffer */
seL4_SlotRegion empty; /* empty slots (null caps) */
seL4_SlotRegion sharedFrames; /* shared-frame caps (shared between seL4 nodes) */
seL4_SlotRegion userImageFrames; /* userland-image frame caps */
seL4_SlotRegion userImagePaging; /* userland-image paging structure caps */
seL4_SlotRegion untyped; /* untyped-object caps (untyped caps) */
seL4_PAddr untypedPaddrList [CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* physical address of each untyped cap */
seL4_Uint8 untypedSizeBitsList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* size (2^n) bytes of each untyped cap */
seL4_Uint8 initThreadCNodeSizeBits; /* initial thread's root CNode size (2^n slots) */
seL4_Word numDeviceRegions; /* number of device regions */
seL4_DeviceRegion deviceRegions[CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS]; /* device regions */
seL4_Domain initThreadDomain; /* Initial thread's domain ID */
} seL4_BootInfo;
#endif // __LIBSEL4_BOOTINFO_TYPES_H

3
libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/types.h
View File

@@ -15,6 +15,9 @@
typedef seL4_Uint32 seL4_Word;
typedef seL4_Word seL4_CPtr;
typedef seL4_Word seL4_NodeId;
typedef seL4_Word seL4_PAddr;
typedef seL4_Word seL4_Domain;
typedef struct seL4_UserContext_ {
/* frame registers */

30
src/arch/arm/32/kernel/vspace.c
View File

@@ -358,8 +358,8 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
cap_t pd_cap;
vptr_t pt_vptr;
pptr_t pt_pptr;
slot_pos_t slot_pos_before;
slot_pos_t slot_pos_after;
seL4_SlotPos slot_pos_before;
seL4_SlotPos slot_pos_after;
pptr_t pd_pptr;
/* create PD obj and cap */
@@ -378,7 +378,7 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
pd_pptr /* capPDBasePtr */
);
slot_pos_before = ndks_boot.slot_pos_cur;
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_VSPACE), pd_cap);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadVSpace), pd_cap);
/* create all PT objs and caps necessary to cover userland image */
@@ -398,7 +398,7 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
}
slot_pos_after = ndks_boot.slot_pos_cur;
ndks_boot.bi_frame->ui_paging_caps = (slot_region_t) {
ndks_boot.bi_frame->userImagePaging = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after
};
@@ -408,22 +408,22 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
BOOT_CODE bool_t
create_device_frames(cap_t root_cnode_cap)
{
slot_pos_t slot_pos_before;
slot_pos_t slot_pos_after;
seL4_SlotPos slot_pos_before;
seL4_SlotPos slot_pos_after;
vm_page_size_t frame_size;
region_t dev_reg;
bi_dev_reg_t bi_dev_reg;
seL4_DeviceRegion bi_dev_reg;
cap_t frame_cap;
word_t i;
pptr_t f;
ndks_boot.bi_frame->num_dev_regs = get_num_dev_p_regs();
if (ndks_boot.bi_frame->num_dev_regs > CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS) {
ndks_boot.bi_frame->numDeviceRegions = get_num_dev_p_regs();
if (ndks_boot.bi_frame->numDeviceRegions > CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS) {
printf("Kernel init: Too many device regions for boot info\n");
ndks_boot.bi_frame->num_dev_regs = CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS;
ndks_boot.bi_frame->numDeviceRegions = CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS;
}
for (i = 0; i < ndks_boot.bi_frame->num_dev_regs; i++) {
for (i = 0; i < ndks_boot.bi_frame->numDeviceRegions; i++) {
/* write the frame caps of this device region into the root CNode and update the bootinfo */
dev_reg = paddr_to_pptr_reg(get_dev_p_reg(i));
/* use 1M frames if possible, otherwise use 4K frames */
@@ -447,12 +447,12 @@ create_device_frames(cap_t root_cnode_cap)
slot_pos_after = ndks_boot.slot_pos_cur;
/* add device-region entry to bootinfo */
bi_dev_reg.base_paddr = pptr_to_paddr((void*)dev_reg.start);
bi_dev_reg.frame_size_bits = pageBitsForSize(frame_size);
bi_dev_reg.frame_caps = (slot_region_t) {
bi_dev_reg.basePaddr = pptr_to_paddr((void*)dev_reg.start);
bi_dev_reg.frameSizeBits = pageBitsForSize(frame_size);
bi_dev_reg.frames = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after
};
ndks_boot.bi_frame->dev_reg_list[i] = bi_dev_reg;
ndks_boot.bi_frame->deviceRegions[i] = bi_dev_reg;
}
return true;

7
src/arch/arm/kernel/boot.c
View File

@@ -133,10 +133,9 @@ init_irqs(cap_t root_cnode_cap)
setIRQState(IRQTimer, KERNEL_TIMER_IRQ);
/* provide the IRQ control cap */
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IRQ_CTRL), cap_irq_control_cap_new());
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapIRQControl), cap_irq_control_cap_new());
}
/* This and only this function initialises the CPU. It does NOT initialise any kernel state. */
BOOT_CODE static void
@@ -262,7 +261,7 @@ try_init_kernel(
if (!create_frames_ret.success) {
return false;
}
ndks_boot.bi_frame->ui_frame_caps = create_frames_ret.region;
ndks_boot.bi_frame->userImageFrames = create_frames_ret.region;
/* create/initialise the initial thread's ASID pool */
it_ap_cap = create_it_asid_pool(root_cnode_cap);
@@ -310,7 +309,7 @@ try_init_kernel(
}
/* no shared-frame caps (ARM has no multikernel support) */
ndks_boot.bi_frame->sh_frame_caps = S_REG_EMPTY;
ndks_boot.bi_frame->sharedFrames = S_REG_EMPTY;
/* finalise the bootinfo frame */
bi_finalise();

10
src/arch/x86/32/kernel/vspace.c
View File

@@ -439,8 +439,8 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
cap_t vspace_cap;
vptr_t vptr;
pptr_t pptr;
slot_pos_t slot_pos_before;
slot_pos_t slot_pos_after;
seL4_SlotPos slot_pos_before;
seL4_SlotPos slot_pos_after;
slot_pos_before = ndks_boot.slot_pos_cur;
if (PDPT_BITS == 0) {
@@ -457,7 +457,7 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
if (!provide_cap(root_cnode_cap, pd_cap)) {
return cap_null_cap_new();
}
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_VSPACE), pd_cap);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadVSpace), pd_cap);
vspace_cap = pd_cap;
} else {
cap_t pdpt_cap;
@@ -505,7 +505,7 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
}
/* now that PDs exist we can copy the global mappings */
copyGlobalMappings((vspace_root_t*)pdpt_pptr);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_VSPACE), pdpt_cap);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadVSpace), pdpt_cap);
vspace_cap = pdpt_cap;
}
@@ -527,7 +527,7 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
}
slot_pos_after = ndks_boot.slot_pos_cur;
ndks_boot.bi_frame->ui_paging_caps = (slot_region_t) {
ndks_boot.bi_frame->userImagePaging = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after
};

28
src/arch/x86/kernel/boot.c
View File

@@ -59,7 +59,7 @@ init_irqs(cap_t root_cnode_cap)
}
Arch_irqStateInit();
/* provide the IRQ control cap */
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IRQ_CTRL), cap_irq_control_cap_new());
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapIRQControl), cap_irq_control_cap_new());
}
BOOT_CODE static bool_t
@@ -68,11 +68,11 @@ create_device_frames(
dev_p_regs_t* dev_p_regs
)
{
slot_pos_t slot_pos_before;
slot_pos_t slot_pos_after;
seL4_SlotPos slot_pos_before;
seL4_SlotPos slot_pos_after;
vm_page_size_t frame_size;
region_t dev_reg;
bi_dev_reg_t bi_dev_reg;
seL4_DeviceRegion bi_dev_reg;
cap_t frame_cap;
uint32_t i;
pptr_t f;
@@ -101,15 +101,15 @@ create_device_frames(
slot_pos_after = ndks_boot.slot_pos_cur;
/* add device-region entry to bootinfo */
bi_dev_reg.base_paddr = pptr_to_paddr((void*)dev_reg.start);
bi_dev_reg.frame_size_bits = pageBitsForSize(frame_size);
bi_dev_reg.frame_caps = (slot_region_t) {
bi_dev_reg.basePaddr = pptr_to_paddr((void*)dev_reg.start);
bi_dev_reg.frameSizeBits = pageBitsForSize(frame_size);
bi_dev_reg.frames = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after
};
ndks_boot.bi_frame->dev_reg_list[i] = bi_dev_reg;
ndks_boot.bi_frame->deviceRegions[i] = bi_dev_reg;
}
ndks_boot.bi_frame->num_dev_regs = dev_p_regs->count;
ndks_boot.bi_frame->numDeviceRegions = dev_p_regs->count;
return true;
}
@@ -219,7 +219,7 @@ init_sys_state(
/* create the IO port cap */
write_slot(
SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IO_PORT),
SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapIOPort),
cap_io_port_cap_new(
0, /* first port */
NUM_IO_PORTS - 1 /* last port */
@@ -276,7 +276,7 @@ init_sys_state(
if (!create_frames_ret.success) {
return false;
}
ndks_boot.bi_frame->ui_frame_caps = create_frames_ret.region;
ndks_boot.bi_frame->userImageFrames = create_frames_ret.region;
/* create the initial thread's ASID pool */
it_ap_cap = create_it_asid_pool(root_cnode_cap);
@@ -318,12 +318,12 @@ init_sys_state(
}
/* write number of IOMMU PT levels into bootinfo */
ndks_boot.bi_frame->num_iopt_levels = x86KSnumIOPTLevels;
ndks_boot.bi_frame->numIOPTLevels = x86KSnumIOPTLevels;
/* write IOSpace master cap */
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IO_SPACE), master_iospace_cap());
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapIOSpace), master_iospace_cap());
} else {
ndks_boot.bi_frame->num_iopt_levels = -1;
ndks_boot.bi_frame->numIOPTLevels = -1;
}
/* convert the remaining free memory into UT objects and provide the caps */

64
src/kernel/boot.c
View File

@@ -131,7 +131,7 @@ write_slot(slot_ptr_t slot_ptr, cap_t cap)
*/
compile_assert(root_cnode_size_valid,
CONFIG_ROOT_CNODE_SIZE_BITS < 32 - seL4_SlotBits &&
(1U << CONFIG_ROOT_CNODE_SIZE_BITS) >= BI_CAP_DYN_START)
(1U << CONFIG_ROOT_CNODE_SIZE_BITS) >= seL4_NumInitialCaps)
BOOT_CODE cap_t
create_root_cnode(void)
@@ -158,7 +158,7 @@ create_root_cnode(void)
);
/* write the root CNode cap into the root CNode */
write_slot(SLOT_PTR(pptr, BI_CAP_IT_CNODE), cap);
write_slot(SLOT_PTR(pptr, seL4_CapInitThreadCNode), cap);
return cap;
}
@@ -200,7 +200,7 @@ create_domain_cap(cap_t root_cnode_cap)
}
cap = cap_domain_cap_new();
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_DOM), cap);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapDomain), cap);
}
@@ -220,7 +220,7 @@ create_ipcbuf_frame(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 = create_mapped_it_frame_cap(pd_cap, pptr, vptr, IT_ASID, false, false);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_IPCBUF), cap);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadIPCBuffer), cap);
return cap;
}
@@ -237,7 +237,7 @@ create_bi_frame_cap(
/* create a cap of it and write it into the root CNode */
cap = create_mapped_it_frame_cap(pd_cap, pptr, vptr, IT_ASID, false, false);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_BI_FRAME), cap);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapBootInfoFrame), cap);
}
BOOT_CODE pptr_t
@@ -259,14 +259,14 @@ allocate_bi_frame(
/* initialise bootinfo-related global state */
ndks_boot.bi_frame = BI_PTR(pptr);
ndks_boot.slot_pos_cur = BI_CAP_DYN_START;
ndks_boot.slot_pos_cur = seL4_NumInitialCaps;
BI_PTR(pptr)->node_id = node_id;
BI_PTR(pptr)->num_nodes = num_nodes;
BI_PTR(pptr)->num_iopt_levels = 0;
BI_PTR(pptr)->ipcbuf_vptr = ipcbuf_vptr;
BI_PTR(pptr)->it_cnode_size_bits = CONFIG_ROOT_CNODE_SIZE_BITS;
BI_PTR(pptr)->it_domain = ksDomSchedule[ksDomScheduleIdx].domain;
BI_PTR(pptr)->nodeID = node_id;
BI_PTR(pptr)->numNodes = num_nodes;
BI_PTR(pptr)->numIOPTLevels = 0;
BI_PTR(pptr)->ipcBuffer = (seL4_IPCBuffer *) ipcbuf_vptr;
BI_PTR(pptr)->initThreadCNodeSizeBits = CONFIG_ROOT_CNODE_SIZE_BITS;
BI_PTR(pptr)->initThreadDomain = ksDomSchedule[ksDomScheduleIdx].domain;
return pptr;
}
@@ -294,8 +294,8 @@ create_frames_of_region(
{
pptr_t f;
cap_t frame_cap;
slot_pos_t slot_pos_before;
slot_pos_t slot_pos_after;
seL4_SlotPos slot_pos_before;
seL4_SlotPos slot_pos_after;
slot_pos_before = ndks_boot.slot_pos_cur;
@@ -314,7 +314,7 @@ create_frames_of_region(
slot_pos_after = ndks_boot.slot_pos_cur;
return (create_frames_of_region_ret_t) {
(slot_region_t) { slot_pos_before, slot_pos_after }, true
(seL4_SlotRegion) { slot_pos_before, slot_pos_after }, true
};
}
@@ -332,11 +332,11 @@ create_it_asid_pool(cap_t root_cnode_cap)
}
memzero(ASID_POOL_PTR(ap_pptr), 1 << seL4_ASIDPoolBits);
ap_cap = cap_asid_pool_cap_new(IT_ASID >> asidLowBits, ap_pptr);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_ASID_POOL), ap_cap);
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), BI_CAP_ASID_CTRL),
SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapASIDControl),
cap_asid_control_cap_new()
);
@@ -385,7 +385,7 @@ create_initial_thread(
Arch_initContext(&tcb->tcbArch.tcbContext);
/* derive a copy of the IPC buffer cap for inserting */
dc_ret = deriveCap(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_IPCBUF), ipcbuf_cap);
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 false;
@@ -394,17 +394,17 @@ create_initial_thread(
/* initialise TCB (corresponds directly to abstract specification) */
cteInsert(
root_cnode_cap,
SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_CNODE),
SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadCNode),
SLOT_PTR(pptr, tcbCTable)
);
cteInsert(
it_pd_cap,
SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_VSPACE),
SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadVSpace),
SLOT_PTR(pptr, tcbVTable)
);
cteInsert(
dc_ret.cap,
SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_IPCBUF),
SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadIPCBuffer),
SLOT_PTR(pptr, tcbBuffer)
);
tcb->tcbIPCBuffer = ipcbuf_vptr;
@@ -423,7 +423,7 @@ create_initial_thread(
/* create initial thread's TCB cap */
cap = cap_thread_cap_new(TCB_REF(tcb));
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_TCB), cap);
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadTCB), cap);
#ifdef DEBUG
setThreadName(tcb, "rootserver");
@@ -437,14 +437,14 @@ provide_untyped_cap(
cap_t root_cnode_cap,
pptr_t pptr,
word_t size_bits,
slot_pos_t first_untyped_slot
seL4_SlotPos first_untyped_slot
)
{
bool_t ret;
word_t i = ndks_boot.slot_pos_cur - first_untyped_slot;
if (i < CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS) {
ndks_boot.bi_frame->ut_obj_paddr_list[i] = pptr_to_paddr((void*)pptr);
ndks_boot.bi_frame->ut_obj_size_bits_list[i] = size_bits;
ndks_boot.bi_frame->untypedPaddrList[i] = pptr_to_paddr((void*)pptr);
ndks_boot.bi_frame->untypedSizeBitsList[i] = size_bits;
ret = provide_cap(root_cnode_cap, cap_untyped_cap_new(0, size_bits, pptr));
} else {
printf("Kernel init: Too many untyped regions for boot info\n");
@@ -465,7 +465,7 @@ BOOT_CODE static bool_t
create_untypeds_for_region(
cap_t root_cnode_cap,
region_t reg,
slot_pos_t first_untyped_slot
seL4_SlotPos first_untyped_slot
)
{
word_t align_bits;
@@ -495,8 +495,8 @@ create_untypeds_for_region(
BOOT_CODE bool_t
create_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg)
{
slot_pos_t slot_pos_before;
slot_pos_t slot_pos_after;
seL4_SlotPos slot_pos_before;
seL4_SlotPos slot_pos_after;
word_t i;
region_t reg;
@@ -517,7 +517,7 @@ create_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg)
}
slot_pos_after = ndks_boot.slot_pos_cur;
ndks_boot.bi_frame->ut_obj_caps = (slot_region_t) {
ndks_boot.bi_frame->untyped = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after
};
return true;
@@ -526,9 +526,9 @@ create_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg)
BOOT_CODE void
bi_finalise(void)
{
slot_pos_t slot_pos_start = ndks_boot.slot_pos_cur;
slot_pos_t slot_pos_end = ndks_boot.slot_pos_max;
ndks_boot.bi_frame->null_caps = (slot_region_t) {
seL4_SlotPos slot_pos_start = ndks_boot.slot_pos_cur;
seL4_SlotPos slot_pos_end = ndks_boot.slot_pos_max;
ndks_boot.bi_frame->empty = (seL4_SlotRegion) {
slot_pos_start, slot_pos_end
};
}