ExternalVendorCode/genode
1
0
Fork 0
mirror of https://github.com/genodelabs/genode.git synced 2024-12-18 21:27:56 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

sel4: update to 12.1.0 release

Browse Source 
Fixes #4910
This commit is contained in:
Alexander Boettcher 2023-04-11 18:42:54 +02:00 committed by Christian Helmuth
parent 7351aa1670
commit d92bd3afee
45 changed files with 388 additions and 603 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
repos/base-sel4/include/sel4/functions_aarch32.h Normal file
View File

@ -0,0 +1,24 @@
/*
* \brief Implementation for seL4_GetIPCBuffer on aarch32
* \author Alexander Boettcher
* \date 2023-05-23
*/
/*
* Copyright (C) 2023 Genode Labs GmbH
*
* This file is part of the Genode OS framework, which is distributed
* under the terms of the GNU Affero General Public License version 3.
*/
#ifndef _INCLUDE__SEL4__FUNCTIONS_AARCH32_H_
#define _INCLUDE__SEL4__FUNCTIONS_AARCH32_H_
LIBSEL4_INLINE_FUNC seL4_IPCBuffer *seL4_GetIPCBuffer(void)
{
seL4_IPCBuffer ** ptr = nullptr;
asm volatile ("mrc p15, 0, %0, c13, c0, 2" : "=r"(ptr));
return *ptr;
}
#endif /* _INCLUDE__SEL4__FUNCTIONS_AARCH32_H_ */

24
repos/base-sel4/include/sel4/functions_x86_64.h Normal file
View File

@ -0,0 +1,24 @@
/*
* \brief Implementation for seL4_GetIPCBuffer on x86_64
* \author Alexander Boettcher
* \date 2023-05-23
*/
/*
* Copyright (C) 2023 Genode Labs GmbH
*
* This file is part of the Genode OS framework, which is distributed
* under the terms of the GNU Affero General Public License version 3.
*/
#ifndef _INCLUDE__SEL4__FUNCTIONS_X86_64_H_
#define _INCLUDE__SEL4__FUNCTIONS_X86_64_H_
LIBSEL4_INLINE_FUNC seL4_IPCBuffer *seL4_GetIPCBuffer(void)
{
seL4_IPCBuffer * ptr = nullptr;
asm volatile ("movq %%fs:0, %0" : "=r" (ptr) : :);
return ptr;
}
#endif /* _INCLUDE__SEL4__FUNCTIONS_X86_64_H_ */

32
repos/base-sel4/lib/mk/spec/arm/kernel-sel4.inc
View File

@ -18,14 +18,36 @@ else
SEL4_CCACHE=
endif
elfloader/elfloader.o:
configured_kernel:
$(VERBOSE) cmake -DCROSS_COMPILER_PREFIX=$(CROSS_DEV_PREFIX) \
-DCMAKE_TOOLCHAIN_FILE=$(SEL4_DIR)/gcc.cmake \
-DKernelARMPlatform=sabre \
-G Ninja \
-C $(SEL4_DIR)/configs/ARM_verified.cmake \
$(SEL4_DIR) \
&& echo -e "\n#define CONFIG_PRINTING 1" >>gen_config/kernel/gen_config.h \
&& echo -e "#define CONFIG_DEBUG_BUILD 1" >>gen_config/kernel/gen_config.h \
&& echo -e "#define CONFIG_ENABLE_BENCHMARKS 1" >>gen_config/kernel/gen_config.h \
&& echo -e "#define CONFIG_BENCHMARK_TRACK_UTILISATION 1" >>gen_config/kernel/gen_config.h \
&& echo -e "#define CONFIG_SET_TLS_BASE_SELF 1" >>gen_config/kernel/gen_config.h \
&& echo -e "#define CONFIG_HAVE_FPU 1" >>gen_config/kernel/gen_config.h \
&& echo -e "#define CONFIG_AARCH32_FPU_ENABLE_CONTEXT_SWITCH 1" >>gen_config/kernel/gen_config.h \
&& echo -e "#define CONFIG_FPU_MAX_RESTORES_SINCE_SWITCH 64" >>gen_config/kernel/gen_config.h \
\
&& sed -e "s/CONFIG_NUM_DOMAINS 16/CONFIG_NUM_DOMAINS 1/" \
-e "s/CONFIG_ROOT_CNODE_SIZE_BITS 12/CONFIG_ROOT_CNODE_SIZE_BITS 15/" \
gen_config/kernel/gen_config.h >gen_config/kernel/gen_config.tmp \
&& mv gen_config/kernel/gen_config.tmp gen_config/kernel/gen_config.h \
&& touch configured_kernel
elfloader/elfloader.o: configured_kernel
$(VERBOSE)cp -r $(TOOLS_DIR)/elfloader-tool $(LIB_CACHE_DIR)/$(LIB)/elfloader
$(VERBOSE)mkdir -p $(LIB_CACHE_DIR)/$(LIB)/elfloader/tools/kbuild
$(VERBOSE)mkdir -p $(LIB_CACHE_DIR)/$(LIB)/elfloader/include/generated
$(VERBOSE)ln -s $(TOOLS_DIR)/common-tool/common.mk $(LIB_CACHE_DIR)/$(LIB)/elfloader/
$(VERBOSE)ln -s $(TOOLS_DIR)/common-tool/files_to_obj.sh $(LIB_CACHE_DIR)/$(LIB)/elfloader/
$(VERBOSE)ln -s $(TOOLS_DIR)/kbuild-tool/Kbuild.include $(LIB_CACHE_DIR)/$(LIB)/elfloader/tools/kbuild/
$(VERBOSE)ln -s $(SEL4_DIR)/configs/$(PLAT)/$(BOARD)/autoconf.h $(LIB_CACHE_DIR)/$(LIB)/elfloader/include/generated/
$(VERBOSE)ln -s $(LIB_CACHE_DIR)/$(LIB)/gen_config/kernel/gen_config.h $(LIB_CACHE_DIR)/$(LIB)/elfloader/include/generated/autoconf.h
$(VERBOSE)$(MAKE) -C $(LIB_CACHE_DIR)/$(LIB)/elfloader \
TOOLPREFIX=$(CROSS_DEV_PREFIX) \
ARCH=arm PLAT=$(PLAT) ARMV=armv7-a __ARM_32__="y" \
@ -35,7 +57,5 @@ elfloader/elfloader.o:
srctree=.
build_kernel: elfloader/elfloader.o
$(VERBOSE)$(MAKE) \
TOOLPREFIX=$(CROSS_DEV_PREFIX) \
BOARD=$(BOARD) ARCH=arm PLAT=$(PLAT) CPU=$(CPU) ARMV=armv7-a DEBUG=1 \
SOURCE_ROOT=$(SEL4_DIR) -f$(SEL4_DIR)/Makefile
$(VERBOSE) ninja kernel.elf && \
$(CUSTOM_STRIP) -o kernel.elf.strip kernel.elf

4
repos/base-sel4/lib/mk/spec/arm/syscall-sel4-imx6q_sabrelite.mk
View File

@ -1,8 +1,10 @@
PLAT := imx6
ARCH := arm
BOARD := imx6q_sabrelite
SEL4_ARCH := aarch32
PLAT_BOARD := /imx6q_sabrelite
SEL4_WORDBITS := 32
LIBS += kernel-sel4-imx6q_sabrelite
include $(REP_DIR)/lib/mk/syscall-sel4.inc

39
repos/base-sel4/lib/mk/spec/x86_64/kernel-sel4-pc.mk
View File

@ -11,9 +11,38 @@ else
all:
endif
build_kernel:
$(VERBOSE)$(MAKE) \
TOOLPREFIX=$(CROSS_DEV_PREFIX) \
BOARD=x86_64 ARCH=x86 SEL4_ARCH=x86_64 PLAT=pc99 DEBUG=1 \
SOURCE_ROOT=$(SEL4_DIR) -f$(SEL4_DIR)/Makefile
configured_kernel:
$(VERBOSE) cmake -DCROSS_COMPILER_PREFIX=$(CROSS_DEV_PREFIX) \
-DCMAKE_TOOLCHAIN_FILE=$(SEL4_DIR)/gcc.cmake \
-G Ninja \
-C $(SEL4_DIR)/configs/X64_verified.cmake \
$(SEL4_DIR) \
\
&& echo -e "\n#define CONFIG_PRINTING 1" >>gen_config/kernel/gen_config.h \
&& echo -e "#define CONFIG_DEBUG_BUILD 1" >>gen_config/kernel/gen_config.h \
&& echo -e "#define CONFIG_VTX 1" >>gen_config/kernel/gen_config.h \
&& echo -e "#define CONFIG_ENABLE_BENCHMARKS 1" >>gen_config/kernel/gen_config.h \
&& echo -e "#define CONFIG_BENCHMARK_TRACK_UTILISATION 1" >>gen_config/kernel/gen_config.h \
&& echo -e "#define CONFIG_ARCH_X86_GENERIC 1" >>gen_config/kernel/gen_config.h \
&& echo -e "#define CONFIG_FXSAVE 1" >>gen_config/kernel/gen_config.h \
&& echo -e "#define CONFIG_SET_TLS_BASE_SELF 1" >>gen_config/kernel/gen_config.h \
\
&& sed -e "s/CONFIG_MAX_NUM_NODES 1/CONFIG_MAX_NUM_NODES 16/" \
-e "s/CONFIG_MAX_VPIDS 0/CONFIG_MAX_VPIDS 64/" \
-e "s/CONFIG_NUM_DOMAINS 16/CONFIG_NUM_DOMAINS 1/" \
-e "s/CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 50/CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 160/" \
-e "s/CONFIG_FSGSBASE_INST 1/CONFIG_FSGSBASE_MSR 1/" \
-e "s/CONFIG_KERNEL_FSGS_BASE inst/CONFIG_KERNEL_FSGS_BASE msr/" \
-e "/CONFIG_HUGE_PAGE/d" \
-e "/CONFIG_SUPPORT_PCID/d" \
-e "/CONFIG_XSAVE 1/d" \
-e "/CONFIG_XSAVE_XSAVEOPT 1/d" \
-e "/CONFIG_ARCH_X86_NEHALEM 1/d" \
-e "/CONFIG_KERNEL_X86_MICRO_ARCH nehalem/d" \
gen_config/kernel/gen_config.h >gen_config/kernel/gen_config.tmp \
&& mv gen_config/kernel/gen_config.tmp gen_config/kernel/gen_config.h \
&& touch configured_kernel
build_kernel: configured_kernel
$(VERBOSE) ninja kernel.elf && \
$(CUSTOM_STRIP) -o kernel.elf.strip kernel.elf

4
repos/base-sel4/lib/mk/spec/x86_64/syscall-sel4-pc.mk
View File

@ -1,11 +1,13 @@
PLAT := pc99
ARCH := x86
BOARD := pc
SEL4_ARCH := x86_64
PLAT_BOARD := /$(SEL4_ARCH)
SEL4_WORDBITS := 64
ARCH_INCLUDES := exIPC.h vmenter.h
SEL4_ARCH_INCLUDES := syscalls_syscall.h
LIBS += kernel-sel4-pc
include $(REP_DIR)/lib/mk/syscall-sel4.inc

43
repos/base-sel4/lib/mk/syscall-sel4.inc
View File

@ -10,7 +10,6 @@
# port, if missing, is added to the missing-ports list of this stage.
#
LIBSEL4_DIR := $(call select_from_ports,sel4)/src/kernel/sel4/libsel4
LIBSEL4_AUTO:= $(call select_from_ports,sel4)/src/kernel/sel4/configs/$(PLAT)$(PLAT_BOARD)
#
# Execute the rules in this file only at the second build stage when we know
@ -29,14 +28,15 @@ SEL4_ARCH_INCLUDES += simple_types.h types.h constants.h objecttype.h \
functions.h syscalls.h invocation.h deprecated.h \
types_gen.h faults.h
ARCH_INCLUDES += objecttype.h types.h constants.h functions.h deprecated.h \
ARCH_INCLUDES += objecttype.h types.h constants.h deprecated.h \
syscalls.h invocation.h simple_types.h
INCLUDES := objecttype.h types.h bootinfo.h bootinfo_types.h errors.h \
constants.h messages.h sel4.h macros.h simple_types.h \
constants.h sel4.h macros.h simple_types.h \
syscall.h invocation.h shared_types_gen.h debug_assert.h \
shared_types.h sel4.h deprecated.h autoconf.h syscalls.h faults.h \
benchmark_utilisation_types.h
shared_types.h deprecated.h autoconf.h syscalls.h faults.h \
benchmark_utilisation_types.h \
syscalls_master.h virtual_client.h
PLAT_API_INCLUDES := constants.h
@ -49,6 +49,29 @@ INCLUDE_SYMLINKS += include/interfaces/sel4_client.h
all: $(INCLUDE_SYMLINKS)
#
# IPCBuffer pointer are not set up by kernel anymore, instead user land has
# to care about tracking the IPCBuffer, details are in the RFC
#
# https://sel4.atlassian.net/browse/RFC-3
#
# The usage of the __thread variable in the original include/sel4/functions.h
# would require our emutls emulation to work in core/roottask at an very
# early stage, which we don't support currently.
#
# As workaround, we setup the tls pointer per architecture such, that it
# points to the IPCBuffer pointer per thread, which is implemented in
# repos/base-sel4/include/sel4/functions_$(SEL4_ARCH).h
#
include/sel4/sel4_arch/functions.h: $(LIBSEL4_DIR)/include/sel4/functions.h
$(VERBOSE)mkdir -p $(dir $@) && \
sed -e "s|extern __thread seL4_IPCBuffer|//extern __thread seL4_IPCBuffer|" \
-e "s|#include <sel4/syscalls.h>|#include <sel4/syscalls.h>\n#include <sel4/functions_$(SEL4_ARCH).h>\n|" \
-e "/LIBSEL4_INLINE_FUNC void seL4_SetIPCBuffer(seL4_IPCBuffer \*ipc_buffer)/,+4d" \
-e "/LIBSEL4_INLINE_FUNC seL4_IPCBuffer \*seL4_GetIPCBuffer/,+3d" \
$< >include/sel4/functions.h && \
touch $@
#
# Plain symlinks to existing headers
#
@ -60,9 +83,11 @@ include/sel4/arch/%.h: $(LIBSEL4_DIR)/arch_include/$(ARCH)/sel4/arch/%.h
$(VERBOSE)mkdir -p $(dir $@)
$(VERBOSE)ln -sf $< $@
include/sel4/autoconf.h: $(LIBSEL4_AUTO)/autoconf.h
include/sel4/autoconf.h: $(LIB_CACHE_DIR)/kernel-sel4-$(BOARD)/autoconf/autoconf.h
$(VERBOSE)mkdir -p $(dir $@)
$(VERBOSE)ln -sf $< $@
$(VERBOSE)mkdir include/sel4/kernel -p
$(VERBOSE)ln -sf $(LIB_CACHE_DIR)/kernel-sel4-$(BOARD)/gen_config/kernel/gen_config.h include/sel4/kernel/gen_config.h
include/sel4/%.h: $(LIBSEL4_DIR)/include/sel4/%.h
$(VERBOSE)mkdir -p $(dir $@)
@ -79,17 +104,17 @@ include/sel4/mode/types.h: $(LIBSEL4_DIR)/mode_include/$(SEL4_WORDBITS)/sel4/mod
#
# Generated headers
#
include/sel4/%.pbf: $(LIBSEL4_DIR)/include/sel4/%.bf include/sel4/autoconf.h
include/sel4/mode_include/$(SEL4_WORDBITS)/sel4/shared_types.pbf: $(LIBSEL4_DIR)/mode_include/$(SEL4_WORDBITS)/sel4/shared_types.bf include/sel4/autoconf.h
$(MSG_CONVERT)$(notdir $@)
$(VERBOSE)mkdir -p $(dir $@)
$(VERBOSE)$(CPP) -P $< >$@
$(VERBOSE)$(CPP) -Iinclude/sel4 -P $< >$@
include/sel4/sel4_arch/types.pbf: $(LIBSEL4_DIR)/sel4_arch_include/$(SEL4_ARCH)/sel4/sel4_arch/types.bf include/sel4/autoconf.h
$(MSG_CONVERT)$(notdir $@)
$(VERBOSE)mkdir -p $(dir $@)
$(VERBOSE)$(CPP) -Iinclude/sel4 -I$(LIBSEL4_DIR)/arch_include/$(ARCH) -P $< >$@
include/sel4/shared_types_gen.h: include/sel4/shared_types_$(SEL4_WORDBITS).pbf
include/sel4/shared_types_gen.h: include/sel4/mode_include/$(SEL4_WORDBITS)/sel4/shared_types.pbf
$(MSG_CONVERT)$(notdir $@)
$(VERBOSE)mkdir -p $(dir $@)
$(VERBOSE)python -B $(LIBSEL4_DIR)/tools/bitfield_gen.py \

50
repos/base-sel4/patches/address_of_packed_member.patch
View File

@ -1,50 +0,0 @@
From 3e83f89990e356b02b227cd883d32ccafa283127 Mon Sep 17 00:00:00 2001
From: Simon Shields <simon.shields@data61.csiro.au>
Date: Tue, 17 Sep 2019 11:54:22 +1000
Subject: [PATCH] x86: avoid -Waddress-of-packed-member
It's safe to take the address of this member, since it's the
first thing in a cacheline-aligned struct.
---
include/arch/x86/arch/32/mode/stack.h | 7 ++++++-
src/arch/x86/kernel/vspace.c | 9 +++++++--
2 files changed, 13 insertions(+), 3 deletions(-)
diff --git a/include/arch/x86/arch/32/mode/stack.h b/include/arch/x86/arch/32/mode/stack.h
index 93304b96fa..e8e7f1c254 100644
--- src/kernel/sel4/include/arch/x86/arch/32/mode/stack.h
+++ src/kernel/sel4/include/arch/x86/arch/32/mode/stack.h
@@ -45,7 +45,12 @@ static inline void setKernelEntryStackPointer(tcb_t *target_thread)
/* The first item to be pushed onto the stack should always be SS */
register_context_top = (word_t)&target_thread->tcbArch.tcbContext.registers[SS + 1];
- tss_ptr_set_esp0(&x86KSGlobalState[CURRENT_CPU_INDEX()].x86KStss.tss, register_context_top);
+ /*
+ * Work around -Waddress-of-packed-member. TSS is the first thing
+ * in the struct and so it's safe to take its address.
+ */
+ void *tss = &x86KSGlobalState[CURRENT_CPU_INDEX()].x86KStss.tss;
+ tss_ptr_set_esp0(tss, register_context_top);
if (config_set(CONFIG_HARDWARE_DEBUG_API)) {
x86_wrmsr(IA32_SYSENTER_ESP_MSR, register_context_top);
diff --git a/src/arch/x86/kernel/vspace.c b/src/arch/x86/kernel/vspace.c
index 0ff6d30fff..be9d5f6266 100644
--- src/kernel/sel4/src/arch/x86/kernel/vspace.c
+++ src/kernel/sel4/src/arch/x86/kernel/vspace.c
@@ -493,8 +493,13 @@ BOOT_CODE bool_t init_vm_state(void)
SMP_COND_STATEMENT(return false);
}
- init_tss(&x86KSGlobalState[CURRENT_CPU_INDEX()].x86KStss.tss);
- init_gdt(x86KSGlobalState[CURRENT_CPU_INDEX()].x86KSgdt, &x86KSGlobalState[CURRENT_CPU_INDEX()].x86KStss.tss);
+ /*
+ * Work around -Waddress-of-packed-member. TSS is the first thing
+ * in the struct and so it's safe to take its address.
+ */
+ void *tss_ptr = &x86KSGlobalState[CURRENT_CPU_INDEX()].x86KStss.tss;
+ init_tss(tss_ptr);
+ init_gdt(x86KSGlobalState[CURRENT_CPU_INDEX()].x86KSgdt, tss_ptr);
init_idt(x86KSGlobalState[CURRENT_CPU_INDEX()].x86KSidt);
return true;
}

15
repos/base-sel4/patches/arm_no_dtb.patch Normal file
View File

@ -0,0 +1,15 @@
--- src/kernel/sel4/src/arch/arm/kernel/boot.c
+++ src/kernel/sel4/src/arch/arm/kernel/boot.c
@@ -582,6 +582,12 @@
dtb_end_p = dtb_addr_p + dtb_size;
}
+ /*
+ * no DTB support on Genode/seL4 - avoids assertion in
+ * src/kernel/boot.c: assert(r->start >= reserved[i - 1].end);
+ */
+ dtb_addr_p = dtb_end_p = 0;
+
#ifdef ENABLE_SMP_SUPPORT
/* we assume there exists a cpu with id 0 and will use it for bootstrapping */
if (getCurrentCPUIndex() == 0) {

48
repos/base-sel4/patches/autoconf_32.patch
View File

@ -1,48 +0,0 @@
--- src/kernel/sel4/configs/pc99/autoconf.h
+++ src/kernel/sel4/configs/pc99/autoconf.h
@@ -51,13 +51,13 @@
#define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 167
#define CONFIG_FPU_MAX_RESTORES_SINCE_SWITCH 64
#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0
-#define CONFIG_MAX_NUM_NODES 1
+#define CONFIG_MAX_NUM_NODES 16
#define CONFIG_CROSS_COMPILER_PREFIX ""
#define CONFIG_LIB_SEL4_INLINE_INVOCATIONS 1
#define CONFIG_LIB_SEL4_MUSLC_SYS 1
#define CONFIG_HAVE_LIB_SEL4_TEST 1
#define CONFIG_LIB_MUSL_C 1
-#define CONFIG_ARCH_X86_NEHALEM 1
+#define CONFIG_ARCH_X86_GENERIC 1
#define CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION 100
#define CONFIG_USER_CFLAGS ""
#define CONFIG_HAVE_LIB_SEL4_DEBUG 1
@@ -75,13 +75,13 @@
#define CONFIG_HAVE_LIB_SEL4_SIMPLE 1
#define CONFIG_HAVE_LIB_ELF 1
#define CONFIG_HAVE_LIB_PLATSUPPORT 1
-#define CONFIG_NUM_DOMAINS 16
+#define CONFIG_NUM_DOMAINS 1
#define CONFIG_ARCH_IA32 1
#define CONFIG_HAVE_LIB_UTILS 1
#define CONFIG_USER_OPTIMISATION_O2 1
#define CONFIG_LIB_CPIO 1
#define CONFIG_RETYPE_FAN_OUT_LIMIT 256
-#define CONFIG_ROOT_CNODE_SIZE_BITS 16
+#define CONFIG_ROOT_CNODE_SIZE_BITS 18
#define CONFIG_NUM_PRIORITIES 256
#define CONFIG_TESTPRINTER_REGEX ".*"
#define CONFIG_APP_SEL4TEST 1
@@ -96,6 +96,13 @@
#define CONFIG_CACHE_LN_SZ 64
#define CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES 1048576
#define CONFIG_BUILDSYS_USE_CCACHE 1
+#define CONFIG_MULTIBOOT1_HEADER
+#define CONFIG_MULTIBOOT2_HEADER
+#define CONFIG_PRINTING 1
+#define CONFIG_ENABLE_BENCHMARKS 1
+#define CONFIG_BENCHMARK_TRACK_UTILISATION 1
+#define CONFIG_VTX 1
+#define CONFIG_MAX_VPIDS 64
#else
#define AUTOCONF_INCLUDED
#define CONFIG_LIB_SEL4_SIMPLE 1

63
repos/base-sel4/patches/autoconf_64.patch
View File

@ -1,63 +0,0 @@
--- src/kernel/sel4/configs/pc99/autoconf.h
+++ src/kernel/sel4/configs/pc99/autoconf.h
@@ -129,7 +129,7 @@
#define CONFIG_SEL4UTILS_STACK_SIZE 655360
#define CONFIG_HAVE_LIB_SEL4_ALLOCMAN 1
#define CONFIG_FASTPATH 1
-#define CONFIG_X2APIC 1
+#define CONFIG_XAPIC 1
#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_OBJS_SZ 0
#define CONFIG_HAVE_TIMER 1
#define CONFIG_SEL4UTILS_CSPACE_SIZE_BITS 18
@@ -147,7 +147,6 @@
#define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 230
#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0
#define CONFIG_SYSCALL 1
-#define CONFIG_MAX_NUM_NODES 1
#define CONFIG_CROSS_COMPILER_PREFIX ""
#define CONFIG_MAX_RMRR_ENTRIES 32
#define CONFIG_LIB_SEL4_INLINE_INVOCATIONS 1
@@ -162,21 +161,20 @@
#define CONFIG_OPTIMISATION_O2 1
#define CONFIG_HAVE_LIB_CPIO 1
#define CONFIG_HAVE_LIB_SEL4_VKA 1
-#define CONFIG_FSGSBASE_INST 1
+#define CONFIG_FSGSBASE_MSR 1
#define CONFIG_HAVE_LIB_SEL4_PLAT_SUPPORT 1
#define CONFIG_USER_EXTRA_CFLAGS "-D_XOPEN_SOURCE=700"
#define CONFIG_HAVE_FPU 1
#define CONFIG_FPU_MAX_RESTORES_SINCE_SWITCH 64
#define CONFIG_HAVE_LIB_SEL4_SIMPLE 1
#define CONFIG_HAVE_LIB_ELF 1
-#define CONFIG_SUPPORT_PCID 1
#define CONFIG_HAVE_LIB_PLATSUPPORT 1
-#define CONFIG_NUM_DOMAINS 16
+#define CONFIG_NUM_DOMAINS 1
#define CONFIG_HAVE_LIB_UTILS 1
#define CONFIG_USER_OPTIMISATION_O2 1
#define CONFIG_LIB_CPIO 1
#define CONFIG_RETYPE_FAN_OUT_LIMIT 256
-#define CONFIG_ROOT_CNODE_SIZE_BITS 16
+#define CONFIG_ROOT_CNODE_SIZE_BITS 18
#define CONFIG_NUM_PRIORITIES 256
#define CONFIG_TESTPRINTER_REGEX ".*"
#define CONFIG_APP_SEL4TEST 1
@@ -189,9 +187,16 @@
#define CONFIG_LIBSEL4DEBUG_ALLOC_BUFFER_ENTRIES 128
#define CONFIG_CACHE_LN_SZ 64
#define CONFIG_ARCH_X86_64 1
-#define CONFIG_HUGE_PAGE 1
#define CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES 1048576
#define CONFIG_BUILDSYS_USE_CCACHE 1
-#define CONFIG_MAX_NUM_NODES 1
+#define CONFIG_MAX_NUM_NODES 16
#define CONFIG_KERNEL_STACK_BITS 12
+#define CONFIG_ARCH_X86_GENERIC 1
+#define CONFIG_MULTIBOOT1_HEADER
+#define CONFIG_MULTIBOOT2_HEADER
+#define CONFIG_PRINTING 1
+#define CONFIG_ENABLE_BENCHMARKS 1
+#define CONFIG_BENCHMARK_TRACK_UTILISATION 1
+#define CONFIG_VTX 1
+#define CONFIG_MAX_VPIDS 64
#endif /* ARCH_IA32 */

63
repos/base-sel4/patches/config.patch
View File

@ -1,53 +1,22 @@
--- src/kernel/sel4/Makefile
+++ src/kernel/sel4/Makefile
@@ -287,8 +287,8 @@
# Only set CFLAGS if we're building standalone.
# common/Makefile.Flags sets NK_CFLAGS in Kbuild environments.
ifndef NK_CFLAGS
-STATICHEADERS += ${SOURCE_ROOT}/configs/$(PLAT)/autoconf.h
-INCLUDES += "-I${SOURCE_ROOT}/configs/$(PLAT)"
+STATICHEADERS += ${SOURCE_ROOT}/configs/$(PLAT)/$(BOARD)/autoconf.h
+INCLUDES += "-I${SOURCE_ROOT}/configs/$(PLAT)/$(BOARD)"
DEFINES += -DHAVE_AUTOCONF
ifdef DEBUG
DEFINES += -DCONFIG_DEBUG_BUILD
--- src/kernel/sel4/src/plat/pc99/linker.lds
+++ src/kernel/sel4/src/plat/pc99/linker.lds
@@ -16,13 +16,13 @@
#if defined(CONFIG_ARCH_IA32)
#undef i386
PADDR_BASE = 0x00000000;
-PADDR_LOAD = 0x00100000;
+PADDR_LOAD = 0x00200000;
KERNEL_BASE = 0xe0000000;
OUTPUT_ARCH(i386)
OUTPUT_FORMAT(elf32-i386)
#elif defined(CONFIG_ARCH_X86_64)
PADDR_BASE = 0x00000000;
-PADDR_LOAD = 0x00100000;
+PADDR_LOAD = 0x00200000;
KERNEL_BASE = 0xffffffff80000000;
OUTPUT_FORMAT(elf64-x86-64)
#endif
--- src/kernel/sel4/include/plat/pc99/plat/64/plat_mode/machine/hardware.h
+++ src/kernel/sel4/include/plat/pc99/plat/64/plat_mode/machine/hardware.h
@@ -19,7 +19,7 @@
* because they need to defined like this in linker.lds
*/
#define PADDR_BASE UL_CONST(0x00000000)
-#define PADDR_LOAD UL_CONST(0x00100000)
+#define PADDR_LOAD UL_CONST(0x00200000)
/* our kernel window is 2^39 bits (2^9 * 1gb) and the virtual address
* range is 48 bits. Therefore our base is 2^48 - 2^39
*/
@@ -87,7 +87,7 @@
#define PPTR_TOP UL_CONST(0xffffffff80000000)
/* The physical memory address to use for mapping the kernel ELF */
-#define KERNEL_ELF_PADDR_BASE UL_CONST(0x00100000)
+#define KERNEL_ELF_PADDR_BASE UL_CONST(0x00200000)
/* Kernel mapping starts directly after the physical memory window */
#define KERNEL_ELF_BASE (PPTR_TOP + KERNEL_ELF_PADDR_BASE)
--- src/kernel/sel4/include/plat/pc99/plat/32/plat_mode/machine/hardware.h
+++ src/kernel/sel4/include/plat/pc99/plat/32/plat_mode/machine/hardware.h
@@ -15,7 +15,7 @@
@@ -74,7 +74,7 @@
#define PPTR_TOP KS_LOG_PPTR
/* WARNING: some of these constants are also defined in linker.lds */
#define PADDR_BASE 0x00000000
-#define PADDR_LOAD 0x00100000
+#define PADDR_LOAD 0x00200000
#define PPTR_BASE 0xe0000000
/* The physical memory address to use for mapping the kernel ELF */
-#define KERNEL_ELF_PADDR_BASE UL_CONST(0x00100000)
+#define KERNEL_ELF_PADDR_BASE UL_CONST(0x00200000)
#define PPTR_USER_TOP (PPTR_BASE & (~MASK(seL4_LargePageBits)))
/* The base address in virtual memory to use for the kernel ELF mapping */
#define KERNEL_ELF_BASE (PPTR_BASE + KERNEL_ELF_PADDR_BASE)

24
repos/base-sel4/patches/gcc12.patch
View File

@ -1,17 +1,15 @@
gcc12.patch
diff --git src/kernel/sel4/src/arch/x86/kernel/cmdline.c src/kernel/sel4/src/arch/x86/kernel/cmdline.c
index 6ba5d8668..0459297fa 100644
--- src/kernel/sel4/src/arch/x86/kernel/cmdline.c
+++ src/kernel/sel4/src/arch/x86/kernel/cmdline.c
@@ -112,14 +112,20 @@ void cmdline_parse(const char *cmdline, cmdline_opt_t* cmdline_opt)
@@ -109,14 +109,20 @@
/* use BIOS data area to read serial configuration. The BDA is not
* fully standardized and parts are absolete. See http://wiki.osdev.org/Memory_Map_(x86)#BIOS_Data_Area_.28BDA.29
* for an explanation */
+#pragma GCC diagnostic push
+#pragma GCC diagnostic ignored "-Warray-bounds"
const unsigned short * bda_port = (unsigned short *)0x400;
const unsigned short * bda_equi = (unsigned short *)0x410;
const unsigned short *bda_port = (unsigned short *)0x400;
const unsigned short *bda_equi = (unsigned short *)0x410;
int const bda_ports_count = (*bda_equi >> 9) & 0x7;
+#pragma GCC diagnostic pop
#endif
@ -25,7 +23,7 @@ index 6ba5d8668..0459297fa 100644
if (parse_opt(cmdline, "console_port", cmdline_val, MAX_CMDLINE_VAL_LEN) != -1) {
parse_uint16_array(cmdline_val, &cmdline_opt->console_port, 1);
@@ -141,7 +147,10 @@ void cmdline_parse(const char *cmdline, cmdline_opt_t* cmdline_opt)
@@ -138,7 +144,10 @@
#ifdef CONFIG_DEBUG_BUILD
/* initialise to default or use BDA if available */
@ -36,16 +34,14 @@ index 6ba5d8668..0459297fa 100644
if (parse_opt(cmdline, "debug_port", cmdline_val, MAX_CMDLINE_VAL_LEN) != -1) {
parse_uint16_array(cmdline_val, &cmdline_opt->debug_port, 1);
}
diff --git src/kernel/sel4/tools/circular_includes.py src/kernel/sel4/tools/circular_includes.py
index 825a44a5e..dc4904939 100755
--- src/kernel/sel4/tools/circular_includes.py
+++ src/kernel/sel4/tools/circular_includes.py
@@ -26,7 +26,7 @@ def main():
resulting in the loop is printed out.
"""
@@ -28,7 +28,7 @@
if ignore_args and len(ignore_args):
ignore_args = [re.escape(ignore) for ignore in ignore_args]
ignore_re_string = '(' + '|'.join(ignore_args) + ')'
- ignore_re = re.compile(r'^# 1 ".*' + ignore_re_string + '"')
+ ignore_re = re.compile(r'^# [01] ".*' + ignore_re_string + '"')
- kernel_all_re = re.compile(r'^# 1 ".*kernel_all\.c"')
+ kernel_all_re = re.compile(r'^# [01] ".*kernel_all\.c"')
header_re = re.compile(r'^# (\d+) "(.*\..)"')
file_stack = []

27
repos/base-sel4/patches/imx6q_sabrelite.config
View File

@ -1,27 +0,0 @@
--- src/kernel/sel4/configs/imx6/imx6q_sabrelite/autoconf.h
+++ src/kernel/sel4/configs/imx6/imx6q_sabrelite/autoconf.h
@@ -41,6 +41,7 @@
#define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1
#define CONFIG_LIB_SEL4_UTILS 1
#define CONFIG_LIB_SEL4_VSPACE 1
+#define CONFIG_PRINTING 1
#define CONFIG_LIB_PLATSUPPORT 1
#define CONFIG_LIB_SEL4_ALLOCMAN 1
#define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1
@@ -78,7 +78,7 @@
#define CONFIG_USER_OPTIMISATION_O2 1
#define CONFIG_LIB_CPIO 1
#define CONFIG_RETYPE_FAN_OUT_LIMIT 256
-#define CONFIG_ROOT_CNODE_SIZE_BITS 12
+#define CONFIG_ROOT_CNODE_SIZE_BITS 15
#define CONFIG_NUM_PRIORITIES 256
#define CONFIG_TESTPRINTER_REGEX ".*"
#define CONFIG_APP_SEL4TEST 1
@@ -93,3 +93,7 @@
#define CONFIG_BUILDSYS_USE_CCACHE 1
#define CONFIG_MAX_NUM_NODES 1
#define CONFIG_KERNEL_STACK_BITS 12
+#define CONFIG_ENABLE_BENCHMARKS 1
+#define CONFIG_BENCHMARK_TRACK_UTILISATION 1
+#define CONFIG_HAVE_FPU 1
+#define CONFIG_FPU_MAX_RESTORES_SINCE_SWITCH 64

29
repos/base-sel4/patches/imx7d_sabre.config
View File

@ -1,29 +0,0 @@
--- src/kernel/sel4/configs/imx7/imx7d_sabre/autoconf.h
+++ src/kernel/sel4/configs/imx7/imx7d_sabre/autoconf.h
@@ -38,6 +38,7 @@
#define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1
#define CONFIG_LIB_SEL4_UTILS 1
#define CONFIG_LIB_SEL4_VSPACE 1
+#define CONFIG_PRINTING 1
#define CONFIG_LIB_PLATSUPPORT 1
#define CONFIG_LIB_SEL4_ALLOCMAN 1
#define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1
@@ -75,7 +76,7 @@
#define CONFIG_USER_OPTIMISATION_O2 1
#define CONFIG_LIB_CPIO 1
#define CONFIG_RETYPE_FAN_OUT_LIMIT 256
-#define CONFIG_ROOT_CNODE_SIZE_BITS 12
+#define CONFIG_ROOT_CNODE_SIZE_BITS 15
#define CONFIG_NUM_PRIORITIES 256
#define CONFIG_TESTPRINTER_REGEX ".*"
#define CONFIG_APP_SEL4TEST 1
@@ -89,3 +90,9 @@
#define CONFIG_BUILDSYS_USE_CCACHE 1
#define CONFIG_MAX_NUM_NODES 1
#define CONFIG_KERNEL_STACK_BITS 12
+#define CONFIG_ARCH_AARCH32 1
+#define CONFIG_IPC_BUF_TPIDRURW 1
+#define CONFIG_ENABLE_BENCHMARKS 1
+#define CONFIG_BENCHMARK_TRACK_UTILISATION 1
+#define CONFIG_HAVE_FPU 1
+#define CONFIG_FPU_MAX_RESTORES_SINCE_SWITCH 64

7
repos/base-sel4/patches/intel_vmcs.patch
View File

@ -1,15 +1,14 @@
--- src/kernel/sel4/src/arch/x86/object/vcpu.c
+++ src/kernel/sel4/src/arch/x86/object/vcpu.c
@@ -760,6 +774,8 @@ decodeWriteVMCS(cap_t cap, word_t length, word_t* buffer)
case VMX_GUEST_CR3:
@@ -713,6 +727,7 @@ static exception_t decodeWriteVMCS(cap_t cap, word_t length, word_t *buffer)
case VMX_CONTROL_EXCEPTION_BITMAP:
case VMX_CONTROL_ENTRY_INTERRUPTION_INFO:
+ case VMX_CONTROL_ENTRY_EXCEPTION_ERROR_CODE:
case VMX_CONTROL_ENTRY_EXCEPTION_ERROR_CODE:
+ case VMX_CONTROL_ENTRY_INSTRUCTION_LENGTH:
break;
case VMX_CONTROL_PIN_EXECUTION_CONTROLS:
value = applyFixedBits(value, pin_control_high, pin_control_low);
@@ -909,6 +925,7 @@ decodeReadVMCS(cap_t cap, word_t length, word_t* buffer)
@@ -860,6 +875,7 @@ static exception_t decodeReadVMCS(cap_t cap, word_t length, word_t *buffer)
case VMX_GUEST_CR0:
case VMX_GUEST_CR3:
case VMX_GUEST_CR4:

52
repos/base-sel4/patches/intel_vmx_full_state.patch
View File

@ -1,26 +1,14 @@
--- src/kernel/sel4/src/arch/x86/object/vcpu.c
+++ src/kernel/sel4/src/arch/x86/object/vcpu.c
@@ -88,6 +88,9 @@ static bool_t vmx_feature_ack_on_exit;
static vcpu_t *x86KSVPIDTable[VPID_LAST + 1];
static vpid_t x86KSNextVPID = VPID_FIRST;
@@ -921,6 +921,8 @@
vmwrite(VMX_CONTROL_ENTRY_INTERRUPTION_INFO, getSyscallArg(2, buffer));
}
+static void
+setMRs_vmexit(uint32_t reason, word_t qualification, tcb_t *tcb);
+static void setMRs_vmexit(uint32_t reason, word_t qualification, tcb_t *tcb);
+
static inline bool_t
vmxon(paddr_t vmxon_region)
void vcpu_sysvmenter_reply_to_user(tcb_t *tcb)
{
@@ -967,10 +987,8 @@ vcpu_update_state_sysvmenter(vcpu_t *vcpu)
void
vcpu_sysvmenter_reply_to_user(tcb_t *tcb)
{
- word_t *buffer;
vcpu_t *vcpu;
- buffer = lookupIPCBuffer(true, tcb);
vcpu = tcb->tcbArch.tcbVCPU;
assert(vcpu);
@@ -979,11 +997,9 @@ vcpu_sysvmenter_reply_to_user(tcb_t *tcb)
switchVCPU(vcpu);
}
@ -35,12 +23,12 @@
}
exception_t
@@ -1113,27 +1141,27 @@ vtx_init(void)
@@ -1065,29 +1067,29 @@
return true;
}
static void
-setMRs_vmexit(uint32_t reason, word_t qualification)
+setMRs_vmexit(uint32_t reason, word_t qualification, tcb_t *tcb)
-static void setMRs_vmexit(uint32_t reason, word_t qualification)
+static void setMRs_vmexit(uint32_t reason, word_t qualification, tcb_t *tcb)
{
word_t *buffer;
int i;
@ -49,21 +37,23 @@
+ buffer = lookupIPCBuffer(true, tcb);
- setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_CALL_EIP_MR, vmread(VMX_GUEST_RIP));
- setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_CALL_CONTROL_PPC_MR, vmread(VMX_CONTROL_PRIMARY_PROCESSOR_CONTROLS));
- setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_CALL_CONTROL_PPC_MR,
+ setMR(tcb, buffer, SEL4_VMENTER_CALL_EIP_MR, vmread(VMX_GUEST_RIP));
+ setMR(tcb, buffer, SEL4_VMENTER_CALL_CONTROL_PPC_MR,
vmread(VMX_CONTROL_PRIMARY_PROCESSOR_CONTROLS));
- setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_CALL_CONTROL_ENTRY_MR, vmread(VMX_CONTROL_ENTRY_INTERRUPTION_INFO));
- setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_REASON_MR, reason);
- setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_QUALIFICATION_MR, qualification);
+ setMR(tcb, buffer, SEL4_VMENTER_CALL_EIP_MR, vmread(VMX_GUEST_RIP));
+ setMR(tcb, buffer, SEL4_VMENTER_CALL_CONTROL_PPC_MR, vmread(VMX_CONTROL_PRIMARY_PROCESSOR_CONTROLS));
+ setMR(tcb, buffer, SEL4_VMENTER_CALL_CONTROL_ENTRY_MR, vmread(VMX_CONTROL_ENTRY_INTERRUPTION_INFO));
+ setMR(tcb, buffer, SEL4_VMENTER_FAULT_REASON_MR, reason);
+ setMR(tcb, buffer, SEL4_VMENTER_FAULT_QUALIFICATION_MR, qualification);
-
- setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_INSTRUCTION_LEN_MR, vmread(VMX_DATA_EXIT_INSTRUCTION_LENGTH));
- setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_GUEST_PHYSICAL_MR, vmread(VMX_DATA_GUEST_PHYSICAL));
- setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_RFLAGS_MR, vmread(VMX_GUEST_RFLAGS));
- setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_GUEST_INT_MR, vmread(VMX_GUEST_INTERRUPTABILITY));
- setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_CR3_MR, vmread(VMX_GUEST_CR3));
+ setMR(tcb, buffer, SEL4_VMENTER_CALL_CONTROL_ENTRY_MR, vmread(VMX_CONTROL_ENTRY_INTERRUPTION_INFO));
+ setMR(tcb, buffer, SEL4_VMENTER_FAULT_REASON_MR, reason);
+ setMR(tcb, buffer, SEL4_VMENTER_FAULT_QUALIFICATION_MR, qualification);
+
+ setMR(tcb, buffer, SEL4_VMENTER_FAULT_INSTRUCTION_LEN_MR, vmread(VMX_DATA_EXIT_INSTRUCTION_LENGTH));
+ setMR(tcb, buffer, SEL4_VMENTER_FAULT_GUEST_PHYSICAL_MR, vmread(VMX_DATA_GUEST_PHYSICAL));
+ setMR(tcb, buffer, SEL4_VMENTER_FAULT_RFLAGS_MR, vmread(VMX_GUEST_RFLAGS));
@ -71,8 +61,10 @@
+ setMR(tcb, buffer, SEL4_VMENTER_FAULT_CR3_MR, vmread(VMX_GUEST_CR3));
for (i = 0; i < n_vcpu_gp_register; i++) {
- setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_EAX + i, NODE_STATE(ksCurThread)->tcbArch.tcbVCPU->gp_registers[i]);
+ setMR(tcb, buffer, SEL4_VMENTER_FAULT_EAX + i, tcb->tcbArch.tcbVCPU->gp_registers[i]);
- setMR(NODE_STATE(ksCurThread), buffer, SEL4_VMENTER_FAULT_EAX + i,
- NODE_STATE(ksCurThread)->tcbArch.tcbVCPU->gp_registers[i]);
+ setMR(tcb, buffer, SEL4_VMENTER_FAULT_EAX + i,
+ tcb->tcbArch.tcbVCPU->gp_registers[i]);
}
}

15
repos/base-sel4/patches/intel_vtx_check.patch
View File

@ -36,15 +36,14 @@
case seL4_X86_EPTPML4Object:
--- src/kernel/sel4/src/arch/x86/object/vcpu.c
+++ src/kernel/sel4/src/arch/x86/object/vcpu.c
@@ -409,9 +416,14 @@ applyFixedBits(uint32_t original, uint32_t high, uint32_t low)
@@ -401,8 +401,13 @@
return original;
}
-void
-void vcpu_init(vcpu_t *vcpu)
+static bool_t vcpu_support_available = false;
+
+bool_t
vcpu_init(vcpu_t *vcpu)
+bool_t vcpu_init(vcpu_t *vcpu)
{
+ if (!vcpu_support_available)
+ return false;
@ -61,6 +60,14 @@
}
static void
@@ -937,6 +937,7 @@
buffer = lookupIPCBuffer(true, tcb);
vcpu = tcb->tcbArch.tcbVCPU;
+ (void)buffer;
assert(vcpu);
@@ -1067,6 +1081,12 @@ vtx_init(void)
printf("vt-x: lack of required features\n");
return false;

98
repos/base-sel4/patches/noise.patch
View File

@ -9,101 +9,3 @@
return;
default:
--- src/kernel/sel4/libsel4/include/sel4/shared_types.h
+++ src/kernel/sel4/libsel4/include/sel4/shared_types.h
@@ -33,7 +33,7 @@
seL4_CapFault_GuardMismatch_GuardFound = seL4_CapFault_DepthMismatch_BitsFound,
seL4_CapFault_GuardMismatch_BitsFound,
SEL4_FORCE_LONG_ENUM(seL4_CapFault_Msg),
-} seL4_CapFault_Msg;
+}; // seL4_CapFault_Msg;
#define seL4_ReadWrite seL4_CapRights_new(0, 1, 1)
#define seL4_AllRights seL4_CapRights_new(1, 1, 1)
--- src/kernel/sel4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h
+++ src/kernel/sel4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h
@@ -83,7 +83,7 @@
seL4_VMFault_FSR,
seL4_VMFault_Length,
SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg),
-} seL4_VMFault_Msg;
+}; // seL4_VMFault_Msg;
enum {
seL4_UnknownSyscall_EAX,
@@ -99,7 +99,7 @@
seL4_UnknownSyscall_Syscall,
seL4_UnknownSyscall_Length,
SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg),
-} seL4_UnknownSyscall_Msg;
+}; // seL4_UnknownSyscall_Msg;
enum {
seL4_UserException_FaultIP,
@@ -109,7 +109,7 @@
seL4_UserException_Code,
seL4_UserException_Length,
SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg)
-} seL4_UserException_Msg;
+}; // seL4_UserException_Msg;
#endif /* __ASSEMBLER__ */
#define seL4_FastMessageRegisters 2
--- src/kernel/sel4/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h
+++ src/kernel/sel4/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h
@@ -74,7 +74,7 @@
seL4_VMFault_FSR,
seL4_VMFault_Length,
SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg),
-} seL4_VMFault_Msg;
+}; // seL4_VMFault_Msg;
enum {
seL4_UnknownSyscall_RAX,
@@ -98,7 +98,7 @@
seL4_UnknownSyscall_Syscall,
seL4_UnknownSyscall_Length,
SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg)
-} seL4_UnknownSyscall_Msg;
+}; // seL4_UnknownSyscall_Msg;
enum {
seL4_UserException_FaultIP,
@@ -108,7 +108,7 @@
seL4_UserException_Code,
seL4_UserException_Length,
SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg)
-} seL4_UserException_Msg;
+}; // seL4_UserException_Msg;
#endif /* __ASSEMBLER__ */
#define seL4_FastMessageRegisters 4
--- src/kernel/sel4/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h
+++ src/kernel/sel4/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h
@@ -40,7 +40,7 @@
/* length of an unknown syscall message */
seL4_UnknownSyscall_Length,
SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg),
-} seL4_UnknownSyscall_Msg;
+}; // seL4_UnknownSyscall_Msg;
/* format of a user exception message */
enum {
@@ -52,7 +52,7 @@
/* length of a user exception */
seL4_UserException_Length,
SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg),
-} seL4_UserException_Msg;
+}; // seL4_UserException_Msg;
/* format of a vm fault message */
enum {
@@ -62,7 +62,7 @@
seL4_VMFault_FSR,
seL4_VMFault_Length,
SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg),
-} seL4_VMFault_Msg;
+}; // seL4_VMFault_Msg;
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
enum {

27
repos/base-sel4/patches/sched_bug_x86.patch
View File

@ -1,27 +0,0 @@
--- src/kernel/sel4/src/kernel/thread.c
+++ src/kernel/sel4/src/kernel/thread.c
@@ -437,8 +437,11 @@ scheduleTCB(tcb_t *tptr)
void
timerTick(void)
{
- if (likely(thread_state_get_tsType(NODE_STATE(ksCurThread)->tcbState) ==
- ThreadState_Running)) {
+ switch (thread_state_get_tsType(NODE_STATE(ksCurThread)->tcbState)) {
+ case ThreadState_Running:
+#ifdef CONFIG_VTX
+ case ThreadState_RunningVM:
+#endif
if (NODE_STATE(ksCurThread)->tcbTimeSlice > 1) {
NODE_STATE(ksCurThread)->tcbTimeSlice--;
} else {
@@ -446,6 +449,10 @@ timerTick(void)
SCHED_APPEND_CURRENT_TCB;
rescheduleRequired();
}
+ break;
+ default:
+ /* no tick updates */
+ break;
}
if (CONFIG_NUM_DOMAINS > 1) {

25
repos/base-sel4/patches/sel4_tlb_x86_bug.patch
View File

@ -1,25 +0,0 @@
--- src/kernel/sel4/src/arch/x86/kernel/vspace.c
+++ src/kernel/sel4/src/arch/x86/kernel/vspace.c
@@ -711,7 +711,6 @@ void unmapPage(vm_page_size_t page_size, asid_t asid, vptr_t vptr, void *pptr)
{
findVSpaceForASID_ret_t find_ret;
lookupPTSlot_ret_t lu_ret;
- cap_t threadRoot;
lookupPDSlot_ret_t pd_ret;
pde_t *pde;
@@ -756,12 +756,8 @@ void unmapPage(vm_page_size_t page_size, asid_t asid, vptr_t vptr, void *pptr)
break;
}
- /* check if page belongs to current address space */
- threadRoot = TCB_PTR_CTE_PTR(NODE_STATE(ksCurThread), tcbVTable)->cap;
- if (config_set(CONFIG_SUPPORT_PCID) || (isValidNativeRoot(threadRoot) && (vspace_root_t*)pptr_of_cap(threadRoot) == find_ret.vspace_root)) {
- invalidateTranslationSingleASID(vptr, asid,
- SMP_TERNARY(tlb_bitmap_get(find_ret.vspace_root), 0));
- }
+ invalidateTranslationSingleASID(vptr, asid,
+ SMP_TERNARY(tlb_bitmap_get(find_ret.vspace_root), 0));
}
void unmapPageTable(asid_t asid, vptr_t vaddr, pte_t* pt)

13
repos/base-sel4/patches/vcpu_nullptr_bug.patch
View File

@ -1,13 +0,0 @@
Bug detected by Genode and patch provided by Anna Lyons:
http://sel4.systems/pipermail/devel/2018-September/002161.html
--- src/kernel/sel4/src/arch/x86/c_traps.c
+++ src/kernel/sel4/src/arch/x86/c_traps.c
@@ -111,7 +111,7 @@ slowpath(syscall_t syscall)
{
#ifdef CONFIG_VTX
- if (syscall == SysVMEnter) {
+ if (syscall == SysVMEnter && NODE_STATE(ksCurThread)->tcbArch.tcbVCPU) {
vcpu_update_state_sysvmenter(NODE_STATE(ksCurThread)->tcbArch.tcbVCPU);
if (NODE_STATE(ksCurThread)->tcbBoundNotification && notification_ptr_get_state(NODE_STATE(ksCurThread)->tcbBoundNotification) == NtfnState_Active) {
completeSignal(NODE_STATE(ksCurThread)->tcbBoundNotification, NODE_STATE(ksCurThread));

2
repos/base-sel4/ports/sel4.hash
View File

@ -1 +1 @@
6879db476617c80bbf3467d6b02db11608688c9b
4cbe95411a514cec9492e32455db68d8c82b9766

28
repos/base-sel4/ports/sel4.port
View File

@ -3,31 +3,19 @@ VERSION := git
DOWNLOADS := sel4.git
URL(sel4) := https://github.com/seL4/seL4.git
# master branch, version 9.0.1
REV(sel4) := 0dd40b6c43a290173ea7782b97afbbbddfa23b36
# master branch, version 12.1.0
REV(sel4) := 21c1a2ca7a9786d1297e1ff0a132bc57eeb55530
DIR(sel4) := src/kernel/sel4
$(call check_tool,cmake)
$(call check_tool,ninja)
$(call check_tool,python)
$(call check_python_module,future)
$(call check_python_module,tempita)
$(call check_python_module,jinja2)
$(call check_python_module,ply)
$(call check_python_module,six)
# required for ARM
$(call check_python_module,pyfdt)
$(call check_python_module,jsonschema)
PATCHES := $(sort $(wildcard $(REP_DIR)/patches/*.patch))
HASH_INPUT += $(REP_DIR)/patches/imx6q_sabrelite.config
HASH_INPUT += $(REP_DIR)/patches/imx7d_sabre.config
# adjust kernel config usable on qemu and on native hw, and add a 32bit version
default: $(DOWNLOADS)
$(VERBOSE)mkdir -p src/kernel/sel4/configs/pc99/x86_64
$(VERBOSE)mkdir -p src/kernel/sel4/configs/pc99/ia32
$(VERBOSE)cp src/kernel/sel4/configs/pc99/autoconf.h src/kernel/sel4/configs/pc99/x86_64/autoconf.h
$(VERBOSE)mv src/kernel/sel4/configs/pc99/autoconf.h src/kernel/sel4/configs/pc99/ia32/autoconf.h
$(VERBOSE)sed -i "s.^ \*/. \*/\n#ifndef ARCH_IA32\n#define ARCH_IA32\n#endif\n." src/kernel/sel4/configs/pc99/ia32/autoconf.h
$(VERBOSE)mkdir -p src/kernel/sel4/configs/imx6/imx6q_sabrelite
$(VERBOSE)mv src/kernel/sel4/configs/imx6/autoconf.h src/kernel/sel4/configs/imx6/imx6q_sabrelite/autoconf.h
$(VERBOSE)patch -p0 <$(REP_DIR)/patches/imx6q_sabrelite.config
$(VERBOSE)mkdir -p src/kernel/sel4/configs/imx7/imx7d_sabre
$(VERBOSE)mv src/kernel/sel4/configs/imx7/autoconf.h src/kernel/sel4/configs/imx7/imx7d_sabre/autoconf.h
$(VERBOSE)patch -p0 <$(REP_DIR)/patches/imx7d_sabre.config

4
repos/base-sel4/recipes/src/base-sel4-x86/content.mk
View File

@ -23,9 +23,7 @@ etc/board.conf:
echo "BOARD = pc" > etc/board.conf
content:
for spec in x86_32 x86_64 arm; do \
mv lib/mk/spec/$$spec/ld-sel4.mk lib/mk/spec/$$spec/ld.mk; \
done;
mv lib/mk/spec/x86_64/ld-sel4.mk lib/mk/spec/x86_64/ld.mk;
sed -i "s/pit_timer_drv/timer/" src/timer/pit/target.inc
find lib/mk/spec -name kernel-sel4-*.mk -o -name syscall-sel4-*.mk |\
grep -v "sel4-pc.mk" | xargs rm -rf

3
repos/base-sel4/src/core/core_log_out.cc
View File

@ -15,7 +15,6 @@
#include <core_log.h>
/* seL4 includes */
#include <sel4/arch/functions.h>
#include <sel4/arch/syscalls.h>
#include <base/internal/sel4.h>
void Core::Core_log::out(char const c) { seL4_DebugPutChar(c); }

11
repos/base-sel4/src/core/include/core_cspace.h
View File

@ -35,12 +35,13 @@ class Core::Core_cspace
/* selectors for initially created CNodes during core bootup */
static unsigned top_cnode_sel() { return (unsigned)sel4_boot_info().empty.start; }
static unsigned core_pad_cnode_sel() { return top_cnode_sel() + 1; }
static unsigned core_pad_cnode_sel() { return top_cnode_sel() + 1; }
static unsigned core_cnode_sel() { return core_pad_cnode_sel() + 1; }
static unsigned phys_cnode_sel() { return core_cnode_sel() + 1; }
static unsigned untyped_cnode_4k() { return phys_cnode_sel() + 1; }
static unsigned untyped_cnode_16k() { return untyped_cnode_4k() + 1; }
static unsigned core_static_sel_end() { return untyped_cnode_16k() + 1; }
static unsigned phys_cnode_sel() { return core_cnode_sel() + 1; }
static unsigned untyped_cnode_4k() { return phys_cnode_sel() + 1; }
static unsigned untyped_cnode_16k() { return untyped_cnode_4k() + 1; }
static unsigned io_port_sel() { return untyped_cnode_16k() + 1; }
static unsigned core_static_sel_end() { return io_port_sel() + 1; }
/* indices within top-level CNode */
enum Top_cnode_idx {

16
repos/base-sel4/src/core/include/initial_untyped_pool.h
View File

@ -206,9 +206,6 @@ class Core::Initial_untyped_pool
size_t const retype_size_limit = get_page_size()*256;
size_t const batch_size = min(min(remaining_size, retype_size_limit), max_memory);
/* mark consumed untyped memory range as allocated */
range.free_offset += batch_size;
addr_t const phys_addr = range.phys + page_aligned_free_offset;
size_t const num_pages = batch_size / (1UL << size_log2);
@ -228,6 +225,13 @@ class Core::Initial_untyped_pool
return;
}
/* invoke callback about the range */
bool const used = func(phys_addr, num_pages << size_log2,
range.device);
if (!used)
return;
long const ret = seL4_Untyped_Retype(service,
type,
size_bits,
@ -243,6 +247,9 @@ class Core::Initial_untyped_pool
return;
}
/* mark consumed untyped memory range as allocated */
range.free_offset += batch_size;
/* track memory left to be converted */
max_memory -= batch_size;
@ -251,9 +258,6 @@ class Core::Initial_untyped_pool
size_t const num_pages = batch_size >> get_page_size_log2();
Untyped_memory::convert_to_page_frames(phys_addr, num_pages);
}
/* invoke callback about the range */
func(phys_addr, num_pages << size_log2, range.device);
}
});
}

5
repos/base-sel4/src/core/include/platform.h
View File

@ -225,6 +225,11 @@ class Core::Platform : public Platform_generic
*/
long _unmap_page_frame(Cap_sel const &);
/**
* Initialize I/O ports on x86
*/
void _init_io_ports();
public:
/**

6
repos/base-sel4/src/core/include/platform_thread.h
View File

@ -50,8 +50,8 @@ class Core::Platform_thread : public List<Platform_thread>::Element
/**
* Virtual address of the IPC buffer within the PDs address space
*
* The value is 0 for the PD's main thread. For all other threads,
* the value is somewhere within the stack area.
* The value for the PD's main thread is INITIAL_IPC_BUFFER_VIRT.
* For all other threads, the value is somewhere within the stack area.
*/
addr_t const _utcb;
@ -79,6 +79,8 @@ class Core::Platform_thread : public List<Platform_thread>::Element
Affinity::Location _location;
uint16_t _priority;
bool main_thread() const { return _utcb == INITIAL_IPC_BUFFER_VIRT; }
public:
/**

2
repos/base-sel4/src/core/include/sel4_boot_info.h
View File

@ -15,7 +15,7 @@
#define _CORE__INCLUDE__SEL4_BOOT_INFO_H_
/* seL4 includes */
#include <sel4/bootinfo.h>
#include <base/internal/sel4.h>
/* core includes */
#include <types.h>

3
repos/base-sel4/src/core/include/thread_sel4.h
View File

@ -33,7 +33,8 @@ namespace Core {
* Set register values for the instruction pointer and stack pointer and
* start the seL4 thread
*/
void start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, unsigned cpu);
void start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, unsigned cpu,
addr_t tls_ipcbuffer);
void affinity_sel4_thread(Cap_sel const &tcb_sel, unsigned cpu);
}

6
repos/base-sel4/src/core/include/untyped_memory.h
View File

@ -122,8 +122,10 @@ struct Core::Untyped_memory
num_objects);
if (ret != seL4_NoError) {
error(__FUNCTION__, ": seL4_Untyped_RetypeAtOffset (IA32_4K) "
"returned ", ret);
error(__FUNCTION__, ": seL4_Untyped_RetypeAtOffset "
"returned ", ret, " - physical_range=",
Hex_range(node_offset << get_page_size_log2(),
(num_pages - i) * get_page_size()));
return;
}
}

12
repos/base-sel4/src/core/platform.cc
View File

@ -103,18 +103,20 @@ void Platform::_init_allocators()
/* turn remaining untyped memory ranges into untyped pages */
_initial_untyped_pool.turn_into_untyped_object(Core_cspace::TOP_CNODE_UNTYPED_4K,
[&] (addr_t const phys, addr_t const size, bool const device) {
[&] (addr_t const phys, addr_t const size, bool const device_memory) {
/* register to physical or iomem memory allocator */
addr_t const phys_addr = trunc_page(phys);
size_t const phys_size = round_page(phys - phys_addr + size);
if (device)
if (device_memory)
_io_mem_alloc.add_range(phys_addr, phys_size);
else
_core_mem_alloc.phys_alloc().add_range(phys_addr, phys_size);
_unused_phys_alloc.remove_range(phys_addr, phys_size);
return true; /* range used by this functor */
});
/*
@ -174,7 +176,7 @@ void Platform::_switch_to_core_cspace()
_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapASIDControl));
_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapInitThreadASIDPool));
/* XXX io port not available on ARM, causes just a kernel warning XXX */
_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapIOPort));
_core_cnode.move(initial_cspace, Cnode_index(seL4_CapIOPortControl));
_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapBootInfoFrame));
_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapInitThreadIPCBuffer));
_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapDomain));
@ -648,8 +650,8 @@ Platform::Platform()
affinity_space().height()));
}
/* I/O port allocator (only meaningful for x86) */
_io_port_alloc.add_range(0, 0x10000);
/* solely meaningful for x86 */
_init_io_ports();
_init_rom_modules();

17
repos/base-sel4/src/core/platform_pd.cc
View File

@ -58,7 +58,8 @@ bool Platform_pd::bind_thread(Platform_thread &thread)
thread._ep_sel = alloc_sel();
thread._vcpu_sel = alloc_sel();
/* allocate asynchronous selector used for locks in the PD's CSpace */
thread._lock_sel = thread._utcb ? alloc_sel() : Cap_sel(INITIAL_SEL_LOCK);
thread._lock_sel = thread.main_thread() ? Cap_sel(INITIAL_SEL_LOCK)
: alloc_sel();
thread._vcpu_notify_sel = alloc_sel();
} catch (Platform_pd::Sel_bit_alloc::Out_of_indices) {
if (thread._fault_handler_sel.value()) {
@ -92,24 +93,21 @@ bool Platform_pd::bind_thread(Platform_thread &thread)
* to attach the UTCB as a dataspace to the stack area to make the RM
* session aware to the mapping. This code is missing.
*/
addr_t const utcb = (thread._utcb) ? thread._utcb
: (addr_t)thread.INITIAL_IPC_BUFFER_VIRT;
Vm_space::Map_attr const attr { .cached = true,
.write_combined = false,
.writeable = true,
.executable = false,
.flush_support = true };
enum { ONE_PAGE = 1 };
_vm_space.alloc_page_tables(utcb, get_page_size());
_vm_space.map(thread._info.ipc_buffer_phys, utcb, ONE_PAGE, attr);
_vm_space.alloc_page_tables(thread._utcb, get_page_size());
_vm_space.map(thread._info.ipc_buffer_phys, thread._utcb, ONE_PAGE, attr);
return true;
}
void Platform_pd::unbind_thread(Platform_thread &thread)
{
if (thread._utcb)
if (not thread.main_thread())
free_sel(thread._lock_sel);
free_sel(thread._fault_handler_sel);
@ -117,10 +115,7 @@ void Platform_pd::unbind_thread(Platform_thread &thread)
free_sel(thread._vcpu_sel);
free_sel(thread._vcpu_notify_sel);
if (thread._utcb)
_vm_space.unmap(thread._utcb, 1);
else
_vm_space.unmap(thread.INITIAL_IPC_BUFFER_VIRT, 1);
_vm_space.unmap(thread._utcb, 1);
}

19
repos/base-sel4/src/core/platform_thread.cc
View File

@ -94,8 +94,10 @@ bool Core::install_mapping(Mapping const &mapping, unsigned long pager_object_ba
** Utilities to support the Platform_thread interface **
********************************************************/
static void prepopulate_ipc_buffer(addr_t ipc_buffer_phys, Cap_sel ep_sel,
Cap_sel lock_sel)
static void prepopulate_ipc_buffer(addr_t const ipc_buffer_phys,
Cap_sel const ep_sel,
Cap_sel const lock_sel,
addr_t const utcb_virt)
{
/* IPC buffer is one page */
size_t const page_rounded_size = get_page_size();
@ -112,6 +114,7 @@ static void prepopulate_ipc_buffer(addr_t ipc_buffer_phys, Cap_sel ep_sel,
Native_utcb &utcb = *(Native_utcb *)virt_ptr;
utcb.ep_sel (ep_sel .value());
utcb.lock_sel(lock_sel.value());
utcb.ipcbuffer(utcb_virt);
/* unmap IPC buffer from core */
if (!unmap_local((addr_t)virt_ptr, 1)) {
@ -161,7 +164,7 @@ int Platform_thread::start(void *ip, void *sp, unsigned int)
* thread. Once started, the thread picks up this information in the
* 'Thread::_thread_bootstrap' method.
*/
prepopulate_ipc_buffer(_info.ipc_buffer_phys, _ep_sel, _lock_sel);
prepopulate_ipc_buffer(_info.ipc_buffer_phys, _ep_sel, _lock_sel, _utcb);
/* bind thread to PD and CSpace */
seL4_CNode_CapData const guard_cap_data =
@ -177,7 +180,8 @@ int Platform_thread::start(void *ip, void *sp, unsigned int)
no_cap_data.words[0]);
ASSERT(ret == 0);
start_sel4_thread(_info.tcb_sel, (addr_t)ip, (addr_t)(sp), _location.xpos());
start_sel4_thread(_info.tcb_sel, (addr_t)ip, (addr_t)(sp), _location.xpos(),
_utcb);
return 0;
}
@ -215,7 +219,7 @@ Platform_thread::Platform_thread(size_t, const char *name, unsigned priority,
Affinity::Location location, addr_t utcb)
:
_name(name),
_utcb(utcb),
_utcb(utcb ? utcb : addr_t(INITIAL_IPC_BUFFER_VIRT)),
_pager_obj_sel(platform_specific().core_sel_alloc().alloc()),
_location(location),
_priority((uint16_t)(Cpu_session::scale_priority(CONFIG_NUM_PRIORITIES, priority)))
@ -226,7 +230,7 @@ Platform_thread::Platform_thread(size_t, const char *name, unsigned priority,
if (_priority > 0)
_priority -= 1;
_info.init(_utcb ? _utcb : (addr_t)INITIAL_IPC_BUFFER_VIRT, _priority);
_info.init(_utcb, _priority);
platform_thread_registry().insert(*this);
}
@ -284,5 +288,6 @@ void Platform_thread::setup_vcpu(Cap_sel ept, Cap_sel notification)
_pd->cspace_cnode(_vcpu_notify_sel).copy(platform_specific().core_cnode(),
notification, _vcpu_notify_sel);
prepopulate_ipc_buffer(_info.ipc_buffer_phys, _vcpu_sel, _vcpu_notify_sel);
prepopulate_ipc_buffer(_info.ipc_buffer_phys, _vcpu_sel, _vcpu_notify_sel,
_utcb);
}

23
repos/base-sel4/src/core/spec/arm/platform.cc
View File

@ -40,7 +40,15 @@ seL4_Word Untyped_memory::smallest_page_type() {
return seL4_ARM_SmallPageObject; }
void Platform::init_sel4_ipc_buffer() { }
void Platform::init_sel4_ipc_buffer()
{
/*
* Setup tls pointer such, that it points to the (kernel created) core
* main thread IPC buffer. It is used in seL4_GetIPCBuffer().
*/
seL4_BootInfo const &bi = sel4_boot_info();
seL4_SetTLSBase((unsigned long)&bi.ipcBuffer);
}
long Platform::_unmap_page_frame(Cap_sel const &sel) {
@ -78,9 +86,15 @@ void Platform::_init_core_page_table_registry()
addr_t const max_pd_mem = MAX_PROCESS_COUNT * (1UL << Page_directory_kobj::SIZE_LOG2);
_initial_untyped_pool.turn_into_untyped_object(Core_cspace::TOP_CNODE_UNTYPED_16K,
[&] (addr_t const phys, addr_t const size, bool) {
[&] (addr_t const phys, addr_t const size, bool const device_memory) {
if (device_memory)
return false;
phys_alloc_16k().add_range(phys, size);
_unused_phys_alloc.remove_range(phys, size);
return true;
},
Page_directory_kobj::SIZE_LOG2, max_pd_mem);
@ -122,3 +136,8 @@ void Platform_pd::_deinit_page_directory(addr_t phys_addr) const
Untyped_memory::free_page(phys_alloc_16k(), phys_addr);
}
void Platform::_init_io_ports()
{
}

12
repos/base-sel4/src/core/spec/arm/thread.cc
View File

@ -15,6 +15,7 @@
*/
/* base includes */
#include <base/internal/native_utcb.h>
#include <base/thread_state.h>
/* core includes */
@ -24,7 +25,8 @@
using namespace Core;
void Core::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, unsigned cpu)
void Core::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp,
unsigned cpu, addr_t const virt_utcb)
{
/* set register values for the instruction pointer and stack pointer */
seL4_UserContext regs;
@ -40,6 +42,14 @@ void Core::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, unsigned cpu
affinity_sel4_thread(tcb_sel, cpu);
/*
* Set tls pointer to location, where ipcbuffer address is stored, so
* that it can be used by seL4_GetIPCBuffer()
*/
auto error = seL4_TCB_SetTLSBase(tcb_sel.value(),
virt_utcb + Native_utcb::tls_ipcbuffer_offset);
ASSERT(not error);
seL4_TCB_Resume(tcb_sel.value());
}

12
repos/base-sel4/src/core/spec/x86/io_port_session_support.cc
View File

@ -25,7 +25,7 @@ unsigned char Io_port_session_component::inb(unsigned short address)
/* check boundaries */
if (!_in_bounds(address, sizeof(unsigned char))) return 0;
seL4_X86_IOPort_In8_t v = seL4_X86_IOPort_In8(seL4_CapIOPort, address);
auto const v = seL4_X86_IOPort_In8(Core_cspace::io_port_sel(), address);
if (v.error == seL4_NoError)
return v.result;
@ -39,7 +39,7 @@ unsigned short Io_port_session_component::inw(unsigned short address)
/* check boundaries */
if (!_in_bounds(address, sizeof(unsigned short))) return 0;
seL4_X86_IOPort_In16_t v = seL4_X86_IOPort_In16(seL4_CapIOPort, address);
auto const v = seL4_X86_IOPort_In16(Core_cspace::io_port_sel(), address);
if (v.error == seL4_NoError)
return v.result;
@ -53,7 +53,7 @@ unsigned Io_port_session_component::inl(unsigned short address)
/* check boundaries */
if (!_in_bounds(address, sizeof(unsigned))) return 0;
seL4_X86_IOPort_In32_t v = seL4_X86_IOPort_In32(seL4_CapIOPort, address);
auto const v = seL4_X86_IOPort_In32(Core_cspace::io_port_sel(), address);
if (v.error == seL4_NoError)
return v.result;
@ -67,7 +67,7 @@ void Io_port_session_component::outb(unsigned short address, unsigned char value
/* check boundaries */
if (!_in_bounds(address, sizeof(unsigned char))) return;
int result = seL4_X86_IOPort_Out8(seL4_CapIOPort, address, value);
int result = seL4_X86_IOPort_Out8(Core_cspace::io_port_sel(), address, value);
if (result != seL4_NoError)
error(__PRETTY_FUNCTION__, " failed ", result);
@ -79,7 +79,7 @@ void Io_port_session_component::outw(unsigned short address, unsigned short valu
/* check boundaries */
if (!_in_bounds(address, sizeof(unsigned short))) return;
int result = seL4_X86_IOPort_Out16(seL4_CapIOPort, address, value);
int result = seL4_X86_IOPort_Out16(Core_cspace::io_port_sel(), address, value);
if (result != seL4_NoError)
error(__PRETTY_FUNCTION__, " failed ", result);
@ -91,7 +91,7 @@ void Io_port_session_component::outl(unsigned short address, unsigned value)
/* check boundaries */
if (!_in_bounds(address, sizeof(unsigned))) return;
int result = seL4_X86_IOPort_Out32(seL4_CapIOPort, address, value);
int result = seL4_X86_IOPort_Out32(Core_cspace::io_port_sel(), address, value);
if (result != seL4_NoError)
error(__PRETTY_FUNCTION__, " failed ", result);

58
repos/base-sel4/src/core/spec/x86_64/platform.cc
View File

@ -27,7 +27,15 @@ using namespace Core;
seL4_Word Untyped_memory::smallest_page_type() { return seL4_X86_4K; }
void Platform::init_sel4_ipc_buffer() { }
void Platform::init_sel4_ipc_buffer()
{
/*
* Setup tls pointer such, that it points to the (kernel created) core
* main thread IPC buffer. The fs register is used in seL4_GetIPCBuffer().
*/
seL4_BootInfo const &bi = sel4_boot_info();
seL4_SetTLSBase((unsigned long)&bi.ipcBuffer);
}
long Platform::_unmap_page_frame(Cap_sel const &sel) {
@ -74,31 +82,37 @@ void Platform::_init_core_page_table_registry()
addr_t const max_pd_mem = MAX_VCPU_COUNT * (1UL << Vcpu_kobj::SIZE_LOG2);
_initial_untyped_pool.turn_into_untyped_object(Core_cspace::TOP_CNODE_UNTYPED_16K,
[&] (addr_t const phys, addr_t const size, bool) {
[&] (addr_t const phys, addr_t const size, bool const device_memory) {
if (device_memory)
return false;
phys_alloc_16k().add_range(phys, size);
_unused_phys_alloc.remove_range(phys, size);
return true;
},
Vcpu_kobj::SIZE_LOG2, max_pd_mem);
log(":phys_mem_16k: ", phys_alloc_16k());
/*
* Register initial page frames
* - actually we don't use them in core -> skip
*/
#if 0
addr_t const modules_start = reinterpret_cast<addr_t>(&_boot_modules_binaries_begin);
addr_t const modules_end = reinterpret_cast<addr_t>(&_boot_modules_binaries_end);
virt_addr = (addr_t)(&_prog_img_beg);
for (unsigned sel = bi.userImageFrames.start;
sel < bi.userImageFrames.end;
sel++, virt_addr += get_page_size()) {
/* skip boot modules */
if (modules_start <= virt_addr && virt_addr <= modules_end)
continue;
_core_page_table_registry.insert_page_table_entry(virt_addr, sel);
}
#endif
}
void Platform::_init_io_ports()
{
enum { PORTS = 0x10000, PORT_FIRST = 0, PORT_LAST = PORTS - 1 };
/* I/O port allocator (only meaningful for x86) */
_io_port_alloc.add_range(PORT_FIRST, PORTS);
/* create I/O port capability used by io_port_session_support.cc */
auto const root = _core_cnode.sel().value();
auto const index = Core_cspace::io_port_sel();
auto const depth = CONFIG_ROOT_CNODE_SIZE_BITS;
auto const result = seL4_X86_IOPortControl_Issue(seL4_CapIOPortControl,
PORT_FIRST, PORT_LAST,
root, index, depth);
if (result != 0)
error("IO Port access not available");
}

12
repos/base-sel4/src/core/spec/x86_64/thread.cc
View File

@ -15,6 +15,7 @@
*/
/* base includes */
#include <base/internal/native_utcb.h>
#include <base/thread_state.h>
/* core includes */
@ -24,7 +25,8 @@
using namespace Core;
void Core::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, unsigned cpu)
void Core::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp,
unsigned cpu, addr_t const virt_utcb)
{
/* set register values for the instruction pointer and stack pointer */
seL4_UserContext regs;
@ -40,6 +42,14 @@ void Core::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, unsigned cpu
affinity_sel4_thread(tcb_sel, cpu);
/*
* Set tls pointer to location, where ipcbuffer address is stored, so
* that it can be used by register fs (seL4_GetIPCBuffer())
*/
auto error = seL4_TCB_SetTLSBase(tcb_sel.value(),
virt_utcb + Native_utcb::tls_ipcbuffer_offset);
ASSERT(not error);
seL4_TCB_Resume(tcb_sel.value());
}

5
repos/base-sel4/src/core/thread_start.cc
View File

@ -101,8 +101,11 @@ void Thread::_thread_start()
void Thread::start()
{
/* write ipcbuffer address to utcb*/
utcb()->ipcbuffer(addr_t(utcb()));
start_sel4_thread(Cap_sel(native_thread().tcb_sel), (addr_t)&_thread_start,
(addr_t)stack_top(), _affinity.xpos());
(addr_t)stack_top(), _affinity.xpos(), addr_t(utcb()));
struct Core_trace_source : public Core::Trace::Source::Info_accessor,
private Core::Trace::Control,

4
repos/base-sel4/src/include/base/internal/native_utcb.h
View File

@ -35,6 +35,10 @@ struct Genode::Native_utcb
void ep_sel (addr_t sel) { _raw[ELEMENTS - 1] = sel; }
void lock_sel(addr_t sel) { _raw[ELEMENTS - 2] = sel; }
static addr_t constexpr tls_ipcbuffer_offset = (ELEMENTS - 3) * sizeof(_raw[0]);
void ipcbuffer(addr_t const addr) { _raw[ELEMENTS - 3] = addr; }
};
#endif /* _INCLUDE__BASE__INTERNAL__NATIVE_UTCB_H_ */

3
repos/base-sel4/src/include/base/internal/raw_write_string.h
View File

@ -15,8 +15,7 @@
#define _INCLUDE__BASE__INTERNAL__RAW_WRITE_STRING_H_
/* seL4 includes */
#include <sel4/arch/functions.h>
#include <sel4/arch/syscalls.h>
#include <base/internal/sel4.h>
namespace Genode {

2
tool/run/boot_dir/sel4
View File

@ -12,7 +12,7 @@ proc kernel_files { } { return sel4 }
proc boot_output { } { return "serial" }
proc run_boot_string { } { return "\n\rBooting all finished, dropped to user space" }
proc run_boot_string { } { return "\nBooting all finished, dropped to user space" }
proc core_link_address { } { return "0x02000000" }
proc sel4_elfloader_dir { } {