From 95329c82e2585338f1977c384c20f58250b861d9 Mon Sep 17 00:00:00 2001 From: Alexander Boettcher Date: Mon, 12 Jun 2017 12:41:38 +0200 Subject: [PATCH] sel4: update to 5.2.0 Issue #2451 --- .../lib/import/import-syscall-sel4.mk | 2 +- .../lib/mk/spec/x86_32/kernel-sel4.mk | 5 +- .../lib/mk/spec/x86_32/syscall-sel4.mk | 42 +- repos/base-sel4/patches/autoconf_32.patch | 66 ++ repos/base-sel4/patches/dev_mem.patch | 150 ----- repos/base-sel4/patches/dev_mem_4k.patch | 11 - repos/base-sel4/patches/noise.patch | 40 ++ repos/base-sel4/patches/root_cnode.patch | 6 +- repos/base-sel4/patches/serial.patch | 24 - repos/base-sel4/patches/syscall.patch | 626 ------------------ repos/base-sel4/ports/sel4.hash | 2 +- repos/base-sel4/ports/sel4.port | 6 +- repos/base-sel4/src/core/capability_space.cc | 16 +- repos/base-sel4/src/core/include/cnode.h | 37 +- .../src/core/include/initial_untyped_pool.h | 15 +- .../src/core/include/kernel_object.h | 76 +-- .../src/core/include/page_table_registry.h | 2 +- repos/base-sel4/src/core/include/platform.h | 9 +- .../base-sel4/src/core/include/thread_sel4.h | 32 +- repos/base-sel4/src/core/include/vm_space.h | 49 +- .../src/core/irq_session_component.cc | 9 +- repos/base-sel4/src/core/pager.cc | 2 +- repos/base-sel4/src/core/platform.cc | 161 +++-- repos/base-sel4/src/core/platform_pd.cc | 22 +- .../src/core/signal_source_component.cc | 7 +- repos/libports/run/acpica.run | 3 +- repos/os/run/rom_filter.run | 2 +- tool/run/boot_dir/sel4 | 2 + 28 files changed, 375 insertions(+), 1049 deletions(-) create mode 100644 repos/base-sel4/patches/autoconf_32.patch delete mode 100644 repos/base-sel4/patches/dev_mem.patch delete mode 100644 repos/base-sel4/patches/dev_mem_4k.patch delete mode 100644 repos/base-sel4/patches/serial.patch delete mode 100644 repos/base-sel4/patches/syscall.patch diff --git a/repos/base-sel4/lib/import/import-syscall-sel4.mk b/repos/base-sel4/lib/import/import-syscall-sel4.mk index bf94fa91a..9f64c6cd0 100644 --- a/repos/base-sel4/lib/import/import-syscall-sel4.mk +++ b/repos/base-sel4/lib/import/import-syscall-sel4.mk @@ -12,4 +12,4 @@ INC_DIR += $(SEL4_INCLUDE_DIR) INC_DIR += $(SEL4_INCLUDE_DIR)/sel4 # required for seL4_DebugPutChar -CC_OPT += -DSEL4_DEBUG_KERNEL -DDEBUG +CC_OPT += -DCONFIG_PRINTING diff --git a/repos/base-sel4/lib/mk/spec/x86_32/kernel-sel4.mk b/repos/base-sel4/lib/mk/spec/x86_32/kernel-sel4.mk index e86563bd5..ce0919d2f 100644 --- a/repos/base-sel4/lib/mk/spec/x86_32/kernel-sel4.mk +++ b/repos/base-sel4/lib/mk/spec/x86_32/kernel-sel4.mk @@ -13,13 +13,16 @@ endif LINKER_OPT_PREFIX := -Wl, +# memmove is missing in seL4 5.2.0 - code is generated by our gcc compiler +AVOID_CALLS_TO_MEMMOVE := -fno-tree-loop-distribute-patterns + build_kernel: $(VERBOSE)$(MAKE) \ TOOLPREFIX=$(CROSS_DEV_PREFIX) \ ARCH=x86 SEL4_ARCH=ia32 PLAT=pc99 DEBUG=1 \ LDFLAGS+=-nostdlib LDFLAGS+=-Wl,-nostdlib \ $(addprefix LDFLAGS+=$(LINKER_OPT_PREFIX),$(LD_MARCH)) \ - CFLAGS+="-fno-builtin-printf -O3" \ + CFLAGS+="-fno-builtin-printf -O3 $(AVOID_CALLS_TO_MEMMOVE)" \ $(addprefix CFLAGS+=,$(CC_MARCH)) \ SOURCE_ROOT=$(SEL4_DIR) -f$(SEL4_DIR)/Makefile diff --git a/repos/base-sel4/lib/mk/spec/x86_32/syscall-sel4.mk b/repos/base-sel4/lib/mk/spec/x86_32/syscall-sel4.mk index 0c938ecbb..9766391f2 100644 --- a/repos/base-sel4/lib/mk/spec/x86_32/syscall-sel4.mk +++ b/repos/base-sel4/lib/mk/spec/x86_32/syscall-sel4.mk @@ -10,7 +10,7 @@ # 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/include/plat/pc99 +LIBSEL4_AUTO:= $(call select_from_ports,sel4)/src/kernel/sel4/configs/pc99 # # Execute the rules in this file only at the second build stage when we know @@ -26,19 +26,23 @@ ifeq ($(called_from_lib_mk),yes) # SEL4_ARCH_INCLUDES := simple_types.h types.h constants.h objecttype.h \ - functions.h syscalls.h invocation.h deprecated.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 \ pfIPC.h syscalls.h exIPC.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 types_gen.h syscall.h \ - invocation.h shared_types_gen.h debug_assert.h shared_types.h \ - sel4.h deprecated.h autoconf.h +INCLUDES := objecttype.h types.h bootinfo.h bootinfo_types.h errors.h \ + constants.h messages.h sel4.h macros.h simple_types.h types_gen.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 + +PLAT_API_INCLUDES := constants.h INCLUDE_SYMLINKS += $(addprefix include/sel4/, $(INCLUDES)) INCLUDE_SYMLINKS += $(addprefix include/sel4/arch/, $(ARCH_INCLUDES)) INCLUDE_SYMLINKS += $(addprefix include/sel4/sel4_arch/,$(SEL4_ARCH_INCLUDES)) +INCLUDE_SYMLINKS += $(addprefix include/sel4/plat/api/, $(PLAT_API_INCLUDES)) INCLUDE_SYMLINKS += include/interfaces/sel4_client.h all: $(INCLUDE_SYMLINKS) @@ -62,22 +66,42 @@ include/sel4/%.h: $(LIBSEL4_DIR)/include/sel4/%.h $(VERBOSE)mkdir -p $(dir $@) $(VERBOSE)ln -sf $< $@ +include/sel4/plat/api/%.h: $(LIBSEL4_DIR)/sel4_plat_include/pc99/sel4/plat/api/%.h + $(VERBOSE)mkdir -p $(dir $@) + $(VERBOSE)ln -sf $< $@ + # # Generated headers # -include/sel4/types_gen.h: $(LIBSEL4_DIR)/include/sel4/types_32.bf +include/sel4/%.pbf: $(LIBSEL4_DIR)/include/sel4/%.bf include/sel4/autoconf.h + $(MSG_CONVERT)$(notdir $@) + $(VERBOSE)mkdir -p $(dir $@) + $(VERBOSE)$(CPP) -P $< >$@ + +include/sel4/sel4_arch/types.pbf: $(LIBSEL4_DIR)/sel4_arch_include/ia32/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/x86 -P $< >$@ + +include/sel4/types_gen.h: include/sel4/types_32.pbf $(MSG_CONVERT)$(notdir $@) $(VERBOSE)mkdir -p $(dir $@) $(VERBOSE)python $(LIBSEL4_DIR)/tools/bitfield_gen.py \ --environment libsel4 "$<" $@ -include/sel4/shared_types_gen.h: $(LIBSEL4_DIR)/include/sel4/shared_types_32.bf +include/sel4/shared_types_gen.h: include/sel4/shared_types_32.pbf $(MSG_CONVERT)$(notdir $@) $(VERBOSE)mkdir -p $(dir $@) $(VERBOSE)python $(LIBSEL4_DIR)/tools/bitfield_gen.py \ --environment libsel4 "$<" $@ -include/sel4/syscall.h: $(LIBSEL4_DIR)/include/api/syscall.xml +include/sel4/sel4_arch/types_gen.h: include/sel4/sel4_arch/types.pbf + $(MSG_CONVERT)$(notdir $@) + $(VERBOSE)mkdir -p $(dir $@) + $(VERBOSE)python $(LIBSEL4_DIR)/tools/bitfield_gen.py \ + --environment libsel4 "$<" $@ + +include/sel4/syscall.h: $(LIBSEL4_DIR)/include/api/syscall.xml $(LIBSEL4_DIR)/include/api/syscall.xsd $(MSG_CONVERT)$(notdir $@) $(VERBOSE)mkdir -p $(dir $@) $(VERBOSE)python $(LIBSEL4_DIR)/tools/syscall_header_gen.py \ diff --git a/repos/base-sel4/patches/autoconf_32.patch b/repos/base-sel4/patches/autoconf_32.patch new file mode 100644 index 000000000..30e851a60 --- /dev/null +++ b/repos/base-sel4/patches/autoconf_32.patch @@ -0,0 +1,66 @@ +--- src/kernel/sel4/configs/pc99/autoconf.h ++++ src/kernel/sel4/configs/pc99/autoconf.h +@@ -24,7 +24,8 @@ + #define CONFIG_HAVE_LIBC 1 + #define CONFIG_USER_COMPILER "" + #define CONFIG_LIB_SEL4_PLAT_SUPPORT 1 +-#define CONFIG_WORD_SIZE 64 ++#define CONFIG_WORD_SIZE 32 ++#define CONFIG_ARCH_X86_GENERIC 1 + #define CONFIG_ARCH_X86 1 + #define CONFIG_APP_TESTS 1 + #define CONFIG_MAX_NUM_IOAPIC 1 +@@ -32,15 +32,14 @@ + #define CONFIG_SEL4UTILS_STACK_SIZE 655360 + #define CONFIG_HAVE_LIB_SEL4_ALLOCMAN 1 + #define CONFIG_FASTPATH 1 +-#define CONFIG_X2APIC 1 + #define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_OBJS_SZ 0 +-#define CONFIG_HAVE_TIMER 1 + #define CONFIG_SEL4UTILS_CSPACE_SIZE_BITS 18 + #define CONFIG_DOMAIN_SCHEDULE "" + #define CONFIG_LIB_SEL4 1 + #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 +@@ -49,7 +48,6 @@ + #define CONFIG_HAVE_LIB_SEL4_VSPACE 1 + #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 +@@ -66,7 +64,9 @@ + #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_XAPIC 1 ++#define CONFIG_SYSENTER 1 ++#define CONFIG_FSGSBASE_GDT 1 + #define CONFIG_HAVE_LIB_SEL4_PLAT_SUPPORT 1 + #define CONFIG_USER_EXTRA_CFLAGS "-D_XOPEN_SOURCE=700" + #define CONFIG_HAVE_FPU 1 +@@ -76,6 +76,7 @@ + #define CONFIG_SUPPORT_PCID 1 + #define CONFIG_HAVE_LIB_PLATSUPPORT 1 + #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 +@@ -92,9 +93,6 @@ + #define CONFIG_KERNEL_EXTRA_CPPFLAGS "" + #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_KERNEL_STACK_BITS 12 diff --git a/repos/base-sel4/patches/dev_mem.patch b/repos/base-sel4/patches/dev_mem.patch deleted file mode 100644 index f43ed94a3..000000000 --- a/repos/base-sel4/patches/dev_mem.patch +++ /dev/null @@ -1,150 +0,0 @@ ---- src/kernel/sel4/include/plat/pc99/plat/machine.h -+++ src/kernel/sel4/include/plat/pc99/plat/machine.h -@@ -51,8 +51,11 @@ typedef enum _irq_t { - #define BIOS_PADDR_END 0x100000 - - #define BIOS_PADDR_VIDEO_RAM_START 0x000A0000 -+#define BIOS_PADDR_VIDEO_RAM_END 0x000B0000 - /* The text mode framebuffer exists part way into the video ram region */ - #define BIOS_PADDR_VIDEO_RAM_TEXT_MODE_START 0x000B8000 - #define BIOS_PADDR_IVDEO_RAM_END 0x000C0000 -+#define BIOS_PADDR_VIDEO_BIOS_START 0x000C0000 -+#define BIOS_PADDR_VIDEO_BIOS_END 0x000CF000 - - #endif ---- src/kernel/sel4/src/arch/x86/kernel/boot_sys.c -+++ src/kernel/sel4/src/arch/x86/kernel/boot_sys.c -@@ -286,6 +286,40 @@ add_mem_p_regs(p_region_t reg) - } - - /* -+ * Checks whether there are overlaps between the area _reg_ and _trim_area_. -+ * If there are overlaps, trim the _trim_area_ and if there is some rest left, -+ * store it in _tail_. -+ */ -+static BOOT_CODE void -+trim_region(p_region_t *reg, p_region_t *trim_area, p_region_t *tail, bool_t add) -+{ -+ bool_t const inside_start = trim_area->start <= reg->start && reg->start < trim_area->end; -+ bool_t const inside_end = trim_area->start < reg->end && reg->end <= trim_area->end; -+ -+ if (reg->start >= reg->end) -+ return; -+ -+ /* trim BIOS area if we detect overlaps */ -+ if (!inside_start && !inside_end && -+ (reg->start <= trim_area->start && trim_area->start < reg->end)) -+ trim_area->start = trim_area->end; -+ else -+ if (inside_start && inside_end) { -+ tail->start = reg->end; -+ tail->end = trim_area->end; -+ trim_area->end = reg->start; -+ } else { -+ if (inside_start) -+ trim_area->end = reg->start; -+ if (inside_end) -+ trim_area->start = reg->end; -+ } -+ -+ if (add) -+ insert_dev_p_reg(*reg); -+} -+ -+/* - * the code relies that the GRUB provides correct information - * about the actual physical memory regions. - */ -@@ -295,9 +329,17 @@ parse_mem_map(uint32_t mmap_length, uint32_t mmap_addr) - multiboot_mmap_t *mmap = (multiboot_mmap_t *)((word_t)mmap_addr); - printf("Parsing GRUB physical memory map\n"); - -+ /* -+ * Legacy regions required by ACPI driver, VESA driver and graphic drivers -+ * (Intel) -+ */ -+ p_region_t legacy_area = { .start = BIOS_PADDR_VIDEO_RAM_START, .end = BIOS_PADDR_END }; -+ /* optimistic approach that the area splits at most only one time ;-( */ -+ p_region_t legacy_split = { .start = 0, .end = 0 }; -+ - while ((word_t)mmap < (word_t)(mmap_addr + mmap_length)) { -- uint64_t mem_start = mmap->base_addr; -- uint64_t mem_length = mmap->length; -+ uint64_t mem_start = mmap->base_addr & ~0xFFFUL; -+ uint64_t mem_length = (mmap->length + (mmap->base_addr & 0xFFFUL)) & ~0xFFFUL; - uint32_t type = mmap->type; - if (mem_start != (uint64_t)(word_t)mem_start) { - printf("\tPhysical memory region not addressable\n"); -@@ -308,9 +350,38 @@ parse_mem_map(uint32_t mmap_length, uint32_t mmap_addr) - mem_start, mem_start + mem_length - }); - } -+ if (type == MULTIBOOT_MMAP_RESERVED_TYPE || -+ type == MULTIBOOT_MMAP_ACPI_TYPE || -+ type == MULTIBOOT_MMAP_ACPI_NVS_TYPE) { -+ -+ p_region_t reg = { .start = mem_start, .end = mem_start + mem_length}; -+ p_region_t tail = { .start = 0, .end = 0 }; -+ -+ trim_region(®, &legacy_area, &tail, true); -+ if (tail.start < tail.end) { -+ assert(!(legacy_split.start < legacy_split.end)); -+ legacy_split = tail; -+ } -+ -+ tail.start = 0; tail.end = 0; -+ trim_region(®, &legacy_split, &tail, false); -+ if (tail.start < tail.end) { -+ assert(!(legacy_split.start < legacy_split.end)); -+ legacy_split = tail; -+ } -+ } - } - mmap++; - } -+ -+ /* first physical page - required by acpi drivers and vesa drivers */ -+ insert_dev_p_reg((p_region_t) { .start = 0, .end = 0x1000 }); -+ -+ /* legacy area - required by acpi drivers */ -+ if (legacy_area.start < legacy_area.end) { -+ insert_dev_p_reg(legacy_area); -+ insert_dev_p_reg(legacy_split); -+ } - } - - static BOOT_CODE bool_t -@@ -349,6 +420,9 @@ try_boot_sys( - /* copy CPU bootup code to lower memory */ - memcpy((void*)BOOT_NODE_PADDR, boot_cpu_start, boot_cpu_end - boot_cpu_start); - -+ /* Prepare for accepting device regions from here on */ -+ boot_state.dev_p_regs.count = 0; -+ - boot_state.mem_p_regs.count = 0; - if (mbi->flags & MULTIBOOT_INFO_MMAP_FLAG) { - parse_mem_map(mbi->mmap_length, mbi->mmap_addr); -@@ -378,9 +452,6 @@ try_boot_sys( - pic_disable(); - } - -- /* Prepare for accepting device regions from here on */ -- boot_state.dev_p_regs.count = 0; -- - /* get ACPI root table */ - acpi_rsdt = acpi_init(); - if (!acpi_rsdt) { ---- src/kernel/sel4/src/plat/pc99/machine/hardware.c -+++ src/kernel/sel4/src/plat/pc99/machine/hardware.c -@@ -26,11 +26,6 @@ void platAddDevices(void) - /* discover PCI devices and their regions */ - /* pci_scan() calls insert_dev_p_reg() for each device region */ - pci_scan(); -- /* Add the text mode (EGA) frame buffer. 1 frame is enough for the -- * standard 80x25 text mode. This whole thing is a bit of a hack */ -- insert_dev_p_reg( (p_region_t) { -- BIOS_PADDR_VIDEO_RAM_TEXT_MODE_START, BIOS_PADDR_VIDEO_RAM_TEXT_MODE_START + 0x1000 -- } ); - } - - /* ============================== interrupts/IRQs ============================== */ diff --git a/repos/base-sel4/patches/dev_mem_4k.patch b/repos/base-sel4/patches/dev_mem_4k.patch deleted file mode 100644 index e53bd0534..000000000 --- a/repos/base-sel4/patches/dev_mem_4k.patch +++ /dev/null @@ -1,11 +0,0 @@ ---- src/kernel/sel4/src/arch/x86/kernel/boot.c -+++ src/kernel/sel4/src/arch/x86/kernel/boot.c -@@ -83,7 +83,7 @@ create_device_frames( - /* use large frames if possible, otherwise use 4K frames */ - if (IS_ALIGNED(dev_reg.start, LARGE_PAGE_BITS) && - IS_ALIGNED(dev_reg.end, LARGE_PAGE_BITS)) { -- frame_size = X86_LargePage; -+ frame_size = X86_SmallPage; - } else { - frame_size = X86_SmallPage; - } diff --git a/repos/base-sel4/patches/noise.patch b/repos/base-sel4/patches/noise.patch index cdbb1f4d6..b943763e6 100644 --- a/repos/base-sel4/patches/noise.patch +++ b/repos/base-sel4/patches/noise.patch @@ -9,3 +9,43 @@ 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 diff --git a/repos/base-sel4/patches/root_cnode.patch b/repos/base-sel4/patches/root_cnode.patch index 81a5a07c0..9135d3adc 100644 --- a/repos/base-sel4/patches/root_cnode.patch +++ b/repos/base-sel4/patches/root_cnode.patch @@ -1,10 +1,10 @@ ---- src/kernel/sel4/include/plat/pc99/autoconf.h -+++ src/kernel/sel4/include/plat/pc99/autoconf.h +--- src/kernel/sel4/configs/pc99/autoconf.h ++++ src/kernel/sel4/configs/pc99/autoconf.h @@ -77,7 +77,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 16 +#define CONFIG_ROOT_CNODE_SIZE_BITS 18 #define CONFIG_NUM_PRIORITIES 256 #define CONFIG_TESTPRINTER_REGEX ".*" diff --git a/repos/base-sel4/patches/serial.patch b/repos/base-sel4/patches/serial.patch deleted file mode 100644 index 627dc757e..000000000 --- a/repos/base-sel4/patches/serial.patch +++ /dev/null @@ -1,24 +0,0 @@ ---- src/kernel/sel4/src/plat/pc99/machine/io.c -+++ src/kernel/sel4/src/plat/pc99/machine/io.c -@@ -18,7 +18,7 @@ - - void serial_init(uint16_t port) - { -- while (!(in8(port + 5) & 0x60)); /* wait until not busy */ -+ while (!(in8(port + 5) & 0x20)); /* wait until not busy */ - - out8(port + 1, 0x00); /* disable generating interrupts */ - out8(port + 3, 0x80); /* line control register: command: set divisor */ -@@ -43,10 +43,10 @@ void console_putchar(char c) - lock_acquire(&lock_debug); - - if (port > 0) { -- while (!(in8(port + 5) & 0x60)); -+ while (!(in8(port + 5) & 0x20)); - out8(port, c); - if (c == '\n') { -- while (!(in8(port + 5) & 0x60)); -+ while (!(in8(port + 5) & 0x20)); - out8(port, '\r'); - } - } diff --git a/repos/base-sel4/patches/syscall.patch b/repos/base-sel4/patches/syscall.patch deleted file mode 100644 index 40e911330..000000000 --- a/repos/base-sel4/patches/syscall.patch +++ /dev/null @@ -1,626 +0,0 @@ ---- src/kernel/sel4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h -+++ src/kernel/sel4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h -@@ -15,24 +15,69 @@ - #include - #include - -+#if defined(__pic__) -+ -+#define SEL4_REGS_SAVE "pushl %%ebx \n" -+#define SEL4_REGS_MOV "movl %%edx, %%ebx \n" -+#define SEL4_REGS_RESTORE "popl %%ebx \n" -+#define SEL4_REGS_RESTORE_EDX \ -+ "movl %%ebx, %%edx \n" \ -+ "popl %%ebx \n" -+ -+#define SEL4_REGS_OUT "+d" (dest) -+#define SEL4_REGS_OUT_IN(VAR) "+d" (VAR) -+#define SEL4_REGS_IN -+#define SEL4_REGS_OUT_VAR(VAR) \ -+ "=d" (VAR), -+#define SEL4_REGS_IN_VAR(VAR) \ -+ "d" (VAR) -+ -+#define SEL4_REGS_CLOBBER_EBX -+#define SEL4_REGS_CLOBBER_EDX -+#define SEL4_REGS_CLOBBER_COMMA_EDX -+ -+#else -+ -+#define SEL4_REGS_SAVE -+#define SEL4_REGS_MOV -+#define SEL4_REGS_RESTORE -+#define SEL4_REGS_RESTORE_EDX -+ -+#define SEL4_REGS_OUT -+#define SEL4_REGS_OUT_IN(VAR) "+b" (VAR) -+#define SEL4_REGS_IN "b" (dest), -+#define SEL4_REGS_OUT_VAR(VAR) \ -+ "=b" (VAR), -+#define SEL4_REGS_IN_VAR(VAR) \ -+ "b" (VAR) -+ -+#define SEL4_REGS_CLOBBER_EBX "%ebx", -+#define SEL4_REGS_CLOBBER_EDX "%edx" -+#define SEL4_REGS_CLOBBER_COMMA_EDX , "%edx" -+ -+#endif /* #if defined(__pic__) */ -+ - static inline void - seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) - { - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%ecx, %%ebp \n" - "movl %%esp, %%ecx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE - "popl %%ebp \n" -- : -+ : SEL4_REGS_OUT - : "a" (seL4_SysSend), -- "b" (dest), -+ SEL4_REGS_IN - "S" (msgInfo.words[0]), - "D" (seL4_GetMR(0)), - "c" (seL4_GetMR(1)) -- : "%edx" -+ : SEL4_REGS_CLOBBER_EDX - ); - } - -@@ -42,19 +87,22 @@ seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, - { - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%ecx, %%ebp \n" - "movl %%esp, %%ecx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE - "popl %%ebp \n" -- : -+ : SEL4_REGS_OUT - : "a" (seL4_SysSend), -- "b" (dest), -+ SEL4_REGS_IN - "S" (msgInfo.words[0]), - "D" (mr0 != seL4_Null ? *mr0 : 0), - "c" (mr1 != seL4_Null ? *mr1 : 0) -- : "%edx" -+ : SEL4_REGS_CLOBBER_EDX - ); - } - -@@ -63,19 +111,22 @@ seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) - { - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%ecx, %%ebp \n" - "movl %%esp, %%ecx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE - "popl %%ebp \n" -- : -+ : SEL4_REGS_OUT - : "a" (seL4_SysNBSend), -- "b" (dest), -+ SEL4_REGS_IN - "S" (msgInfo.words[0]), - "D" (seL4_GetMR(0)), - "c" (seL4_GetMR(1)) -- : "%edx" -+ : SEL4_REGS_CLOBBER_EDX - ); - } - -@@ -85,19 +136,22 @@ seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, - { - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%ecx, %%ebp \n" - "movl %%esp, %%ecx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE - "popl %%ebp \n" -- : -+ : SEL4_REGS_OUT - : "a" (seL4_SysNBSend), -- "b" (dest), -+ SEL4_REGS_IN - "S" (msgInfo.words[0]), - "D" (mr0 != seL4_Null ? *mr0 : 0), - "c" (mr1 != seL4_Null ? *mr1 : 0) -- : "%edx" -+ : SEL4_REGS_CLOBBER_EDX - ); - } - -@@ -106,18 +160,20 @@ seL4_Reply(seL4_MessageInfo_t msgInfo) - { - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%ecx, %%ebp \n" - "movl %%esp, %%ecx \n" - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE - "popl %%ebp \n" - : - : "a" (seL4_SysReply), - "S" (msgInfo.words[0]), - "D" (seL4_GetMR(0)), - "c" (seL4_GetMR(1)) -- : "%ebx", "%edx" -+ : SEL4_REGS_CLOBBER_EBX "%edx" - ); - } - -@@ -127,18 +183,20 @@ seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo, - { - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%ecx, %%ebp \n" - "movl %%esp, %%ecx \n" - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE - "popl %%ebp \n" - : - : "a" (seL4_SysReply), - "S" (msgInfo.words[0]), - "D" (mr0 != seL4_Null ? *mr0 : 0), - "c" (mr1 != seL4_Null ? *mr1 : 0) -- : "%ebx", "%edx" -+ : SEL4_REGS_CLOBBER_EBX "%edx" - ); - } - -@@ -147,16 +205,19 @@ seL4_Signal(seL4_CPtr dest) - { - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%esp, %%ecx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE - "popl %%ebp \n" -- : -+ : SEL4_REGS_OUT - : "a" (seL4_SysSend), -- "b" (dest), -+ SEL4_REGS_IN - "S" (seL4_MessageInfo_new(0, 0, 0, 0).words[0]) -- : "%ecx", "%edx" -+ : "%ecx" SEL4_REGS_CLOBBER_COMMA_EDX - ); - } - -@@ -170,20 +231,23 @@ seL4_Recv(seL4_CPtr src, seL4_Word* sender) - - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%esp, %%ecx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE_EDX - "movl %%ebp, %%ecx \n" - "popl %%ebp \n" - : -- "=b" (badge), -+ SEL4_REGS_OUT_VAR(badge) - "=S" (info.words[0]), - "=D" (mr0), - "=c" (mr1) - : "a" (seL4_SysRecv), -- "b" (src) -- : "%edx", "memory" -+ SEL4_REGS_IN_VAR(src) -+ : "memory" SEL4_REGS_CLOBBER_COMMA_EDX - ); - - seL4_SetMR(0, mr0); -@@ -207,20 +271,23 @@ seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender, - - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%esp, %%ecx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE_EDX - "movl %%ebp, %%ecx \n" - "popl %%ebp \n" - : -- "=b" (badge), -+ SEL4_REGS_OUT_VAR(badge) - "=S" (info.words[0]), - "=D" (msg0), - "=c" (msg1) - : "a" (seL4_SysRecv), -- "b" (src) -- : "%edx", "memory" -+ SEL4_REGS_IN_VAR(src) -+ : "memory" SEL4_REGS_CLOBBER_COMMA_EDX - ); - - if (mr0 != seL4_Null) { -@@ -247,20 +314,23 @@ seL4_NBRecv(seL4_CPtr src, seL4_Word* sender) - - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%esp, %%ecx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE_EDX - "movl %%ebp, %%ecx \n" - "popl %%ebp \n" - : -- "=b" (badge), -+ SEL4_REGS_OUT_VAR(badge) - "=S" (info.words[0]), - "=D" (mr0), - "=c" (mr1) - : "a" (seL4_SysNBRecv), -- "b" (src) -- : "%edx", "memory" -+ SEL4_REGS_IN_VAR(src) -+ : "memory" SEL4_REGS_CLOBBER_COMMA_EDX - ); - - seL4_SetMR(0, mr0); -@@ -282,24 +352,26 @@ seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) - - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%ecx, %%ebp \n" - "movl %%esp, %%ecx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE_EDX - "movl %%ebp, %%ecx \n" - "popl %%ebp \n" - : - "=S" (info.words[0]), - "=D" (mr0), - "=c" (mr1), -- "=b" (dest) /* dummy, tells GCC that ebx is clobbered */ -+ SEL4_REGS_OUT_IN(dest) - : "a" (seL4_SysCall), -- "b" (dest), - "S" (msgInfo.words[0]), - "D" (mr0), - "c" (mr1) -- : "%edx", "memory" -+ : "memory" SEL4_REGS_CLOBBER_COMMA_EDX - ); - - seL4_SetMR(0, mr0); -@@ -325,24 +397,26 @@ seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, - - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%ecx, %%ebp \n" - "movl %%esp, %%ecx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE_EDX - "movl %%ebp, %%ecx \n" - "popl %%ebp \n" - : - "=S" (info.words[0]), - "=D" (msg0), - "=c" (msg1), -- "=b" (dest) /* dummy, tells GCC that ebx is clobbered */ -+ SEL4_REGS_OUT_IN(dest) - : "a" (seL4_SysCall), -- "b" (dest), - "S" (msgInfo.words[0]), - "D" (msg0), - "c" (msg1) -- : "%edx", "memory" -+ : "memory" SEL4_REGS_CLOBBER_COMMA_EDX - ); - - if (mr0 != seL4_Null) { -@@ -365,24 +439,27 @@ seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender) - - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%ecx, %%ebp \n" - "movl %%esp, %%ecx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE_EDX - "movl %%ebp, %%ecx \n" - "popl %%ebp \n" - : -- "=b" (badge), -+ SEL4_REGS_OUT_VAR(badge) - "=S" (info.words[0]), - "=D" (mr0), - "=c" (mr1) - : "a" (seL4_SysReplyRecv), -- "b" (dest), -+ SEL4_REGS_IN_VAR(dest), - "S" (msgInfo.words[0]), - "D" (mr0), - "c" (mr1) -- : "%edx", "memory" -+ : "memory" SEL4_REGS_CLOBBER_COMMA_EDX - ); - - seL4_SetMR(0, mr0); -@@ -413,24 +490,27 @@ seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sen - - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%ecx, %%ebp \n" - "movl %%esp, %%ecx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE_EDX - "movl %%ebp, %%ecx \n" - "popl %%ebp \n" - : -- "=b" (badge), -+ SEL4_REGS_OUT_VAR(badge) - "=S" (info.words[0]), - "=D" (msg0), - "=c" (msg1) - : "a" (seL4_SysReplyRecv), -- "b" (dest), -+ SEL4_REGS_IN_VAR(dest), - "S" (msgInfo.words[0]), - "D" (msg0), - "c" (msg1) -- : "%edx", "memory" -+ : "memory" SEL4_REGS_CLOBBER_COMMA_EDX - ); - - if (mr0 != seL4_Null) { -@@ -452,14 +532,16 @@ seL4_Yield(void) - { - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%esp, %%ecx \n" - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE - "popl %%ebp \n" - : - : "a" (seL4_SysYield) -- : "%ebx", "%ecx", "%edx", "%esi", "%edi", "memory" -+ : SEL4_REGS_CLOBBER_EBX "%ecx", "%edx", "%esi", "%edi", "memory" - ); - } - -@@ -469,15 +551,17 @@ seL4_DebugPutChar(char c) - { - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%esp, %%ecx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE - "popl %%ebp \n" -- : -- : "a" (seL4_SysDebugPutChar), -- "b" (c) -- : "%ecx", "%edx", "%esi", "%edi", "memory" -+ : SEL4_REGS_OUT_IN(c) -+ : "a" (seL4_SysDebugPutChar) -+ : "%ecx", "%esi", "%edi", "memory" SEL4_REGS_CLOBBER_COMMA_EDX - ); - } - #endif -@@ -488,14 +572,16 @@ seL4_DebugHalt(void) - { - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%esp, %%ecx \n" - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE - "popl %%ebp \n" - : - : "a" (seL4_SysDebugHalt) -- : "%ebx", "%ecx", "%edx", "%esi", "%edi", "memory" -+ : SEL4_REGS_CLOBBER_EBX "%ecx", "%edx", "%esi", "%edi", "memory" - ); - } - #endif -@@ -506,14 +592,16 @@ seL4_DebugSnapshot(void) - { - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%esp, %%ecx \n" - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE - "popl %%ebp \n" - : - : "a" (seL4_SysDebugSnapshot) -- : "%ebx", "%ecx", "%edx", "%esi", "%edi", "memory" -+ : SEL4_REGS_CLOBBER_EBX "%ecx", "%edx", "%esi", "%edi", "memory" - ); - } - #endif -@@ -524,14 +612,17 @@ seL4_DebugCapIdentify(seL4_CPtr cap) - { - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%esp, %%ecx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE_EDX - "popl %%ebp \n" -- : "=b"(cap) -- : "a"(seL4_SysDebugCapIdentify), "b"(cap) -- : "%ecx", "%edx", "%esi", "%edi", "memory" -+ : SEL4_REGS_OUT_IN(cap) -+ : "a"(seL4_SysDebugCapIdentify) -+ : "%ecx", "%esi", "%edi", "memory" SEL4_REGS_CLOBBER_COMMA_EDX - ); - return (seL4_Uint32)cap; - } -@@ -546,14 +637,17 @@ seL4_DebugNameThread(seL4_CPtr tcb, const char *name) - - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%esp, %%ecx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE - "popl %%ebp \n" -- : -- : "a"(seL4_SysDebugNameThread), "b"(tcb) -- : "%ecx", "%edx", "%esi", "%edi", "memory" -+ : SEL4_REGS_OUT_IN(tcb) -+ : "a"(seL4_SysDebugNameThread) -+ : "%ecx", "%esi", "%edi", "memory" SEL4_REGS_CLOBBER_COMMA_EDX - ); - } - #endif -@@ -564,16 +658,19 @@ seL4_DebugRun(void (*userfn) (void *), void* userarg) - { - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%esp, %%ecx \n" -+ "movl %%edx, %%ebx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE - "popl %%ebp \n" -- : -+ : SEL4_REGS_OUT_IN(userfn) - : "a" (seL4_SysDebugRun), -- "b" (userfn), - "S" (userarg) -- : "%ecx", "%edx", "%edi", "memory" -+ : "%ecx", "%edi", "memory" SEL4_REGS_CLOBBER_COMMA_EDX - ); - } - #endif -@@ -600,16 +697,18 @@ seL4_BenchmarkDumpLog(seL4_Word start, seL4_Word size) - { - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%esp, %%ecx \n" -+ SEL4_REGS_MOV - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE_EDX - "popl %%ebp \n" -- : "=b" (start) -+ : SEL4_REGS_OUT_IN(start) - : "a" (seL4_SysBenchmarkDumpLog), -- "b" (start), - "S" (size) -- : "%ecx", "%edx", "%edi", "memory" -+ : "%ecx", "%edi", "memory" SEL4_REGS_CLOBBER_COMMA_EDX - ); - - return (seL4_Uint32) start; -@@ -622,14 +721,16 @@ seL4_BenchmarkLogSize(void) - seL4_Uint32 ret = 0; - asm volatile ( - "pushl %%ebp \n" -+ SEL4_REGS_SAVE - "movl %%esp, %%ecx \n" - "leal 1f, %%edx \n" - "1: \n" - "sysenter \n" -+ SEL4_REGS_RESTORE_EDX - "popl %%ebp \n" -- : "=b" (ret) -+ : SEL4_REGS_OUT_VAR(ret) - : "a" (seL4_SysBenchmarkLogSize) -- : "%ecx", "%edx", "%edi", "memory" -+ : "%ecx", "%edi", "memory" SEL4_REGS_CLOBBER_COMMA_EDX - ); - - return ret; -@@ -670,4 +771,20 @@ seL4_BenchmarkGetThreadUtilisation(seL4_Word tcp_cptr) - } - #endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */ - #endif /* CONFIG_ENABLE_BENCHMARKS */ -+ -+#undef SEL4_REGS_SAVE -+#undef SEL4_REGS_MOV -+#undef SEL4_REGS_RESTORE -+#undef SEL4_REGS_RESTORE_EDX -+ -+#undef SEL4_REGS_OUT -+#undef SEL4_REGS_OUT_IN -+#undef SEL4_REGS_IN -+#undef SEL4_REGS_OUT_VAR -+#undef SEL4_REGS_IN_VAR -+ -+#undef SEL4_REGS_CLOBBER_EBX -+#undef SEL4_REGS_CLOBBER_EDX -+#undef SEL4_REGS_CLOBBER_COMMA_EDX -+ - #endif diff --git a/repos/base-sel4/ports/sel4.hash b/repos/base-sel4/ports/sel4.hash index 2d137115c..7389a8268 100644 --- a/repos/base-sel4/ports/sel4.hash +++ b/repos/base-sel4/ports/sel4.hash @@ -1 +1 @@ -e8d740ed612452a8d81b992169f459191b3a3f0c +3d2fe27593d616ffd0afeeae8fe21119297da73e diff --git a/repos/base-sel4/ports/sel4.port b/repos/base-sel4/ports/sel4.port index 7c6873d1c..9e5f4f869 100644 --- a/repos/base-sel4/ports/sel4.port +++ b/repos/base-sel4/ports/sel4.port @@ -3,8 +3,10 @@ VERSION := git DOWNLOADS := sel4.git URL(sel4) := https://github.com/seL4/seL4.git -# master branch, version 3.2 -REV(sel4) := e70cd7613bb3aed71d3df58c72146cc44a60190e +# master branch, version 5.2 +REV(sel4) := 3695232f9603af60d56f97072082d90f30e98b0e DIR(sel4) := src/kernel/sel4 +$(call check_tool,python) + PATCHES := $(wildcard $(REP_DIR)/patches/*.patch) diff --git a/repos/base-sel4/src/core/capability_space.cc b/repos/base-sel4/src/core/capability_space.cc index a9ee552cd..e5a46b415 100644 --- a/repos/base-sel4/src/core/capability_space.cc +++ b/repos/base-sel4/src/core/capability_space.cc @@ -93,14 +93,14 @@ Capability_space::create_rpc_obj_cap(Native_capability ep_cap, /* mint endpoint capability into RPC object capability */ { - seL4_CNode const service = seL4_CapInitThreadCNode; - seL4_Word const dest_index = rpc_obj_sel.value(); - uint8_t const dest_depth = 32; - seL4_CNode const src_root = seL4_CapInitThreadCNode; - seL4_Word const src_index = ep_sel.value(); - uint8_t const src_depth = 32; - seL4_CapRights const rights = seL4_AllRights; - seL4_CapData_t const badge = seL4_CapData_Badge_new(rpc_obj_key.value()); + seL4_CNode const service = seL4_CapInitThreadCNode; + seL4_Word const dest_index = rpc_obj_sel.value(); + uint8_t const dest_depth = 32; + seL4_CNode const src_root = seL4_CapInitThreadCNode; + seL4_Word const src_index = ep_sel.value(); + uint8_t const src_depth = 32; + seL4_CapRights_t const rights = seL4_AllRights; + seL4_CapData_t const badge = seL4_CapData_Badge_new(rpc_obj_key.value()); int const ret = seL4_CNode_Mint(service, dest_index, diff --git a/repos/base-sel4/src/core/include/cnode.h b/repos/base-sel4/src/core/include/cnode.h index 2fb2394dc..47f04b160 100644 --- a/repos/base-sel4/src/core/include/cnode.h +++ b/repos/base-sel4/src/core/include/cnode.h @@ -48,13 +48,13 @@ class Genode::Cnode_base */ void copy(Cnode_base const &from, Index from_idx, Index to_idx) { - seL4_CNode const service = sel().value(); - seL4_Word const dest_index = to_idx.value(); - uint8_t const dest_depth = size_log2(); - seL4_CNode const src_root = from.sel().value(); - seL4_Word const src_index = from_idx.value(); - uint8_t const src_depth = from.size_log2(); - seL4_CapRights const rights = seL4_AllRights; + seL4_CNode const service = sel().value(); + seL4_Word const dest_index = to_idx.value(); + uint8_t const dest_depth = size_log2(); + seL4_CNode const src_root = from.sel().value(); + seL4_Word const src_index = from_idx.value(); + uint8_t const src_depth = from.size_log2(); + seL4_CapRights_t const rights = seL4_AllRights; int const ret = seL4_CNode_Copy(service, dest_index, dest_depth, src_root, src_index, src_depth, rights); @@ -71,14 +71,14 @@ class Genode::Cnode_base */ void mint(Cnode_base const &from, Index from_idx, Index to_idx) { - seL4_CNode const service = sel().value(); - seL4_Word const dest_index = to_idx.value(); - uint8_t const dest_depth = size_log2(); - seL4_CNode const src_root = from.sel().value(); - seL4_Word const src_index = from_idx.value(); - uint8_t const src_depth = from.size_log2(); - seL4_CapRights const rights = seL4_AllRights; - seL4_CapData_t const badge = seL4_CapData_Badge_new(to_idx.value()); + seL4_CNode const service = sel().value(); + seL4_Word const dest_index = to_idx.value(); + uint8_t const dest_depth = size_log2(); + seL4_CNode const src_root = from.sel().value(); + seL4_Word const src_index = from_idx.value(); + uint8_t const src_depth = from.size_log2(); + seL4_CapRights_t const rights = seL4_AllRights; + seL4_CapData_t const badge = seL4_CapData_Badge_new(to_idx.value()); int const ret = seL4_CNode_Mint(service, dest_index, dest_depth, src_root, src_index, src_depth, @@ -159,7 +159,9 @@ class Genode::Cnode : public Cnode_base, Noncopyable : Cnode_base(dst_idx, size_log2) { - _phys = create(phys_alloc, parent_sel, dst_idx, size_log2); + _phys = Untyped_memory::alloc_page(phys_alloc); + seL4_Untyped const service = Untyped_memory::untyped_sel(_phys).value(); + create(service, parent_sel, dst_idx, size_log2); } /** @@ -181,7 +183,8 @@ class Genode::Cnode : public Cnode_base, Noncopyable : Cnode_base(dst_idx, size_log2) { - create(untyped_pool, parent_sel, dst_idx, size_log2); + seL4_Untyped sel = untyped_pool.alloc(Cnode_kobj::SIZE_LOG2 + size_log2); + create(sel, parent_sel, dst_idx, size_log2); } void destruct(Range_allocator &phys_alloc, bool revoke = false) diff --git a/repos/base-sel4/src/core/include/initial_untyped_pool.h b/repos/base-sel4/src/core/include/initial_untyped_pool.h index 8c2f3f8f1..49de85c24 100644 --- a/repos/base-sel4/src/core/include/initial_untyped_pool.h +++ b/repos/base-sel4/src/core/include/initial_untyped_pool.h @@ -51,10 +51,12 @@ class Genode::Initial_untyped_pool unsigned const index = sel - sel4_boot_info().untyped.start; /* original size of untyped memory range */ - size_t const size = 1UL << sel4_boot_info().untypedSizeBitsList[index]; + size_t const size = 1UL << sel4_boot_info().untypedList[index].sizeBits; /* physical address of the begin of the untyped memory range */ - addr_t const phys = sel4_boot_info().untypedPaddrList[index]; + addr_t const phys = sel4_boot_info().untypedList[index].paddr; + + bool const device = sel4_boot_info().untypedList[index].isDevice; /* offset to the unused part of the untyped memory range */ addr_t &free_offset; @@ -124,6 +126,9 @@ class Genode::Initial_untyped_pool * a range that is able to host a kernel object of 'size'. */ for_each_range([&] (Range &range) { + /* ignore device memory */ + if (range.device) + return; /* calculate free index after allocation */ addr_t const new_free_offset = _align_offset(range, size_log2); @@ -223,6 +228,12 @@ class Genode::Initial_untyped_pool "returned ", ret); return; } + + /* convert device memory directly into page frames */ + if (range.device) { + size_t const num_pages = batch_size >> get_page_size_log2(); + Untyped_memory::convert_to_page_frames(phys_addr, num_pages); + } } }); } diff --git a/repos/base-sel4/src/core/include/kernel_object.h b/repos/base-sel4/src/core/include/kernel_object.h index ffb770168..20a974e96 100644 --- a/repos/base-sel4/src/core/include/kernel_object.h +++ b/repos/base-sel4/src/core/include/kernel_object.h @@ -80,17 +80,14 @@ namespace Genode { /** - * Create kernel object from untyped memory + * Create kernel object * * \param KOBJ kernel-object description - * \param phys_alloc allocator for untyped memory + * \param service cap to untyped memory * \param dst_cnode_sel CNode selector where to store the cap pointing to * the new kernel object * \param dst_idx designated index of cap selector within 'dst_cnode' - * \param size_log2 size of kernel object in bits, only needed for - * variable-sized objects like CNodes - * - * \return physical address of created kernel object + * \param size_log2 size of kernel object in bits * * \throw Phys_alloc_failed * \throw Retype_untyped_failed @@ -98,19 +95,13 @@ namespace Genode { * The kernel-object description is a policy type that contains enum * definitions for 'SEL4_TYPE' and 'SIZE_LOG2', and a static function * 'name' that returns the type name as a char const pointer. - * - * XXX to be removed */ template - static addr_t create(Range_allocator &phys_alloc, - Cap_sel dst_cnode_sel, - Cnode_index dst_idx, - size_t size_log2 = 0) + static void create(seL4_Untyped const service, + Cap_sel const dst_cnode_sel, + Cnode_index dst_idx, + size_t size_log2 = 0) { - /* allocate physical page */ - addr_t phys_addr = Untyped_memory::alloc_page(phys_alloc); - - seL4_Untyped const service = Untyped_memory::untyped_sel(phys_addr).value(); int const type = KOBJ::SEL4_TYPE; int const size_bits = size_log2; seL4_CNode const root = dst_cnode_sel.value(); @@ -133,59 +124,6 @@ namespace Genode { "returned ", ret); throw Retype_untyped_failed(); } - - return phys_addr; - } - - - /** - * Create kernel object from initial untyped memory pool - * - * \param KOBJ kernel-object description - * \param untyped_pool initial untyped memory pool - * \param dst_cnode_sel CNode selector where to store the cap pointing to - * the new kernel object - * \param dst_idx designated index of cap selector within 'dst_cnode' - * \param size_log2 size of kernel object in bits, only needed for - * variable-sized objects like CNodes - * - * \throw Initial_untyped_pool::Initial_untyped_pool_exhausted - * \throw Retype_untyped_failed - * - * The kernel-object description is a policy type that contains enum - * definitions for 'SEL4_TYPE' and 'SIZE_LOG2', and a static function - * 'name' that returns the type name as a char const pointer. - */ - template - static void create(Initial_untyped_pool &untyped_pool, - Cap_sel dst_cnode_sel, - Cnode_index dst_idx, - size_t size_log2 = 0) - { - unsigned const sel = untyped_pool.alloc(KOBJ::SIZE_LOG2 + size_log2); - - seL4_Untyped const service = sel; - int const type = KOBJ::SEL4_TYPE; - int const size_bits = size_log2; - seL4_CNode const root = dst_cnode_sel.value(); - int const node_index = 0; - int const node_depth = 0; - int const node_offset = dst_idx.value(); - int const num_objects = 1; - - int const ret = seL4_Untyped_Retype(service, - type, - size_bits, - root, - node_index, - node_depth, - node_offset, - num_objects); - - if (ret != 0) { - error("seL4_Untyped_Retype (", KOBJ::name(), ") returned ", ret); - throw Retype_untyped_failed(); - } } }; diff --git a/repos/base-sel4/src/core/include/page_table_registry.h b/repos/base-sel4/src/core/include/page_table_registry.h index c0709a37c..a42b0b539 100644 --- a/repos/base-sel4/src/core/include/page_table_registry.h +++ b/repos/base-sel4/src/core/include/page_table_registry.h @@ -200,7 +200,7 @@ class Genode::Page_table_registry if (_page_table_base(pt->addr) == _page_table_base(addr)) return *pt; } - warning(__func__, ": page-table lookup failed"); + warning(__func__, ": page-table lookup failed ", Hex(addr)); throw Lookup_failed(); } diff --git a/repos/base-sel4/src/core/include/platform.h b/repos/base-sel4/src/core/include/platform.h index eadf0eb33..641d9a612 100644 --- a/repos/base-sel4/src/core/include/platform.h +++ b/repos/base-sel4/src/core/include/platform.h @@ -41,13 +41,18 @@ class Genode::Platform : public Platform_generic */ Phys_allocator _unused_phys_alloc; + /* + * Allocator for tracking unused virtual addresses, which are not + * backed by page tables. + */ + Phys_allocator _unused_virt_alloc; + void _init_unused_phys_alloc(); bool const _init_unused_phys_alloc_done; Rom_fs _rom_fs; /* ROM file system */ - - /** + /* * Virtual address range usable by non-core processes */ addr_t _vm_base; diff --git a/repos/base-sel4/src/core/include/thread_sel4.h b/repos/base-sel4/src/core/include/thread_sel4.h index df6c386b3..a0c0492ae 100644 --- a/repos/base-sel4/src/core/include/thread_sel4.h +++ b/repos/base-sel4/src/core/include/thread_sel4.h @@ -54,7 +54,7 @@ namespace Genode { void Genode::Thread_info::init(addr_t const utcb_virt_addr) { - Platform &platform = *platform_specific(); + Platform &platform = *platform_specific(); Range_allocator &phys_alloc = *platform.ram_alloc(); /* create IPC buffer of one page */ @@ -62,16 +62,31 @@ void Genode::Thread_info::init(addr_t const utcb_virt_addr) Untyped_memory::convert_to_page_frames(ipc_buffer_phys, 1); /* allocate TCB within core's CNode */ - tcb_sel = platform.core_sel_alloc().alloc(); - create(phys_alloc, platform.core_cnode().sel(), tcb_sel); + { + addr_t const phys_addr = Untyped_memory::alloc_page(phys_alloc); + seL4_Untyped const service = Untyped_memory::untyped_sel(phys_addr).value(); + + tcb_sel = platform.core_sel_alloc().alloc(); + create(service, platform.core_cnode().sel(), tcb_sel); + } /* allocate synchronous endpoint within core's CNode */ - ep_sel = platform.core_sel_alloc().alloc(); - create(phys_alloc, platform.core_cnode().sel(), ep_sel); + { + addr_t const phys_addr = Untyped_memory::alloc_page(phys_alloc); + seL4_Untyped const service = Untyped_memory::untyped_sel(phys_addr).value(); + + ep_sel = platform.core_sel_alloc().alloc(); + create(service, platform.core_cnode().sel(), ep_sel); + } /* allocate asynchronous object within core's CSpace */ - lock_sel = platform.core_sel_alloc().alloc(); - create(phys_alloc, platform.core_cnode().sel(), lock_sel); + { + addr_t const phys_addr = Untyped_memory::alloc_page(phys_alloc); + seL4_Untyped const service = Untyped_memory::untyped_sel(phys_addr).value(); + + lock_sel = platform.core_sel_alloc().alloc(); + create(service, platform.core_cnode().sel(), lock_sel); + } /* assign IPC buffer to thread */ { @@ -85,6 +100,7 @@ void Genode::Thread_info::init(addr_t const utcb_virt_addr) /* set scheduling priority */ enum { PRIORITY_MAX = 0xff }; + seL4_TCB_SetMCPriority(tcb_sel.value(), PRIORITY_MAX); seL4_TCB_SetPriority(tcb_sel.value(), PRIORITY_MAX); } @@ -122,7 +138,7 @@ void Genode::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp) regs.eip = ip; regs.esp = sp; - regs.gs = IPCBUF_GDT_SELECTOR; + regs.fs = IPCBUF_GDT_SELECTOR; int const ret = seL4_TCB_WriteRegisters(tcb_sel.value(), false, 0, num_regs, ®s); ASSERT(ret == 0); diff --git a/repos/base-sel4/src/core/include/vm_space.h b/repos/base-sel4/src/core/include/vm_space.h index 51a44af78..cd687d38c 100644 --- a/repos/base-sel4/src/core/include/vm_space.h +++ b/repos/base-sel4/src/core/include/vm_space.h @@ -191,7 +191,7 @@ class Genode::Vm_space seL4_X86_Page const service = _idx_to_sel(pte_idx); seL4_X86_PageDirectory const pd = _pd_sel.value(); seL4_Word const vaddr = to_virt; - seL4_CapRights const rights = seL4_AllRights; + seL4_CapRights_t const rights = seL4_AllRights; seL4_X86_VMAttributes const attr = seL4_X86_Default_VMAttributes; int const ret = seL4_X86_Page_Map(service, pd, vaddr, rights, attr); @@ -210,6 +210,11 @@ class Genode::Vm_space /* delete copy of the mapping's page-frame selector */ _page_table_registry.apply(virt, [&] (unsigned idx) { + seL4_X86_Page const service = _idx_to_sel(idx); + long err = seL4_X86_Page_Unmap(service); + if (err) + error("unmap ", Hex(virt), " failed, idx=", idx, " res=", err); + _leaf_cnode(idx).remove(_leaf_cnode_entry(idx)); _sel_alloc.free(idx); @@ -238,27 +243,18 @@ class Genode::Vm_space * * \throw Alloc_page_table_failed */ - void _alloc_and_map_page_table(addr_t to_virt, bool core_vm) + void _alloc_and_map_page_table(addr_t to_virt) { /* allocate page-table selector */ unsigned const pt_idx = _sel_alloc.alloc(); - /* XXX account the consumed backing store */ - try { - /* XXX evil manual unlock/lock pattern */ - if (core_vm) - _lock.unlock(); - - create(_phys_alloc, + addr_t const phys_addr = Untyped_memory::alloc_page(_phys_alloc); + seL4_Untyped const service = Untyped_memory::untyped_sel(phys_addr).value(); + create(service, _leaf_cnode(pt_idx).sel(), _leaf_cnode_entry(pt_idx)); - - if (core_vm) - _lock.lock(); } catch (...) { - if (core_vm) - _lock.lock(); throw Alloc_page_table_failed(); } @@ -357,22 +353,11 @@ class Genode::Vm_space for (size_t i = 0; i < num_pages; i++) { off_t const offset = i << get_page_size_log2(); - /* check if we need to add a page table to core's VM space */ - if (!_page_table_registry.has_page_table_at(to_virt + offset)) - _alloc_and_map_page_table(to_virt + offset, !flush_support); - if (_map_page(from_phys + offset, to_virt + offset, flush_support)) continue; - /* XXX - Why this quirk is necessary - shouldn't happen ?!? */ - - error("mapping failed - retry once ", Hex(from_phys + offset), + error("mapping failed ", Hex(from_phys + offset), " -> ", Hex(to_virt + offset)); - - _page_table_registry.forget_page_table_entry(to_virt + offset); - _alloc_and_map_page_table(to_virt + offset, !flush_support); - - _map_page(from_phys + offset, to_virt + offset, flush_support); } } @@ -385,6 +370,18 @@ class Genode::Vm_space _unmap_page(virt + offset); } } + + void alloc_page_tables(addr_t const start, addr_t const size) + { + Lock::Guard guard(_lock); + + addr_t virt = trunc_page(start); + for (; virt < start + size; virt += get_page_size()) { + if (!_page_table_registry.has_page_table_at(virt)) { + _alloc_and_map_page_table(virt); + } + } + } }; #endif /* _CORE__INCLUDE__VM_SPACE_H_ */ diff --git a/repos/base-sel4/src/core/irq_session_component.cc b/repos/base-sel4/src/core/irq_session_component.cc index ddf19eeef..78be43194 100644 --- a/repos/base-sel4/src/core/irq_session_component.cc +++ b/repos/base-sel4/src/core/irq_session_component.cc @@ -31,8 +31,13 @@ bool Irq_object::associate(Irq_session::Trigger const irq_trigger, Platform &platform = *platform_specific(); Range_allocator &phys_alloc = *platform.ram_alloc(); - create(phys_alloc, platform.core_cnode().sel(), - _kernel_notify_sel); + { + addr_t const phys_addr = Untyped_memory::alloc_page(phys_alloc); + seL4_Untyped const service = Untyped_memory::untyped_sel(phys_addr).value(); + + create(service, platform.core_cnode().sel(), + _kernel_notify_sel); + } enum { IRQ_EDGE = 0, IRQ_LEVEL = 1 }; enum { IRQ_HIGH = 0, IRQ_LOW = 1 }; diff --git a/repos/base-sel4/src/core/pager.cc b/repos/base-sel4/src/core/pager.cc index 5fc300f26..d574c0052 100644 --- a/repos/base-sel4/src/core/pager.cc +++ b/repos/base-sel4/src/core/pager.cc @@ -37,7 +37,7 @@ struct Fault_info : ip(seL4_GetMR(0)), pf(seL4_GetMR(1)), - write(seL4_Fault_isWriteFault(seL4_GetMR(3))) + write(seL4_GetMR(3) & 0x2) { } }; diff --git a/repos/base-sel4/src/core/platform.cc b/repos/base-sel4/src/core/platform.cc index afd301394..a1f8c84c7 100644 --- a/repos/base-sel4/src/core/platform.cc +++ b/repos/base-sel4/src/core/platform.cc @@ -80,7 +80,7 @@ void Platform::_init_unused_phys_alloc() static inline void init_sel4_ipc_buffer() { - asm volatile ("movl %0, %%gs" :: "r"(IPCBUF_GDT_SELECTOR) : "memory"); + asm volatile ("movl %0, %%fs" :: "r"(IPCBUF_GDT_SELECTOR) : "memory"); } @@ -93,9 +93,18 @@ void Platform::_init_allocators() * XXX allocate intermediate CNodes for organizing the untyped pages here */ - /* register remaining untyped memory to physical memory allocator */ + /* register remaining untyped memory to physical or iomem memory allocator */ auto add_phys_range = [&] (Initial_untyped_pool::Range const &range) { + if (range.device) { + addr_t const phys_addr = trunc_page(range.phys); + size_t const phys_size = round_page((range.phys - phys_addr) + range.size); + + _io_mem_alloc.add_range(phys_addr, phys_size); + _unused_phys_alloc.remove_range(phys_addr, phys_size); + return; + } + addr_t const page_aligned_offset = align_addr(range.free_offset, get_page_size_log2()); @@ -118,66 +127,43 @@ void Platform::_init_allocators() * '_initial_untyped_pool' because the pool is empty. */ - /* move device memory regions to phys cnode */ - seL4_BootInfo const &bi = sel4_boot_info(); - Cnode_base const initial_cspace(Cap_sel(seL4_CapInitThreadCNode), 32); - - for (unsigned region = 0; region < bi.numDeviceRegions; region++) { - size_t const frame_size = 1UL << bi.deviceRegions[region].frameSizeBits; - if (frame_size != 4096) { - error("unsupported device memory frame size of ", Hex(frame_size)); - class Unsupported_dev_memory_framesize{}; - throw Unsupported_dev_memory_framesize(); - } - - for (uint64_t sel = bi.deviceRegions[region].frames.start, - phys_addr = bi.deviceRegions[region].basePaddr; - sel < bi.deviceRegions[region].frames.end; - sel++, phys_addr += frame_size) { - - _io_mem_alloc.add_range(phys_addr, frame_size); - _unused_phys_alloc.remove_range(phys_addr, frame_size); - - addr_t const dst_frame = phys_addr >> get_page_size_log2(); - _phys_cnode.move(initial_cspace, Cnode_index(sel), - Cnode_index(dst_frame)); - } - } - - /* core's virtual memory */ - _core_mem_alloc.virt_alloc()->add_range(_vm_base, _vm_size); + /* core's maximum virtual memory area */ + _unused_virt_alloc.add_range(_vm_base, _vm_size); /* remove core image from core's virtual address allocator */ + addr_t const modules_start = reinterpret_cast(&_boot_modules_binaries_begin); + addr_t const core_virt_beg = trunc_page((addr_t)&_prog_img_beg), + core_virt_end = round_page((addr_t)&_prog_img_end); + addr_t const image_elf_size = core_virt_end - core_virt_beg; - /* - * XXX Why do we need to skip a page after the end of core? - * When allocating a PTE immediately after _prog_img_end, the - * kernel would complain "Mapping already present" on the - * attempt to map a page frame. - */ - addr_t const core_virt_beg = trunc_page((addr_t)&_prog_img_beg), - core_virt_end = round_page((addr_t)&_prog_img_end) - + 4096; - size_t const core_size = core_virt_end - core_virt_beg; + _unused_virt_alloc.remove_range(core_virt_beg, image_elf_size); + _core_mem_alloc.virt_alloc()->add_range(modules_start, core_virt_end - modules_start); - _core_mem_alloc.virt_alloc()->remove_range(core_virt_beg, core_size); + /* remove initial IPC buffer from core's virtual address allocator */ + seL4_BootInfo const &bi = sel4_boot_info(); + addr_t const core_ipc_buffer = reinterpret_cast(bi.ipcBuffer); + addr_t const core_ipc_bsize = 4096; + _unused_virt_alloc.remove_range(core_ipc_buffer, core_ipc_bsize); - if (verbose_boot_info) { - log("core image:"); - log(" virtual address range ", - Hex_range(core_virt_beg, core_virt_end - core_virt_beg), " " - "size=", Hex(core_size)); - } - - /* preserve sel4 boot info page in core's virtual address space */ - addr_t const sel4_boot_info_page = reinterpret_cast(&bi); - _core_mem_alloc.virt_alloc()->remove_range(sel4_boot_info_page, 0x1000); - if (sel4_boot_info_page != core_virt_end) - warning("unexpected core binary layout"); + /* remove sel4_boot_info page from core's virtual address allocator */ + addr_t const boot_info_page = reinterpret_cast(&bi); + addr_t const boot_info_size = 4096 + bi.extraLen; + _unused_virt_alloc.remove_range(boot_info_page, boot_info_size); /* preserve stack area in core's virtual address space */ - _core_mem_alloc.virt_alloc()->remove_range(stack_area_virtual_base(), - stack_area_virtual_size()); + _unused_virt_alloc.remove_range(stack_area_virtual_base(), + stack_area_virtual_size()); + + if (verbose_boot_info) { + typedef Hex_range Hex_range; + log("virtual adress layout of core:"); + log(" overall ", Hex_range(_vm_base, _vm_size)); + log(" core image ", Hex_range(core_virt_beg, image_elf_size)); + log(" ipc buffer ", Hex_range(core_ipc_buffer, core_ipc_bsize)); + log(" boot_info ", Hex_range(boot_info_page, boot_info_size)); + log(" stack area ", Hex_range(stack_area_virtual_base(), + stack_area_virtual_size())); + } } @@ -214,15 +200,26 @@ void Platform::_switch_to_core_cspace() for (unsigned sel = bi.untyped.start; sel < bi.untyped.end; sel++) _core_cnode.move(initial_cspace, Cnode_index(sel)); - /* move the device memory selectors to core's CNode */ - for (unsigned region = 0; region < bi.numDeviceRegions; region++) { - for (unsigned sel = bi.deviceRegions[region].frames.start; - sel < bi.deviceRegions[region].frames.end; sel++) - _core_cnode.move(initial_cspace, Cnode_index(sel)); - } + /* move selectors of core image */ + addr_t const modules_start = reinterpret_cast(&_boot_modules_binaries_begin); + addr_t const modules_end = reinterpret_cast(&_boot_modules_binaries_end); + addr_t virt_addr = (addr_t)(&_prog_img_beg); - for (unsigned sel = bi.userImageFrames.start; sel < bi.userImageFrames.end; sel++) - _core_cnode.copy(initial_cspace, Cnode_index(sel)); + for (unsigned sel = bi.userImageFrames.start; + sel < bi.userImageFrames.end; + sel++, virt_addr += get_page_size()) { + + /* remove mapping to boot modules, no access required within core */ + if (modules_start <= virt_addr && virt_addr < modules_end) { + seL4_X86_Page const service = sel; + long err = seL4_X86_Page_Unmap(service); + if (err) + error("unmapping boot modules ", Hex(virt_addr)); + } + + /* insert cap for core image */ + _core_cnode.move(initial_cspace, Cnode_index(sel)); + } /* copy statically created CNode selectors to core's CNode */ _core_cnode.copy(initial_cspace, Cnode_index(Core_cspace::top_cnode_sel())); @@ -294,15 +291,14 @@ void Platform::_init_core_page_table_registry() * Register initial page frames */ virt_addr = (addr_t)(&_prog_img_beg); - for (unsigned sel = bi.userImageFrames.start; sel < bi.userImageFrames.end; sel++) { - + 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); - - virt_addr += get_page_size(); } } @@ -367,7 +363,7 @@ void Platform::_init_rom_modules() */ Cnode_base const initial_cspace(Cap_sel(seL4_CapInitThreadCNode), 32); for (unsigned i = 0; i < module_num_frames; i++) - _phys_cnode.copy(initial_cspace, Cnode_index(module_frame_sel + i), + _phys_cnode.move(initial_cspace, Cnode_index(module_frame_sel + i), Cnode_index(dst_frame + i)); log("boot module '", (char const *)header->name, "' " @@ -392,6 +388,7 @@ Platform::Platform() _io_mem_alloc(core_mem_alloc()), _io_port_alloc(core_mem_alloc()), _irq_alloc(core_mem_alloc()), _unused_phys_alloc(core_mem_alloc()), + _unused_virt_alloc(core_mem_alloc()), _init_unused_phys_alloc_done((_init_unused_phys_alloc(), true)), _vm_base(0x2000), /* 2nd page is used as IPC buffer of main thread */ _vm_size(3*1024*1024*1024UL - _vm_base), /* use the lower 3GiB */ @@ -414,7 +411,11 @@ Platform::Platform() Cap_sel lock_sel (INITIAL_SEL_LOCK); Cap_sel core_sel = _core_sel_alloc.alloc(); - create(*ram_alloc(), core_cnode().sel(), core_sel); + { + addr_t const phys_addr = Untyped_memory::alloc_page(*ram_alloc()); + seL4_Untyped const service = Untyped_memory::untyped_sel(phys_addr).value(); + create(service, core_cnode().sel(), core_sel); + } /* mint a copy of the notification object with badge of lock_sel */ _core_cnode.mint(_core_cnode, core_sel, lock_sel); @@ -426,17 +427,35 @@ Platform::Platform() ASSERT(sender == INITIAL_SEL_LOCK); + /* back stack area with page tables */ + enum { MAX_CORE_THREADS = 32 }; + _core_vm_space.alloc_page_tables(stack_area_virtual_base(), + stack_virtual_size() * MAX_CORE_THREADS); + + /* add some minor virtual region for dynamic usage by core */ + addr_t const virt_size = 32 * 1024 * 1024; + void * virt_ptr = nullptr; + if (_unused_virt_alloc.alloc(virt_size, &virt_ptr)) { + + addr_t const virt_addr = (addr_t)virt_ptr; + + /* add to available virtual region of core */ + _core_mem_alloc.virt_alloc()->add_range(virt_addr, virt_size); + + /* back region by page tables */ + _core_vm_space.alloc_page_tables(virt_addr, virt_size); + } + /* I/O port allocator (only meaningful for x86) */ _io_port_alloc.add_range(0, 0x10000); /* * Log statistics about allocator initialization */ - log("VM area at ", Hex_range(_vm_base, _vm_size)); - if (verbose_boot_info) { log(":phys_alloc: ", *_core_mem_alloc.phys_alloc()); log(":unused_phys_alloc:", _unused_phys_alloc); + log(":unused_virt_alloc:", _unused_virt_alloc); log(":virt_alloc: ", *_core_mem_alloc.virt_alloc()); log(":io_mem_alloc: ", _io_mem_alloc); } diff --git a/repos/base-sel4/src/core/platform_pd.cc b/repos/base-sel4/src/core/platform_pd.cc index 262e27c36..a1372edca 100644 --- a/repos/base-sel4/src/core/platform_pd.cc +++ b/repos/base-sel4/src/core/platform_pd.cc @@ -87,11 +87,10 @@ 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. */ - if (thread->_utcb) { - _vm_space.map(thread->_info.ipc_buffer_phys, thread->_utcb, 1); - } else { - _vm_space.map(thread->_info.ipc_buffer_phys, thread->INITIAL_IPC_BUFFER_VIRT, 1); - } + addr_t const utcb = (thread->_utcb) ? thread->_utcb : thread->INITIAL_IPC_BUFFER_VIRT; + + _vm_space.alloc_page_tables(utcb, get_page_size()); + _vm_space.map(thread->_info.ipc_buffer_phys, utcb, 1); return true; } @@ -132,10 +131,12 @@ void Platform_pd::assign_parent(Native_capability parent) addr_t Platform_pd::_init_page_directory() { - addr_t const phys = - create(*platform()->ram_alloc(), - platform_specific()->core_cnode().sel(), - _page_directory_sel); + addr_t const phys_addr = Untyped_memory::alloc_page(*platform()->ram_alloc()); + seL4_Untyped const service = Untyped_memory::untyped_sel(phys_addr).value(); + + create(service, + platform_specific()->core_cnode().sel(), + _page_directory_sel); int const ret = seL4_X86_ASIDPool_Assign(platform_specific()->asid_pool().value(), _page_directory_sel.value()); @@ -143,7 +144,7 @@ addr_t Platform_pd::_init_page_directory() if (ret != seL4_NoError) error("seL4_X86_ASIDPool_Assign returned ", ret); - return phys; + return phys_addr; } @@ -165,6 +166,7 @@ void Platform_pd::free_sel(Cap_sel sel) void Platform_pd::install_mapping(Mapping const &mapping) { + _vm_space.alloc_page_tables(mapping.to_virt(), mapping.num_pages() * get_page_size()); _vm_space.map(mapping.from_phys(), mapping.to_virt(), mapping.num_pages()); } diff --git a/repos/base-sel4/src/core/signal_source_component.cc b/repos/base-sel4/src/core/signal_source_component.cc index a9c8805ca..49e343220 100644 --- a/repos/base-sel4/src/core/signal_source_component.cc +++ b/repos/base-sel4/src/core/signal_source_component.cc @@ -73,12 +73,15 @@ Signal_source_component::Signal_source_component(Rpc_entrypoint *ep) _entrypoint(ep), _finalizer(*this), _finalizer_cap(_entrypoint->manage(&_finalizer)) { - Platform &platform = *platform_specific(); + Platform &platform = *platform_specific(); Range_allocator &phys_alloc = *platform.ram_alloc(); + addr_t const phys_addr = Untyped_memory::alloc_page(phys_alloc); + seL4_Untyped const service = Untyped_memory::untyped_sel(phys_addr).value(); + /* allocate notification object within core's CNode */ Cap_sel ny_sel = platform.core_sel_alloc().alloc(); - create(phys_alloc, platform.core_cnode().sel(), ny_sel); + create(service, platform.core_cnode().sel(), ny_sel); _notify = Capability_space::create_notification_cap(ny_sel); } diff --git a/repos/libports/run/acpica.run b/repos/libports/run/acpica.run index b54837d27..249195586 100644 --- a/repos/libports/run/acpica.run +++ b/repos/libports/run/acpica.run @@ -2,7 +2,8 @@ assert_spec acpi if { ![have_spec hw] && - ![have_spec nova] + ![have_spec nova] && + ![have_spec sel4] } { puts "Platform is unsupported." exit 0 diff --git a/repos/os/run/rom_filter.run b/repos/os/run/rom_filter.run index c770c7a28..2d25e4887 100644 --- a/repos/os/run/rom_filter.run +++ b/repos/os/run/rom_filter.run @@ -119,7 +119,7 @@ build_boot_image $boot_modules append qemu_args " -nographic " -run_genode_until {.*finished.*\n} 20 +run_genode_until {.*xray: change \(finished\).*\n} 20 # pay only attention to the output of the rom_logger grep_output {^\[init -> rom_logger\] .+} diff --git a/tool/run/boot_dir/sel4 b/tool/run/boot_dir/sel4 index ff126fc38..b6b433712 100644 --- a/tool/run/boot_dir/sel4 +++ b/tool/run/boot_dir/sel4 @@ -2,6 +2,8 @@ proc binary_name_ld_lib_so { } { return "ld-sel4.lib.so" } proc binary_name_core_o { } { return "core-sel4.o" } proc binary_name_timer { } { return "pit_timer_drv" } +proc kernel_files { } { return sel4 } + proc run_boot_string { } { return "\n\rStarting node #0" } proc core_link_address { } { return "0x02000000" }