sel4: add x86_64 support

Issue #2451

repos/base-sel4/lib/mk/core-sel4.inc

@@ -13,8 +13,6 @@ SRC_CC      += \
                pd_assign_pci.cc \
                io_mem_session_component.cc \
                io_mem_session_support.cc \
-               io_port_session_component.cc \
-               io_port_session_support.cc \
                thread_start.cc \
                platform_thread.cc \
                platform_pd.cc \
@@ -55,8 +53,6 @@ vpath pd_upgrade_ram_quota.cc      $(GEN_CORE_DIR)
 vpath region_map_component.cc      $(GEN_CORE_DIR)
 vpath io_mem_session_component.cc  $(GEN_CORE_DIR)
 vpath io_mem_session_support.cc    $(GEN_CORE_DIR)
-vpath io_port_session_component.cc $(GEN_CORE_DIR)/spec/x86
-vpath platform_services.cc         $(GEN_CORE_DIR)/spec/x86
 vpath trace_session_component.cc   $(GEN_CORE_DIR)
 vpath signal_transmitter_proxy.cc  $(GEN_CORE_DIR)
 vpath signal_receiver.cc           $(GEN_CORE_DIR)

repos/base-sel4/lib/mk/spec/x86_32/core-sel4.mk

@@ -0,0 +1,10 @@
+SRC_CC += $(addprefix spec/x86_32/, boot_info.cc thread.cc platform.cc \
+                                    platform_pd.cc vm_space.cc)
+
+SRC_CC += io_port_session_component.cc
+SRC_CC += io_port_session_support.cc
+
+include $(REP_DIR)/lib/mk/core-sel4.inc
+
+vpath io_port_session_component.cc $(GEN_CORE_DIR)/spec/x86
+vpath platform_services.cc         $(GEN_CORE_DIR)/spec/x86

repos/base-sel4/lib/mk/spec/x86_32/kernel-sel4.mk

@@ -11,18 +11,9 @@ else
 all:
 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 \
+	          BOARD=ia32 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 $(AVOID_CALLS_TO_MEMMOVE)" \
-	          $(addprefix CFLAGS+=,$(CC_MARCH)) \
 	          SOURCE_ROOT=$(SEL4_DIR) -f$(SEL4_DIR)/Makefile
 

repos/base-sel4/lib/mk/spec/x86_32/startup-sel4.mk

@@ -7,6 +7,4 @@ INC_DIR += $(REP_DIR)/src/include $(BASE_DIR)/src/include
 
 LIBS += syscall-sel4
 
-include $(BASE_DIR)/lib/mk/startup.inc
+include $(BASE_DIR)/lib/mk/spec/x86_32/startup.inc
-
-vpath crt0.s $(BASE_DIR)/src/lib/startup/spec/x86_32

repos/base-sel4/lib/mk/spec/x86_32/syscall-sel4.mk

@@ -1,138 +1,10 @@
-#
+PLAT := pc99
-# Create prerequisites for building Genode for seL4
+ARCH := x86
-#
-# Prior building Genode programs for seL4, the kernel bindings needed are
-# symlinked to the build directory.
-#
 
-#
+SEL4_ARCH := ia32
-# We do this also in the first build stage to ensure that the kernel
+PLAT_BOARD := /$(SEL4_ARCH)
-# port, if missing, is added to the missing-ports list of this stage.
+SEL4_WORDBITS := 32
-#
-LIBSEL4_DIR := $(call select_from_ports,sel4)/src/kernel/sel4/libsel4
-LIBSEL4_AUTO:= $(call select_from_ports,sel4)/src/kernel/sel4/configs/pc99
 
-#
+ARCH_INCLUDES := exIPC.h
-# Execute the rules in this file only at the second build stage when we know
-# about the complete build settings, e.g., the 'CROSS_DEV_PREFIX'.
-#
-ifeq ($(called_from_lib_mk),yes)
 
-#
+include $(REP_DIR)/lib/mk/syscall-sel4.inc
-# Make seL4 kernel API headers available to the Genode build system
-#
-# We have to create symbolic links of the content of seL4's 'include/sel4' and
-# 'include_arch/<arch>/sel4' directories into our local build directory.
-#
-
-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 \
-                 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 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)
-
-#
-# Plain symlinks to existing headers
-#
-include/sel4/sel4_arch/%.h: $(LIBSEL4_DIR)/sel4_arch_include/ia32/sel4/sel4_arch/%.h
-	$(VERBOSE)mkdir -p $(dir $@)
-	$(VERBOSE)ln -sf $< $@
-
-include/sel4/arch/%.h: $(LIBSEL4_DIR)/arch_include/x86/sel4/arch/%.h
-	$(VERBOSE)mkdir -p $(dir $@)
-	$(VERBOSE)ln -sf $< $@
-
-include/sel4/autoconf.h: $(LIBSEL4_AUTO)/autoconf.h
-	$(VERBOSE)mkdir -p $(dir $@)
-	$(VERBOSE)ln -sf $< $@
-
-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/%.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: 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/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 \
-	                 --xml $< --libsel4_header $@
-
-include/sel4/invocation.h: $(LIBSEL4_DIR)/include/interfaces/sel4.xml
-	$(MSG_CONVERT)$(notdir $@)
-	$(VERBOSE)mkdir -p $(dir $@)
-	$(VERBOSE)python $(LIBSEL4_DIR)/tools/invocation_header_gen.py \
-	                 --xml $< --libsel4 --dest $@
-
-include/sel4/sel4_arch/invocation.h: $(LIBSEL4_DIR)/sel4_arch_include/ia32/interfaces/sel4arch.xml
-	$(MSG_CONVERT)$(notdir $@)
-	$(VERBOSE)mkdir -p $(dir $@)
-	$(VERBOSE)python $(LIBSEL4_DIR)/tools/invocation_header_gen.py \
-	                 --xml $< --libsel4 --sel4_arch --dest $@
-
-include/sel4/arch/invocation.h: $(LIBSEL4_DIR)/arch_include/x86/interfaces/sel4arch.xml
-	$(MSG_CONVERT)arch/$(notdir $@)
-	$(VERBOSE)mkdir -p $(dir $@)
-	$(VERBOSE)python $(LIBSEL4_DIR)/tools/invocation_header_gen.py \
-	                 --xml $< --libsel4 --arch --dest $@
-
-SEL4_CLIENT_H_SRC := $(LIBSEL4_DIR)/sel4_arch_include/ia32/interfaces/sel4arch.xml \
-                     $(LIBSEL4_DIR)/arch_include/x86/interfaces/sel4arch.xml \
-                     $(LIBSEL4_DIR)/include/interfaces/sel4.xml
-
-include/interfaces/sel4_client.h: $(SEL4_CLIENT_H_SRC)
-	$(MSG_CONVERT)$(notdir $@)
-	$(VERBOSE)mkdir -p $(dir $@)
-	$(VERBOSE)python $(LIBSEL4_DIR)/tools/syscall_stub_gen.py \
-	                 --buffer -a ia32 --word-size 32 -o $@ $(SEL4_CLIENT_H_SRC)
-
-endif

repos/base-sel4/lib/mk/spec/x86_64/core-sel4.mk

@@ -0,0 +1,10 @@
+SRC_CC += $(addprefix spec/x86_64/, boot_info.cc thread.cc platform.cc \
+                                    platform_pd.cc vm_space.cc)
+
+SRC_CC += io_port_session_component.cc
+SRC_CC += io_port_session_support.cc
+
+include $(REP_DIR)/lib/mk/core-sel4.inc
+
+vpath io_port_session_component.cc $(GEN_CORE_DIR)/spec/x86
+vpath platform_services.cc         $(GEN_CORE_DIR)/spec/x86

repos/base-sel4/lib/mk/spec/x86_64/kernel-sel4.mk

@@ -0,0 +1,19 @@
+SEL4_DIR := $(call select_from_ports,sel4)/src/kernel/sel4
+
+#
+# Execute the kernel build only at the second build stage when we know
+# about the complete build settings (e.g., the 'CROSS_DEV_PREFIX') and the
+# current working directory is the library location.
+#
+ifeq ($(called_from_lib_mk),yes)
+all: build_kernel
+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
+

repos/base-sel4/lib/mk/spec/x86_64/ld-sel4.mk

@@ -0,0 +1,3 @@
+BASE_LIBS += base-sel4-common base-sel4
+
+include $(BASE_DIR)/lib/mk/spec/x86_64/ld-platform.inc

repos/base-sel4/lib/mk/spec/x86_64/startup-sel4.mk

@@ -0,0 +1,10 @@
+#
+# Make the includes of src/base/include/ available to the startup lib. This is
+# needed because the seL4-specific src/platform/_main_parent_cap.h as included
+# by the startup lib depends on base/internal/capability_space_sel4.h.
+#
+INC_DIR += $(REP_DIR)/src/include $(BASE_DIR)/src/include
+
+LIBS += syscall-sel4
+
+include $(BASE_DIR)/lib/mk/spec/x86_64/startup.inc

repos/base-sel4/lib/mk/spec/x86_64/syscall-sel4.mk

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

repos/base-sel4/lib/mk/syscall-sel4.inc

@@ -0,0 +1,138 @@
+#
+# Create prerequisites for building Genode for seL4
+#
+# Prior building Genode programs for seL4, the kernel bindings needed are
+# symlinked to the build directory.
+#
+
+#
+# We do this also in the first build stage to ensure that the kernel
+# 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
+# about the complete build settings, e.g., the 'CROSS_DEV_PREFIX'.
+#
+ifeq ($(called_from_lib_mk),yes)
+
+#
+# Make seL4 kernel API headers available to the Genode build system
+#
+# We have to create symbolic links of the content of seL4's 'include/sel4' and
+# 'include_arch/<arch>/sel4' directories into our local build directory.
+#
+
+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 \
+                 pfIPC.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 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)
+
+#
+# Plain symlinks to existing headers
+#
+include/sel4/sel4_arch/%.h: $(LIBSEL4_DIR)/sel4_arch_include/$(SEL4_ARCH)/sel4/sel4_arch/%.h
+	$(VERBOSE)mkdir -p $(dir $@)
+	$(VERBOSE)ln -sf $< $@
+
+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
+	$(VERBOSE)mkdir -p $(dir $@)
+	$(VERBOSE)ln -sf $< $@
+
+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/$(PLAT)/sel4/plat/api/%.h
+	$(VERBOSE)mkdir -p $(dir $@)
+	$(VERBOSE)ln -sf $< $@
+
+#
+# Generated headers
+#
+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/$(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/types_gen.h: include/sel4/types_$(SEL4_WORDBITS).pbf
+	$(MSG_CONVERT)$(notdir $@)
+	$(VERBOSE)mkdir -p $(dir $@)
+	$(VERBOSE)python $(LIBSEL4_DIR)/tools/bitfield_gen.py \
+	                 --environment libsel4 "$<" $@
+
+include/sel4/shared_types_gen.h: include/sel4/shared_types_$(SEL4_WORDBITS).pbf
+	$(MSG_CONVERT)$(notdir $@)
+	$(VERBOSE)mkdir -p $(dir $@)
+	$(VERBOSE)python $(LIBSEL4_DIR)/tools/bitfield_gen.py \
+	                 --environment libsel4 "$<" $@
+
+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 \
+	                 --xml $< --libsel4_header $@
+
+include/sel4/invocation.h: $(LIBSEL4_DIR)/include/interfaces/sel4.xml
+	$(MSG_CONVERT)$(notdir $@)
+	$(VERBOSE)mkdir -p $(dir $@)
+	$(VERBOSE)python $(LIBSEL4_DIR)/tools/invocation_header_gen.py \
+	                 --xml $< --libsel4 --dest $@
+
+include/sel4/sel4_arch/invocation.h: $(LIBSEL4_DIR)/sel4_arch_include/$(SEL4_ARCH)/interfaces/sel4arch.xml
+	$(MSG_CONVERT)$(notdir $@)
+	$(VERBOSE)mkdir -p $(dir $@)
+	$(VERBOSE)python $(LIBSEL4_DIR)/tools/invocation_header_gen.py \
+	                 --xml $< --libsel4 --sel4_arch --dest $@
+
+include/sel4/arch/invocation.h: $(LIBSEL4_DIR)/arch_include/$(ARCH)/interfaces/sel4arch.xml
+	$(MSG_CONVERT)arch/$(notdir $@)
+	$(VERBOSE)mkdir -p $(dir $@)
+	$(VERBOSE)python $(LIBSEL4_DIR)/tools/invocation_header_gen.py \
+	                 --xml $< --libsel4 --arch --dest $@
+
+SEL4_CLIENT_H_SRC := $(LIBSEL4_DIR)/sel4_arch_include/$(SEL4_ARCH)/interfaces/sel4arch.xml \
+                     $(LIBSEL4_DIR)/arch_include/$(ARCH)/interfaces/sel4arch.xml \
+                     $(LIBSEL4_DIR)/include/interfaces/sel4.xml
+
+include/interfaces/sel4_client.h: $(SEL4_CLIENT_H_SRC)
+	$(MSG_CONVERT)$(notdir $@)
+	$(VERBOSE)mkdir -p $(dir $@)
+	$(VERBOSE)python $(LIBSEL4_DIR)/tools/syscall_stub_gen.py \
+	                 --buffer -a $(SEL4_ARCH) --word-size $(SEL4_WORDBITS) -o $@ $(SEL4_CLIENT_H_SRC)
+
+endif

repos/base-sel4/patches/autoconf_32.config

@@ -1,5 +1,5 @@
---- src/kernel/sel4/configs/pc99/autoconf.h
+--- src/kernel/sel4/configs/pc99/ia32/autoconf.h
-+++ src/kernel/sel4/configs/pc99/autoconf.h
++++ src/kernel/sel4/configs/pc99/ia32/autoconf.h
 @@ -24,7 +24,8 @@
  #define CONFIG_HAVE_LIBC 1
  #define CONFIG_USER_COMPILER ""

repos/base-sel4/patches/autoconf_64.config

@@ -0,0 +1,51 @@
+--- src/kernel/sel4/configs/pc99/x86_64/autoconf.h
++++ src/kernel/sel4/configs/pc99/x86_64/autoconf.h
+@@ -25,6 +25,7 @@
+ #define CONFIG_USER_COMPILER ""
+ #define CONFIG_LIB_SEL4_PLAT_SUPPORT 1
+ #define CONFIG_WORD_SIZE 64
++#define CONFIG_ARCH_X86_GENERIC 1
+ #define CONFIG_ARCH_X86 1
+ #define CONFIG_APP_TESTS 1
+ #define CONFIG_MAX_NUM_IOAPIC 1
+@@ -32,7 +33,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
+@@ -41,6 +42,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
+@@ -66,14 +68,13 @@
+ #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 1
+ #define CONFIG_HAVE_LIB_UTILS 1
+@@ -93,7 +94,6 @@
+ #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

repos/base-sel4/patches/config.patch

@@ -0,0 +1,24 @@
+--- 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
+@@ -22,7 +22,7 @@
+ 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

repos/base-sel4/patches/noise.patch

@@ -49,3 +49,32 @@
  
  #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

repos/base-sel4/ports/sel4.hash

@@ -1 +1 @@
-3d2fe27593d616ffd0afeeae8fe21119297da73e
+3858de13ad9db6b4fa5e21c8a246180aec74571c

repos/base-sel4/ports/sel4.port

@@ -10,3 +10,12 @@ DIR(sel4) := src/kernel/sel4
 $(call check_tool,python)
 
 PATCHES   := $(wildcard $(REP_DIR)/patches/*.patch)
+
+# 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)patch -p0 <$(REP_DIR)/patches/autoconf_32.config
+	$(VERBOSE)patch -p0 <$(REP_DIR)/patches/autoconf_64.config

repos/base-sel4/src/core/include/initial_untyped_pool.h

@@ -85,8 +85,6 @@ class Genode::Initial_untyped_pool
 			return aligned_free_offset + (1 << size_log2);
 		}
 
-	public:
-
 		/**
 		 * Apply functor to each untyped memory range
 		 *
@@ -102,6 +100,7 @@ class Genode::Initial_untyped_pool
 			}
 		}
 
+	public:
 
 		/**
 		 * Return selector of untyped memory range where the allocation of
@@ -174,9 +173,14 @@ class Genode::Initial_untyped_pool
 		}
 
 		/**
-		 * Convert remainder of the initial untyped memory into untyped pages
+		 * Convert (remainder) of the initial untyped memory into untyped
+		 * objects of size_log2 and up to a maximum as specified by max_memory
 		 */
-		void turn_remainder_into_untyped_pages()
+		template <typename FUNC>
+		void turn_into_untyped_object(addr_t const node_index,
+		                              FUNC   const & func,
+		                              addr_t const size_log2 = get_page_size_log2(),
+		                              addr_t max_memory = 0UL - 0x1000UL)
 		{
 			for_each_range([&] (Range &range) {
 
@@ -189,39 +193,47 @@ class Genode::Initial_untyped_pool
 				for (;;) {
 
 					addr_t const page_aligned_free_offset =
-						align_addr(range.free_offset, get_page_size_log2());
+						align_addr(range.free_offset, size_log2);
 
 					/* back out if no further page can be allocated */
-					if (page_aligned_free_offset + get_page_size() > range.size)
+					if (page_aligned_free_offset + (1UL << size_log2) > range.size)
+						return;
+
+					if (!max_memory)
 						return;
 
 					size_t const remaining_size    = range.size - page_aligned_free_offset;
 					size_t const retype_size_limit = get_page_size()*256;
-					size_t const batch_size        = min(remaining_size, retype_size_limit);
+					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 / get_page_size();
+					size_t const num_pages = batch_size / (1UL << size_log2);
 
 					seL4_Untyped const service     = range.sel;
-					int          const type        = seL4_UntypedObject;
+					addr_t       const type        = seL4_UntypedObject;
-					int          const size_bits   = get_page_size_log2();
+					addr_t       const size_bits   = size_log2;
 					seL4_CNode   const root        = Core_cspace::top_cnode_sel();
-					int          const node_index  = Core_cspace::TOP_CNODE_UNTYPED_IDX;
+					addr_t       const node_depth  = Core_cspace::NUM_TOP_SEL_LOG2;
-					int          const node_depth  = Core_cspace::NUM_TOP_SEL_LOG2;
+					addr_t       const node_offset = phys_addr >> size_log2;
-					int          const node_offset = phys_addr >> get_page_size_log2();
+					addr_t       const num_objects = num_pages;
-					int          const num_objects = num_pages;
 
-					int const ret = seL4_Untyped_Retype(service,
+					/* XXX skip memory because of limited untyped cnode range */
-					                                    type,
+					if (node_offset >= (1UL << (32 - get_page_size_log2()))) {
-					                                    size_bits,
+						Genode::warning(range.device ? "device" : "      ", " memory in range ", Hex_range<addr_t>(range.phys, range.size), " is unavailable (due to limited untyped cnode range)");
-					                                    root,
+						return;
-					                                    node_index,
+					}
-					                                    node_depth,
+
-					                                    node_offset,
+					long const ret = seL4_Untyped_Retype(service,
-					                                    num_objects);
+					                                     type,
+					                                     size_bits,
+					                                     root,
+					                                     node_index,
+					                                     node_depth,
+					                                     node_offset,
+					                                     num_objects);
 
 					if (ret != 0) {
 						error(__func__, ": seL4_Untyped_Retype (untyped) "
@@ -229,11 +241,17 @@ class Genode::Initial_untyped_pool
 						return;
 					}
 
+					/* track memory left to be converted */
+					max_memory -= batch_size;
+
 					/* 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);
 					}
+
+					/* invoke callback about the range */
+					func(phys_addr, num_pages << size_log2, range.device);
 				}
 			});
 		}

repos/base-sel4/src/core/include/kernel_object.h

@@ -57,25 +57,10 @@ namespace Genode {
 
 	struct Cnode_kobj
 	{
-		enum { SEL4_TYPE = seL4_CapTableObject, SIZE_LOG2 = 4 };
+		enum { SEL4_TYPE = seL4_CapTableObject, SIZE_LOG2 = (CONFIG_WORD_SIZE == 32) ? 4 : 5 };
 		static char const *name() { return "cnode"; }
 	};
 
-
-	struct Page_table_kobj
-	{
-		enum { SEL4_TYPE = seL4_X86_PageTableObject, SIZE_LOG2 = 12 };
-		static char const *name() { return "page table"; }
-	};
-
-
-	struct Page_directory_kobj
-	{
-		enum { SEL4_TYPE = seL4_X86_PageDirectoryObject, SIZE_LOG2 = 12 };
-		static char const *name() { return "page directory"; }
-	};
-
-
 	struct Retype_untyped_failed : Genode::Exception { };
 
 

repos/base-sel4/src/core/include/map_local.h

@@ -27,15 +27,20 @@ namespace Genode {
 	 * \param from_phys  physical source address
 	 * \param to_virt    core-local destination address
 	 * \param num_pages  number of pages to map
+	 * \param platform   pointer to platform object (to avoid deadlocks during
+	 *                   early Platform() construction caused by nested calls
+	 *                   of platform_specific())
 	 *
 	 * \return true on success
 	 */
-	inline bool map_local(addr_t from_phys, addr_t to_virt, size_t num_pages)
+	inline bool map_local(addr_t from_phys, addr_t to_virt, size_t num_pages,
+	                      Platform * platform = nullptr)
 	{
 		enum { DONT_FLUSH = false };
 		try {
-			platform_specific()->core_vm_space().map(from_phys, to_virt,
+			platform = platform ? platform : platform_specific();
-			                                         num_pages, DONT_FLUSH);
+			platform->core_vm_space().map(from_phys, to_virt, num_pages,
+			                              DONT_FLUSH);
 		} catch (Page_table_registry::Mapping_cache_full) {
 			return false;
 		}

repos/base-sel4/src/core/include/page_table_registry.h

@@ -15,9 +15,11 @@
 #define _CORE__INCLUDE__PAGE_TABLE_REGISTRY_H_
 
 /* Genode includes */
-#include <util/list.h>
 #include <base/exception.h>
+#include <base/heap.h>
 #include <base/log.h>
+#include <base/tslab.h>
+#include <util/avl_tree.h>
 
 /* core includes */
 #include <util.h>
@@ -25,183 +27,170 @@
 
 namespace Genode { class Page_table_registry; }
 
-
 class Genode::Page_table_registry
 {
 	public:
 
-		class Lookup_failed : Exception { };
 		class Mapping_cache_full : Exception { };
 
 	private:
 
-		/*
+		enum Level { FRAME, PAGE_TABLE, LEVEL2, LEVEL3 };
-		 * XXX use AVL tree (with virtual address as key) instead of list
-		 */
 
-		class Page_table : public List<Page_table>::Element
+		class Frame : public Avl_node<Frame>
-		{
-			public:
-
-				struct Entry : List<Entry>::Element
-				{
-					addr_t   const addr;
-					unsigned const sel;
-
-					Entry(addr_t addr, unsigned sel) : addr(addr), sel(sel) { }
-				};
-
-				addr_t const addr;
-
-			private:
-
-				List<Entry> _entries;
-
-				static addr_t _page_frame_base(addr_t addr)
-				{
-					return addr & get_page_mask();
-				}
-
-				bool _entry_exists(addr_t addr) const
-				{
-					for (Entry const *e = _entries.first(); e; e = e->next()) {
-						if (_page_frame_base(e->addr) == _page_frame_base(addr))
-							return true;
-					}
-					return false;
-				}
-
-			public:
-
-				class Lookup_failed : Exception { };
-
-				Page_table(addr_t addr) : addr(addr) { }
-
-				Entry *first() { return _entries.first(); }
-
-				Entry &lookup(addr_t addr)
-				{
-					for (Entry *e = _entries.first(); e; e = e->next()) {
-						if (_page_frame_base(e->addr) == _page_frame_base(addr))
-							return *e;
-					}
-					throw Lookup_failed();
-				}
-
-				void insert_entry(Allocator &entry_alloc, addr_t addr, unsigned sel)
-				{
-					if (_entry_exists(addr)) {
-						warning("trying to insert page frame for ", Hex(addr), " twice");
-						return;
-					}
-
-					try {
-						_entries.insert(new (entry_alloc) Entry(addr, sel));
-					} catch (Genode::Allocator::Out_of_memory) {
-						throw Mapping_cache_full();
-					}
-				}
-
-				void remove_entry(Allocator &entry_alloc, addr_t addr)
-				{
-					try {
-						Entry &entry = lookup(addr);
-						_entries.remove(&entry);
-						destroy(entry_alloc, &entry);
-					} catch (Lookup_failed) { }
-				}
-
-				void flush_all(Allocator &entry_alloc)
-				{
-					for (; Entry *entry = _entries.first();) {
-						_entries.remove(entry);
-						destroy(entry_alloc, entry);
-					}
-				}
-		};
-
-		/**
-		 * Allocator operating on a static memory pool
-		 *
-		 * \param ELEM  element type
-		 * \param MAX   maximum number of elements
-		 *
-		 * The size of a single ELEM must be a multiple of sizeof(long).
-		 */
-		template <typename ELEM, size_t MAX>
-		class Static_allocator : public Allocator
 		{
 			private:
 
-				Bit_allocator<MAX> _used;
+				addr_t  const _vaddr;
+				Cap_sel const _sel;
 
-				struct Elem_space
+				Frame *_lookup(addr_t vaddr)
 				{
-					long space[sizeof(ELEM)/sizeof(long)];
+					if (vaddr == _vaddr) return this;
-				};
 
-				Elem_space _elements[MAX];
+					Frame *e = Avl_node<Frame>::child(vaddr > _vaddr);
+
+					return e ? e->_lookup(vaddr) : 0;
+				}
+
+				static addr_t _base(addr_t const vaddr, unsigned const log2base)
+				{
+					addr_t const size = 1UL << log2base;
+					return vaddr & ~(size - 1);
+				}
 
 			public:
 
-				class Alloc_failed { };
+				Frame(addr_t const vaddr, Cap_sel const sel, unsigned log2base)
+				:
+					_vaddr(_base(vaddr, log2base)), _sel(sel)
+				{ }
 
-				bool alloc(size_t size, void **out_addr) override
+				Cap_sel const sel() const { return _sel; }
+				addr_t  const vaddr() const { return _vaddr; }
+
+				static Frame * lookup(Avl_tree<Frame> &tree,
+				                      addr_t const vaddr,
+				                      unsigned const log2base)
 				{
-					*out_addr = nullptr;
+					Frame * element = tree.first();
+					if (!element)
+						return nullptr;
 
-					if (size > sizeof(Elem_space)) {
+					addr_t const align_addr = _base(vaddr, log2base);
-						error("unexpected allocation size of ", size);
+					return element->_lookup(align_addr);
-						return false;
-					}
-
-					try {
-						*out_addr = &_elements[_used.alloc()]; }
-					catch (typename Bit_allocator<MAX>::Out_of_indices) {
-						return false; }
-
-					return true;
 				}
 
-				size_t overhead(size_t) const override { return 0; }
+				bool higher(Frame const *other) const {
-
+					return other->_vaddr > _vaddr; }
-				void free(void *ptr, size_t) override
-				{
-					Elem_space *elem = reinterpret_cast<Elem_space *>(ptr);
-					unsigned const index = elem - &_elements[0];
-					_used.free(index);
-				}
-
-				bool need_size_for_free() const { return false; }
 		};
 
-		Static_allocator<Page_table, 128>         _page_table_alloc;
+		class Table : public Avl_node<Table>
-		Static_allocator<Page_table::Entry, 3 * 1024> _page_table_entry_alloc;
-
-		List<Page_table> _page_tables;
-
-		static addr_t _page_table_base(addr_t addr)
 		{
-			return addr & ~(4*1024*1024 - 1);
+			private:
+
+				addr_t  const _vaddr;
+				addr_t  const _paddr;
+				Cap_sel const _sel;
+
+				Table *_lookup(addr_t vaddr)
+				{
+					if (vaddr == _vaddr) return this;
+
+					Table *e = Avl_node<Table>::child(vaddr > _vaddr);
+
+					return e ? e->_lookup(vaddr) : 0;
+				}
+
+				static addr_t _base(addr_t const vaddr, unsigned const log2base)
+				{
+					addr_t const size = 1UL << log2base;
+					return vaddr & ~(size - 1);
+				}
+
+			public:
+
+				Table(addr_t const vaddr, addr_t const paddr,
+				     Cap_sel const sel, unsigned log2base)
+				:
+					_vaddr(_base(vaddr, log2base)), _paddr(paddr), _sel(sel)
+				{ }
+
+				Cap_sel const sel()   const { return _sel; }
+				addr_t  const vaddr() const { return _vaddr; }
+				addr_t  const paddr() const { return _paddr; }
+
+				static Table * lookup(Avl_tree<Table> &tree,
+				                     addr_t const vaddr,
+				                     unsigned const log2base)
+				{
+					Table * element = tree.first();
+					if (!element)
+						return nullptr;
+
+					addr_t const align_addr = _base(vaddr, log2base);
+					return element->_lookup(align_addr);
+				}
+
+				bool higher(Table const *other) const {
+					return other->_vaddr > _vaddr; }
+		};
+
+		enum {
+			LEVEL_0 = 12, /* 4K Page */
+		};
+
+		static constexpr size_t SLAB_BLOCK_SIZE = get_page_size() - Sliced_heap::meta_data_size();
+		Tslab<Frame, SLAB_BLOCK_SIZE> _alloc_frames;
+		uint8_t _initial_sb_frame[SLAB_BLOCK_SIZE];
+
+		Tslab<Table, SLAB_BLOCK_SIZE> _alloc_high;
+		uint8_t _initial_sb_high[SLAB_BLOCK_SIZE];
+
+		Avl_tree<Frame> _frames;
+		Avl_tree<Table> _level1;
+		Avl_tree<Table> _level2;
+		Avl_tree<Table> _level3;
+
+		void _insert(addr_t const vaddr, Cap_sel const sel, Level const level,
+		             addr_t const paddr, unsigned const level_log2_size)
+		{
+			try {
+				switch (level) {
+				case FRAME:
+					_frames.insert(new (_alloc_frames) Frame(vaddr, sel,
+					                                         level_log2_size));
+					break;
+				case PAGE_TABLE:
+					_level1.insert(new (_alloc_high) Table(vaddr, paddr, sel,
+					                                         level_log2_size));
+					break;
+				case LEVEL2:
+					_level2.insert(new (_alloc_high) Table(vaddr, paddr, sel,
+					                                      level_log2_size));
+					break;
+				case LEVEL3:
+					_level3.insert(new (_alloc_high) Table(vaddr, paddr, sel,
+					                                      level_log2_size));
+					break;
+				}
+			} catch (Genode::Allocator::Out_of_memory) {
+				throw Mapping_cache_full();
+			} catch (Genode::Out_of_caps) {
+				throw Mapping_cache_full();
+			}
 		}
 
-		bool _page_table_exists(addr_t addr) const
+		template <typename FN, typename T>
+		void _flush_high(FN const &fn, Avl_tree<T> &tree, Allocator &alloc)
 		{
-			for (Page_table const *pt = _page_tables.first(); pt; pt = pt->next()) {
+			for (T *element; (element = tree.first());) {
-				if (_page_table_base(pt->addr) == _page_table_base(addr))
-					return true;
-			}
-			return false;
-		}
 
-		Page_table &_lookup(addr_t addr)
+				fn(element->sel(), element->paddr());
-		{
+
-			for (Page_table *pt = _page_tables.first(); pt; pt = pt->next()) {
+				tree.remove(element);
-				if (_page_table_base(pt->addr) == _page_table_base(addr))
+				destroy(alloc, element);
-					return *pt;
 			}
-			warning(__func__, ": page-table lookup failed ", Hex(addr));
-			throw Lookup_failed();
 		}
 
 	public:
@@ -210,105 +199,89 @@ class Genode::Page_table_registry
 		 * Constructor
 		 *
 		 * \param md_alloc  backing store allocator for metadata
-		 *
-		 * XXX The md_alloc argument is currently unused as we dimension
-		 *     MAX_PAGE_TABLES and MAX_PAGE_TABLE_ENTRIES statically.
 		 */
-		Page_table_registry(Allocator &md_alloc) { }
+		Page_table_registry(Allocator &md_alloc)
+		:
+			_alloc_frames(md_alloc, _initial_sb_frame),
+			_alloc_high(md_alloc, _initial_sb_high)
+		{ }
 
 		~Page_table_registry()
 		{
-			if (_page_tables.first())
+			if (_frames.first() || _level1.first() || _level2.first() ||
+			    _level3.first())
 				error("still entries in page table registry in destruction");
 		}
 
-		/**
+		bool page_table_at(addr_t const vaddr, addr_t const level_log2) {
-		 * Register page table
+			return Table::lookup(_level1, vaddr, level_log2); }
-		 *
+		bool page_directory_at(addr_t const vaddr, addr_t const level_log2) {
-		 * \param addr  virtual address
+			return Table::lookup(_level2, vaddr, level_log2); }
-		 * \param sel   page-table selector
+		bool page_level3_at(addr_t const vaddr, addr_t const level_log2) {
-		 */
+			return Table::lookup(_level3, vaddr, level_log2); }
-		void insert_page_table(addr_t addr, Cap_sel sel)
-		{
-			/* XXX sel is unused */
 
-			if (_page_table_exists(addr)) {
+		void insert_page_frame(addr_t const vaddr, Cap_sel const sel) {
-				warning("attempt to insert page table for ", Hex(addr), " twice");
+			_insert(vaddr, sel, Level::FRAME, 0, LEVEL_0); }
-				return;
+		void insert_page_table(addr_t const vaddr, Cap_sel const sel,
-			}
+		                       addr_t const paddr, addr_t const level_log2) {
-
+			_insert(vaddr, sel, Level::PAGE_TABLE, paddr, level_log2); }
-			_page_tables.insert(new (_page_table_alloc) Page_table(addr));
+		void insert_page_directory(addr_t const vaddr, Cap_sel const sel,
-		}
+		                           addr_t const paddr, addr_t const level_log2) {
-
+			_insert(vaddr, sel, Level::LEVEL2, paddr, level_log2); }
-		bool has_page_table_at(addr_t addr) const
+		void insert_page_level3(addr_t const vaddr, Cap_sel const sel,
-		{
+		                        addr_t const paddr, addr_t const level_log2) {
-			return _page_table_exists(addr);
+			_insert(vaddr, sel, Level::LEVEL3, paddr, level_log2); }
-		}
 
 		/**
-		 * Register page table entry
+		 * Apply functor 'fn' to selector of specified virtual address and
+		 * flush the page frame from the this cache.
 		 *
-		 * \param addr  virtual address
+		 * \param vaddr  virtual address
-		 * \param sel   page frame selector
-		 *
-		 * \throw  Lookup_failed  no page table for given address
-		 */
-		void insert_page_table_entry(addr_t addr, unsigned sel)
-		{
-			_lookup(addr).insert_entry(_page_table_entry_alloc, addr, sel);
-		}
-
-		/**
-		 * Discard the information about the given virtual address
-		 */
-		void forget_page_table_entry(addr_t addr)
-		{
-			try {
-				Page_table &page_table = _lookup(addr);
-				page_table.remove_entry(_page_table_entry_alloc, addr);
-			} catch (...) { }
-		}
-
-
-		void flush_cache()
-		{
-			for (Page_table *pt = _page_tables.first(); pt; pt = pt->next())
-				pt->flush_all(_page_table_entry_alloc);
-		}
-
-		/**
-		 * Apply functor 'fn' to selector of specified virtual address
-		 *
-		 * \param addr  virtual address
 		 *
 		 * The functor is called with the selector of the page table entry
 		 * (the copy of the phys frame selector) as argument.
 		 */
 		template <typename FN>
-		void apply(addr_t addr, FN const &fn)
+		void flush_page(addr_t vaddr, FN const &fn)
 		{
-			try {
+			Frame * frame = Frame::lookup(_frames, vaddr, LEVEL_0);
-				Page_table        &page_table = _lookup(addr);
+			if (!frame)
-				Page_table::Entry &entry      = page_table.lookup(addr);
+				return;
 
-				fn(entry.sel);
+			fn(frame->sel(), frame->vaddr());
-			} catch (...) { }
+			_frames.remove(frame);
+			destroy(_alloc_frames, frame);
 		}
 
 		template <typename FN>
-		void apply_to_and_destruct_all(FN const &fn)
+		void flush_pages(FN const &fn)
 		{
-			for (Page_table *pt; (pt = _page_tables.first());) {
+			Avl_tree<Frame> tmp;
 
-				Page_table::Entry *entry = pt->first();
+			for (Frame *frame; (frame = _frames.first());) {
-				for (; entry; entry = entry->next())
-					fn(entry->sel);
 
-				pt->flush_all(_page_table_entry_alloc);
+				if (fn(frame->sel(), frame->vaddr())) {
-
+					_frames.remove(frame);
-				_page_tables.remove(pt);
+					destroy(_alloc_frames, frame);
-				destroy(_page_table_alloc, pt);
+				} else {
+					_frames.remove(frame);
+					tmp.insert(frame);
+				}
 			}
+
+			for (Frame *frame; (frame = tmp.first());) {
+				tmp.remove(frame);
+				_frames.insert(frame);
+			}
+		}
+
+		template <typename PG, typename LV>
+		void flush_all(PG const &pages, LV const &level)
+		{
+			flush_pages(pages);
+			_flush_high(level, _level1, _alloc_high);
+			_flush_high(level, _level2, _alloc_high);
+			_flush_high(level, _level3, _alloc_high);
 		}
 };
 

repos/base-sel4/src/core/include/platform.h

@@ -21,9 +21,63 @@
 #include <core_cspace.h>
 #include <initial_untyped_pool.h>
 
-namespace Genode { class Platform; }
+namespace Genode {
+	class Platform;
+	template <Genode::size_t> class Static_allocator;
+}
 
 
+/**
+ * Allocator operating on a static memory pool
+ *
+ * \param MAX   maximum number of 4096 blocks
+ *
+ * The size of a single ELEM must be a multiple of sizeof(long).
+ */
+template <Genode::size_t MAX>
+class Genode::Static_allocator : public Allocator
+{
+	private:
+
+		Bit_allocator<MAX> _used;
+
+		struct Elem_space { uint8_t space[4096]; };
+
+		Elem_space _elements[MAX];
+
+	public:
+
+		class Alloc_failed { };
+
+		bool alloc(size_t size, void **out_addr) override
+		{
+			*out_addr = nullptr;
+
+			if (size > sizeof(Elem_space)) {
+				error("unexpected allocation size of ", size);
+				return false;
+			}
+
+			try {
+				*out_addr = &_elements[_used.alloc()]; }
+			catch (typename Bit_allocator<MAX>::Out_of_indices) {
+				return false; }
+
+			return true;
+		}
+
+		size_t overhead(size_t) const override { return 0; }
+
+		void free(void *ptr, size_t) override
+		{
+			Elem_space *elem = reinterpret_cast<Elem_space *>(ptr);
+			unsigned const index = elem - &_elements[0];
+			_used.free(index);
+		}
+
+		bool need_size_for_free() const { return false; }
+};
+
 class Genode::Platform : public Platform_generic
 {
 	private:
@@ -65,6 +119,7 @@ class Genode::Platform : public Platform_generic
 		 * need to initialize the TLS mechanism that is used to find the IPC
 		 * buffer for the calling thread.
 		 */
+		void init_sel4_ipc_buffer();
 		bool const _init_sel4_ipc_buffer_done;
 
 		/* allocate 1st-level CNode */
@@ -131,6 +186,7 @@ class Genode::Platform : public Platform_generic
 		void       _switch_to_core_cspace();
 		bool const _switch_to_core_cspace_done;
 
+		Static_allocator<sizeof(void *) * 6> _core_page_table_registry_alloc;
 		Page_table_registry _core_page_table_registry;
 
 		/**
@@ -159,6 +215,11 @@ class Genode::Platform : public Platform_generic
 
 		void _init_rom_modules();
 
+		/**
+		 * Unmap page frame provided by kernel during early bootup.
+		 */
+		long _unmap_page_frame(Cap_sel const &);
+
 	public:
 
 		/**

repos/base-sel4/src/core/include/sel4_boot_info.h

@@ -14,26 +14,9 @@
 #ifndef _CORE__INCLUDE__SEL4_BOOT_INFO_H_
 #define _CORE__INCLUDE__SEL4_BOOT_INFO_H_
 
-/* Genode includes */
-#include <base/stdint.h>
-
 /* seL4 includes */
 #include <sel4/bootinfo.h>
 
-
+namespace Genode { seL4_BootInfo const &sel4_boot_info(); }
-/* provided by the assembly startup code */
-extern Genode::addr_t __initial_bx;
-
-
-namespace Genode {
-
-	/**
-	 * Obtain seL4 boot info structure
-	 */
-	static inline seL4_BootInfo const &sel4_boot_info()
-	{
-		return *(seL4_BootInfo const *)__initial_bx;
-	}
-}
 
 #endif /* _CORE__INCLUDE__SEL4_BOOT_INFO_H_ */

repos/base-sel4/src/core/include/thread_sel4.h

@@ -1,5 +1,5 @@
 /*
- * \brief  Utilities fo thread creation on seL4
+ * \brief  Utilities for thread creation on seL4
  * \author Norman Feske
  * \date   2015-05-12
  *
@@ -48,7 +48,7 @@ namespace Genode {
 	 * Set register values for the instruction pointer and stack pointer and
 	 * start the seL4 thread
 	 */
-	static inline void start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp);
+	void start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp);
 };
 
 
@@ -129,21 +129,6 @@ void Genode::Thread_info::destruct()
 }
 
 
-void Genode::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp)
+void Genode::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp);
-{
-	/* set register values for the instruction pointer and stack pointer */
-	seL4_UserContext regs;
-	Genode::memset(&regs, 0, sizeof(regs));
-	size_t const num_regs = sizeof(regs)/sizeof(seL4_Word);
-
-	regs.eip = ip;
-	regs.esp = sp;
-	regs.fs  = IPCBUF_GDT_SELECTOR;
-
-	int const ret = seL4_TCB_WriteRegisters(tcb_sel.value(), false, 0, num_regs, &regs);
-	ASSERT(ret == 0);
-
-	seL4_TCB_Resume(tcb_sel.value());
-}
 
 #endif /* _CORE__INCLUDE__THREAD_SEL4_H_ */

repos/base-sel4/src/core/include/untyped_memory.h

@@ -90,6 +90,9 @@ struct Genode::Untyped_memory
 	}
 
 
+	static seL4_Word smallest_page_type();
+
+
 	/**
 	 * Create page frames from untyped memory
 	 */
@@ -99,22 +102,22 @@ struct Genode::Untyped_memory
 		for (size_t i = 0; i < num_pages; i++, phys_addr += get_page_size()) {
 
 			seL4_Untyped const service     = untyped_sel(phys_addr).value();
-			int          const type        = seL4_X86_4K;
+			seL4_Word    const type        = smallest_page_type();
-			int          const size_bits   = 0;
+			seL4_Word    const size_bits   = 0;
 			seL4_CNode   const root        = Core_cspace::top_cnode_sel();
-			int          const node_index  = Core_cspace::TOP_CNODE_PHYS_IDX;
+			seL4_Word    const node_index  = Core_cspace::TOP_CNODE_PHYS_IDX;
-			int          const node_depth  = Core_cspace::NUM_TOP_SEL_LOG2;
+			seL4_Word    const node_depth  = Core_cspace::NUM_TOP_SEL_LOG2;
-			int          const node_offset = phys_addr >> get_page_size_log2();
+			seL4_Word    const node_offset = phys_addr >> get_page_size_log2();
-			int          const num_objects = 1;
+			seL4_Word    const num_objects = 1;
 
-			int const ret = seL4_Untyped_Retype(service,
+			long const ret = seL4_Untyped_Retype(service,
-			                                    type,
+			                                     type,
-			                                    size_bits,
+			                                     size_bits,
-			                                    root,
+			                                     root,
-			                                    node_index,
+			                                     node_index,
-			                                    node_depth,
+			                                     node_depth,
-			                                    node_offset,
+			                                     node_offset,
-			                                    num_objects);
+			                                     num_objects);
 
 			if (ret != seL4_NoError) {
 				error(__FUNCTION__, ": seL4_Untyped_RetypeAtOffset (IA32_4K) "

repos/base-sel4/src/core/include/vm_space.h

@@ -22,6 +22,8 @@
 #include <base/session_label.h>
 
 /* core includes */
+#include <base/internal/capability_space_sel4.h>
+#include <base/internal/stack_area.h>
 #include <page_table_registry.h>
 #include <cnode.h>
 #include <cap_sel_alloc.h>
@@ -49,18 +51,18 @@ class Genode::Vm_space
 			/**
 			 * Number of entries of 3rd-level VM CNode ('_vm_3rd_cnode')
 			 */
-			VM_3RD_CNODE_SIZE_LOG2 = 8,
+			VM_3RD_CNODE_SIZE_LOG2 = (CONFIG_WORD_SIZE == 32) ? 8 : 7,
 
 			/**
 			 * Number of entries of each leaf CNodes
 			 */
-			LEAF_CNODE_SIZE_LOG2 = 8UL,
+			LEAF_CNODE_SIZE_LOG2 = (CONFIG_WORD_SIZE == 32) ? 8 : 7,
 			LEAF_CNODE_SIZE      = 1UL << LEAF_CNODE_SIZE_LOG2,
 
 			/**
 			 * Number of leaf CNodes
 			 */
-			NUM_LEAF_CNODES_LOG2 = 6UL,
+			NUM_LEAF_CNODES_LOG2 = (CONFIG_WORD_SIZE == 32) ? 6 : 5,
 			NUM_LEAF_CNODES      = 1UL << NUM_LEAF_CNODES_LOG2,
 
 			/**
@@ -151,12 +153,12 @@ class Genode::Vm_space
 		/**
 		 * Return selector for a capability slot within '_vm_cnodes'
 		 */
-		unsigned _idx_to_sel(unsigned idx) const { return (_id << 20) | idx; }
+		addr_t _idx_to_sel(addr_t idx) const { return (_id << 20) | idx; }
 
-		bool _map_page(addr_t from_phys, addr_t to_virt, bool flush_support)
+		bool _map_frame(addr_t from_phys, addr_t to_virt, bool flush_support)
 		{
 			/* allocate page-table entry selector */
-			unsigned pte_idx = _sel_alloc.alloc();
+			addr_t pte_idx = _sel_alloc.alloc();
 
 			/*
 			 * Copy page-frame selector to pte_sel
@@ -170,99 +172,95 @@ class Genode::Vm_space
 
 			/* remember relationship between pte_sel and the virtual address */
 			try {
-				_page_table_registry.insert_page_table_entry(to_virt, pte_idx);
+				_page_table_registry.insert_page_frame(to_virt, Cap_sel(pte_idx));
 			} catch (Page_table_registry::Mapping_cache_full) {
-				if (!flush_support)
+				if (!flush_support) {
+					warning("mapping cache full, but can't flush");
 					throw;
+				}
 
 				warning("flush page table entries - mapping cache full - PD: ",
 				        _pd_label.string());
 
-				_page_table_registry.flush_cache();
+				_page_table_registry.flush_pages([&] (Cap_sel const &idx,
+				                                      addr_t const v_addr)
+				{
+					/* XXX - INITIAL_IPC_BUFFER can't be re-mapped currently */
+					if (v_addr == 0x1000)
+						return false;
+					/* XXX - UTCB can't be re-mapped currently */
+					if (stack_area_virtual_base() <= v_addr
+					    && (v_addr < stack_area_virtual_base() +
+					                 stack_area_virtual_size())
+					    && !((v_addr + 0x1000) & (stack_virtual_size() - 1)))
+							return false;
+
+					long err = _unmap_page(idx);
+					if (err != seL4_NoError)
+						error("unmap failed, idx=", idx, " res=", err);
+
+					_leaf_cnode(idx.value()).remove(_leaf_cnode_entry(idx.value()));
+
+					_sel_alloc.free(idx.value());
+
+					return true;
+				});
 
 				/* re-try once */
-				_page_table_registry.insert_page_table_entry(to_virt, pte_idx);
+				_page_table_registry.insert_page_frame(to_virt, Cap_sel(pte_idx));
 			}
 
 			/*
 			 * Insert copy of page-frame selector into page table
 			 */
-			{
+			long ret = _map_page(Cap_sel(pte_idx), to_virt);
-				seL4_X86_Page          const service = _idx_to_sel(pte_idx);
+			if (ret != seL4_NoError) {
-				seL4_X86_PageDirectory const pd      = _pd_sel.value();
+				error("seL4_*_Page_Map ", Hex(from_phys), "->",
-				seL4_Word              const vaddr   = to_virt;
+				      Hex(to_virt), " returned ", ret);
-				seL4_CapRights_t       const rights  = seL4_AllRights;
+				return false;
-				seL4_X86_VMAttributes  const attr    = seL4_X86_Default_VMAttributes;
-
-				int const ret = seL4_X86_Page_Map(service, pd, vaddr, rights, attr);
-
-				if (ret != seL4_NoError) {
-					error("seL4_X86_Page_Map to ", Hex(from_phys), "->",
-					      Hex(to_virt), " returned ", ret);
-					return false;
-				}
 			}
 			return true;
 		}
 
-		void _unmap_page(addr_t virt)
+		/**
-		{
+		 * Platform specific map/unmap of a page frame
-			/* delete copy of the mapping's page-frame selector */
+		 */
-			_page_table_registry.apply(virt, [&] (unsigned idx) {
+		long _map_page(Genode::Cap_sel const &idx, Genode::addr_t const virt);
-
+		long _unmap_page(Genode::Cap_sel const &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);
-			});
-
-			/* release meta data about the mapping */
-			_page_table_registry.forget_page_table_entry(virt);
-		}
-
-		void _map_page_table(Cap_sel pt_sel, addr_t to_virt)
-		{
-			seL4_X86_PageTable     const service = pt_sel.value();
-			seL4_X86_PageDirectory const pd      = _pd_sel.value();
-			seL4_Word              const vaddr   = to_virt;
-			seL4_X86_VMAttributes  const attr    = seL4_X86_Default_VMAttributes;
-
-			int const ret = seL4_X86_PageTable_Map(service, pd, vaddr, attr);
-			if (ret != seL4_NoError)
-				error("seL4_X86_PageTable_Map returned ", ret);
-		}
 
 		class Alloc_page_table_failed : Exception { };
 
 		/**
-		 * Allocate and install page table at given virtual address
+		 * Allocate and install page structures for the protection domain.
 		 *
 		 * \throw Alloc_page_table_failed
 		 */
-		void _alloc_and_map_page_table(addr_t to_virt)
+		template <typename KOBJ>
+		Cap_sel _alloc_and_map(addr_t const virt,
+			                   long (&map_fn)(Cap_sel, Cap_sel, addr_t),
+			                   addr_t &phys)
 		{
-			/* allocate page-table selector */
+			/* allocate page-* selector */
-			unsigned const pt_idx = _sel_alloc.alloc();
+			addr_t const idx = _sel_alloc.alloc();
 
 			try {
-				addr_t const phys_addr     = Untyped_memory::alloc_page(_phys_alloc);
+				phys = Untyped_memory::alloc_page(_phys_alloc);
-				seL4_Untyped const service = Untyped_memory::untyped_sel(phys_addr).value();
+				seL4_Untyped const service = Untyped_memory::untyped_sel(phys).value();
-				create<Page_table_kobj>(service,
+				create<KOBJ>(service, _leaf_cnode(idx).sel(),
-				                        _leaf_cnode(pt_idx).sel(),
+				             _leaf_cnode_entry(idx));
-				                        _leaf_cnode_entry(pt_idx));
 			} catch (...) {
+				/* XXX free idx, revert untyped memory, phys_addr, */
 				 throw Alloc_page_table_failed();
 			}
 
-			Cap_sel const pt_sel(_idx_to_sel(pt_idx));
+			Cap_sel const pt_sel(_idx_to_sel(idx));
 
-			_page_table_registry.insert_page_table(to_virt, pt_sel);
+			long const result = map_fn(pt_sel, _pd_sel, virt);
+			if (result != seL4_NoError)
+				error("seL4_*_Page*_Map(,", Hex(virt), ") returned ",
+				      result);
 
-			_map_page_table(pt_sel, to_virt);
+			return Cap_sel(idx);
 		}
 
 	public:
@@ -324,10 +322,24 @@ class Genode::Vm_space
 		~Vm_space()
 		{
 			/* delete copy of the mapping's page-frame selectors */
-			_page_table_registry.apply_to_and_destruct_all([&] (unsigned idx) {
+			_page_table_registry.flush_all([&] (Cap_sel const &idx, addr_t const virt) {
-				_leaf_cnode(idx).remove(_leaf_cnode_entry(idx));
 
-				_sel_alloc.free(idx);
+				long err = _unmap_page(idx);
+				if (err != seL4_NoError)
+					error("unmap ", Hex(virt), " failed, ", idx, " res=", err);
+
+				_leaf_cnode(idx.value()).remove(_leaf_cnode_entry(idx.value()));
+
+				_sel_alloc.free(idx.value());
+
+				return true;
+			}, [&] (Cap_sel const &idx, addr_t const paddr) {
+
+				_leaf_cnode(idx.value()).remove(idx);
+
+				_sel_alloc.free(idx.value());
+
+				Untyped_memory::free_page(_phys_alloc, paddr);
 			});
 
 			for (unsigned i = 0; i < NUM_LEAF_CNODES; i++) {
@@ -342,7 +354,6 @@ class Genode::Vm_space
 
 			_cap_sel_alloc.free(_vm_3rd_cnode.sel());
 			_cap_sel_alloc.free(_vm_pad_cnode.sel());
-
 		}
 
 		void map(addr_t from_phys, addr_t to_virt, size_t num_pages,
@@ -353,11 +364,10 @@ class Genode::Vm_space
 			for (size_t i = 0; i < num_pages; i++) {
 				off_t const offset = i << get_page_size_log2();
 
-				if (_map_page(from_phys + offset, to_virt + offset, flush_support))
+				if (!_map_frame(from_phys + offset, to_virt + offset,
-					continue;
+				                flush_support))
-
+					error("mapping failed ", Hex(from_phys + offset),
-				error("mapping failed ", Hex(from_phys + offset),
+					      " -> ", Hex(to_virt + offset));
-				      " -> ", Hex(to_virt + offset));
 			}
 		}
 
@@ -367,20 +377,30 @@ class Genode::Vm_space
 
 			for (size_t i = 0; i < num_pages; i++) {
 				off_t const offset = i << get_page_size_log2();
-				_unmap_page(virt + offset);
+
+				_page_table_registry.flush_page(virt + offset, [&] (Cap_sel const &idx, addr_t) {
+
+					long result = _unmap_page(idx);
+					if (result != seL4_NoError) {
+						error("unmap ", Hex(virt + offset), " failed, idx=",
+						      idx, " result=", result);
+						return;
+					}
+
+					_leaf_cnode(idx.value()).remove(_leaf_cnode_entry(idx.value()));
+
+					_sel_alloc.free(idx.value());
+				});
 			}
 		}
 
+		void unsynchronized_alloc_page_tables(addr_t const start,
+		                                      addr_t const size);
+
 		void alloc_page_tables(addr_t const start, addr_t const size)
 		{
 			Lock::Guard guard(_lock);
-
+			unsynchronized_alloc_page_tables(start, size);
-			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);
-				}
-			}
 		}
 };
 

repos/base-sel4/src/core/platform.cc

@@ -31,6 +31,13 @@ using namespace Genode;
 
 static bool const verbose_boot_info = true;
 
+/**
+ * Platform object is set if object is currently in construction.
+ * Avoids deadlocks due to nested calls of Platform() constructor caused by
+ * platform_specific(). May happen if meta data allocator of phys_alloc runs
+ * out of memory.
+ */
+static Platform * platform_in_construction = nullptr;
 
 /*
  * Memory-layout information provided by the linker script
@@ -47,11 +54,14 @@ extern unsigned _prog_img_beg, _prog_img_end;
 bool Mapped_mem_allocator::_map_local(addr_t virt_addr, addr_t phys_addr,
                                       unsigned size)
 {
+	if (platform_in_construction)
+		Genode::warning("need physical memory, but Platform object not constructed yet");
+
 	size_t const num_pages = size / get_page_size();
 
 	Untyped_memory::convert_to_page_frames(phys_addr, num_pages);
 
-	return map_local(phys_addr, virt_addr, num_pages);
+	return map_local(phys_addr, virt_addr, num_pages, platform_in_construction);
 }
 
 
@@ -78,12 +88,6 @@ void Platform::_init_unused_phys_alloc()
 }
 
 
-static inline void init_sel4_ipc_buffer()
-{
-	asm volatile ("movl %0, %%fs" :: "r"(IPCBUF_GDT_SELECTOR) : "memory");
-}
-
-
 void Platform::_init_allocators()
 {
 	/* interrupt allocator */
@@ -93,34 +97,21 @@ void Platform::_init_allocators()
 	 * XXX allocate intermediate CNodes for organizing the untyped pages here
 	 */
 
-	/* 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());
-
-		if (page_aligned_offset >= range.size)
-			return;
-
-		addr_t const base = range.phys + page_aligned_offset;
-		size_t const size = range.size - page_aligned_offset;
-
-		_core_mem_alloc.phys_alloc()->add_range(base, size);
-		_unused_phys_alloc.remove_range(base, size);
-	};
-	_initial_untyped_pool.for_each_range(add_phys_range);
-
 	/* turn remaining untyped memory ranges into untyped pages */
-	_initial_untyped_pool.turn_remainder_into_untyped_pages();
+	_initial_untyped_pool.turn_into_untyped_object(Core_cspace::TOP_CNODE_UNTYPED_IDX,
+		[&] (addr_t const phys, addr_t const size, bool const device) {
+			/* 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)
+				_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);
+		});
 
 	/*
 	 * From this point on, we can no longer create kernel objects from the
@@ -156,7 +147,7 @@ void Platform::_init_allocators()
 
 	if (verbose_boot_info) {
 		typedef Hex_range<addr_t> Hex_range;
-		log("virtual adress layout of core:");
+		log("virtual address 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));
@@ -169,7 +160,8 @@ void Platform::_init_allocators()
 
 void Platform::_switch_to_core_cspace()
 {
-	Cnode_base const initial_cspace(Cap_sel(seL4_CapInitThreadCNode), 32);
+	Cnode_base const initial_cspace(Cap_sel(seL4_CapInitThreadCNode),
+	                                CONFIG_WORD_SIZE);
 
 	/* copy initial selectors to core's CNode */
 	_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapInitThreadTCB));
@@ -211,10 +203,9 @@ void Platform::_switch_to_core_cspace()
 
 		/* 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 = _unmap_page_frame(Cap_sel(sel));
-			long err = seL4_X86_Page_Unmap(service);
+			if (err != seL4_NoError)
-			if (err)
+				error("unmapping boot modules ", Hex(virt_addr), " error=", err);
-				error("unmapping boot modules ", Hex(virt_addr));
 		}
 
 		/* insert cap for core image */
@@ -250,10 +241,12 @@ void Platform::_switch_to_core_cspace()
 	/* activate core's CSpace */
 	{
 		seL4_CapData_t null_data = { { 0 } };
+		seL4_CapData_t const guard = seL4_CapData_Guard_new(0, CONFIG_WORD_SIZE - 32);
 
 		int const ret = seL4_TCB_SetSpace(seL4_CapInitThreadTCB,
 		                                  seL4_CapNull, /* fault_ep */
-		                                  Core_cspace::top_cnode_sel(), null_data,
+		                                  Core_cspace::top_cnode_sel(),
+		                                  guard,
 		                                  seL4_CapInitThreadPD, null_data);
 
 		if (ret != seL4_NoError)
@@ -268,41 +261,6 @@ Cap_sel Platform::_init_asid_pool()
 }
 
 
-void Platform::_init_core_page_table_registry()
-{
-	seL4_BootInfo const &bi = sel4_boot_info();
-
-	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);
-
-	/*
-	 * Register initial page tables
-	 */
-	addr_t virt_addr = (addr_t)(&_prog_img_beg);
-	for (unsigned sel = bi.userImagePaging.start; sel < bi.userImagePaging.end; sel++) {
-
-		_core_page_table_registry.insert_page_table(virt_addr, Cap_sel(sel));
-
-		/* one page table has 1024 entries */
-		virt_addr += 1024*get_page_size();
-	}
-
-	/*
-	 * Register initial page frames
-	 */
-	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);
-	}
-}
-
-
 void Platform::_init_rom_modules()
 {
 	seL4_BootInfo const &bi = sel4_boot_info();
@@ -394,7 +352,7 @@ Platform::Platform()
 	_vm_size(3*1024*1024*1024UL - _vm_base), /* use the lower 3GiB */
 	_init_sel4_ipc_buffer_done((init_sel4_ipc_buffer(), true)),
 	_switch_to_core_cspace_done((_switch_to_core_cspace(), true)),
-	_core_page_table_registry(*core_mem_alloc()),
+	_core_page_table_registry(_core_page_table_registry_alloc),
 	_init_core_page_table_registry_done((_init_core_page_table_registry(), true)),
 	_init_allocators_done((_init_allocators(), true)),
 	_core_vm_space(Cap_sel(seL4_CapInitThreadPD),
@@ -407,6 +365,8 @@ Platform::Platform()
 	               _core_page_table_registry,
 	               "core")
 {
+	platform_in_construction = this;
+
 	/* create notification object for Genode::Lock used by this first thread */
 	Cap_sel lock_sel (INITIAL_SEL_LOCK);
 	Cap_sel core_sel = _core_sel_alloc.alloc();
@@ -429,8 +389,9 @@ Platform::Platform()
 
 	/* back stack area with page tables */
 	enum { MAX_CORE_THREADS = 32 };
-	_core_vm_space.alloc_page_tables(stack_area_virtual_base(),
+	_core_vm_space.unsynchronized_alloc_page_tables(stack_area_virtual_base(),
-	                                 stack_virtual_size() * MAX_CORE_THREADS);
+	                                                stack_virtual_size() *
+	                                                MAX_CORE_THREADS);
 
 	/* add some minor virtual region for dynamic usage by core */
 	addr_t const virt_size = 32 * 1024 * 1024;
@@ -443,7 +404,7 @@ Platform::Platform()
 		_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);
+		_core_vm_space.unsynchronized_alloc_page_tables(virt_addr, virt_size);
 	}
 
 	/* I/O port allocator (only meaningful for x86) */
@@ -461,6 +422,8 @@ Platform::Platform()
 	}
 
 	_init_rom_modules();
+
+	platform_in_construction = nullptr;
 }
 
 

repos/base-sel4/src/core/platform_pd.cc

@@ -129,25 +129,6 @@ void Platform_pd::assign_parent(Native_capability parent)
 }
 
 
-addr_t Platform_pd::_init_page_directory()
-{
-	addr_t       const phys_addr = Untyped_memory::alloc_page(*platform()->ram_alloc());
-	seL4_Untyped const service   = Untyped_memory::untyped_sel(phys_addr).value();
-
-	create<Page_directory_kobj>(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());
-
-	if (ret != seL4_NoError)
-		error("seL4_X86_ASIDPool_Assign returned ", ret);
-
-	return phys_addr;
-}
-
-
 Cap_sel Platform_pd::alloc_sel()
 {
 	Lock::Guard guard(_sel_alloc_lock);
@@ -166,8 +147,13 @@ 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());
+	try {
-	_vm_space.map(mapping.from_phys(), mapping.to_virt(), mapping.num_pages());
+		_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());
+	} catch (...) {
+		/* pager ep would die when we re-throw - let core survive */
+		Genode::error("unexpected exception during page fault handling");
+	}
 }
 
 

repos/base-sel4/src/core/platform_thread.cc

@@ -143,7 +143,7 @@ int Platform_thread::start(void *ip, void *sp, unsigned int cpu_no)
 
 	/* bind thread to PD and CSpace */
 	seL4_CapData_t const guard_cap_data =
-		seL4_CapData_Guard_new(0, 32 - _pd->cspace_size_log2());
+		seL4_CapData_Guard_new(0, CONFIG_WORD_SIZE - _pd->cspace_size_log2());
 
 	seL4_CapData_t const no_cap_data = { { 0 } };
 
@@ -180,41 +180,6 @@ void Platform_thread::state(Thread_state s)
 }
 
 
-Thread_state Platform_thread::state()
-{
-	seL4_TCB   const thread         = _info.tcb_sel.value();
-	seL4_Bool  const suspend_source = false;
-	seL4_Uint8 const arch_flags     = 0;
-	seL4_UserContext registers;
-	seL4_Word  const register_count = sizeof(registers) / sizeof(registers.eip);
-
-	int const ret = seL4_TCB_ReadRegisters(thread, suspend_source, arch_flags,
-	                                       register_count, &registers);
-	if (ret != seL4_NoError) {
-		error("reading thread state ", ret);
-		throw Cpu_thread::State_access_failed();
-	}
-
-	Thread_state state;
-	state.ip     = registers.eip;
-	state.sp     = registers.esp;
-	state.edi    = registers.edi;
-	state.esi    = registers.esi;
-	state.ebp    = registers.ebp;
-	state.ebx    = registers.ebx;
-	state.edx    = registers.edx;
-	state.ecx    = registers.ecx;
-	state.eax    = registers.eax;
-	state.gs     = registers.gs;
-	state.fs     = registers.fs;
-	state.eflags = registers.eflags;
-	state.trapno = 0; /* XXX detect/track if in exception and report here */
-	/* registers.tls_base unused */
-
-	return state;
-}
-
-
 void Platform_thread::cancel_blocking()
 {
 	seL4_Signal(_info.lock_sel.value());

repos/base-sel4/src/core/spec/x86_32/arch_kernel_object.h

@@ -0,0 +1,40 @@
+/*
+ * \brief   Utilities for creating seL4 kernel objects
+ * \author  Norman Feske
+ * \date    2015-05-08
+ */
+
+/*
+ * Copyright (C) 2015-2017 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 _CORE__X86_32_ARCH_KERNEL_OBJECT_H_
+#define _CORE__X86_32_ARCH_KERNEL_OBJECT_H_
+
+#include <sel4/objecttype.h>
+
+namespace Genode {
+
+	enum {
+		PAGE_TABLE_LOG2_SIZE = 22 /* 4M region */
+	};
+
+	struct Page_table_kobj
+	{
+		enum { SEL4_TYPE = seL4_X86_PageTableObject, SIZE_LOG2 = 12 };
+		static char const *name() { return "page table"; }
+	};
+
+
+	struct Page_directory_kobj
+	{
+		enum { SEL4_TYPE = seL4_X86_PageDirectoryObject, SIZE_LOG2 = 12 };
+		static char const *name() { return "page directory"; }
+	};
+
+};
+
+#endif /* _CORE__X86_32_ARCH_KERNEL_OBJECT_H_ */

repos/base-sel4/src/core/spec/x86_32/boot_info.cc

@@ -0,0 +1,30 @@
+/*
+ * \brief   Access to seL4 boot info
+ * \author  Norman Feske
+ * \date    2015-05-04
+ */
+
+/*
+ * Copyright (C) 2015-2017 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.
+ */
+
+/* Genode includes */
+#include <base/stdint.h>
+
+/* core includes */
+#include <sel4_boot_info.h>
+
+
+/* provided by the assembly startup code */
+extern Genode::addr_t __initial_bx;
+
+/**
+ * Obtain seL4 boot info structure
+ */
+seL4_BootInfo const & Genode::sel4_boot_info()
+{
+	return *(seL4_BootInfo const *)__initial_bx;
+}

repos/base-sel4/src/core/spec/x86_32/platform.cc

@@ -0,0 +1,74 @@
+/*
+ * \brief   Platform interface implementation - x86_32 specific
+ * \author  Norman Feske
+ * \date    2015-05-01
+ */
+
+/*
+ * Copyright (C) 2015-2017 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.
+ */
+
+/* base includes */
+#include <base/internal/crt0.h>
+
+/* core includes */
+#include <boot_modules.h>
+#include <platform.h>
+
+#include "arch_kernel_object.h"
+
+seL4_Word Genode::Untyped_memory::smallest_page_type() { return seL4_X86_4K; }
+
+void Genode::Platform::init_sel4_ipc_buffer()
+{
+	asm volatile ("movl %0, %%fs" :: "r"(IPCBUF_GDT_SELECTOR) : "memory");
+}
+
+long Genode::Platform::_unmap_page_frame(Cap_sel const &sel) {
+	return seL4_X86_Page_Unmap(sel.value()); }
+
+void Genode::Platform::_init_core_page_table_registry()
+{
+	seL4_BootInfo const &bi = sel4_boot_info();
+
+	addr_t virt_addr = (addr_t)(&_prog_img_beg);
+	unsigned sel     = bi.userImagePaging.start;
+
+	/* we don't know the physical location of some objects XXX */
+	enum { XXX_PHYS_UNKNOWN = ~0UL };
+
+	/*
+	 * Register initial page tables
+	 */
+	for (; sel < bi.userImagePaging.end; sel++) {
+		_core_page_table_registry.insert_page_table(virt_addr, Cap_sel(sel),
+		                                            XXX_PHYS_UNKNOWN,
+		                                            PAGE_TABLE_LOG2_SIZE);
+		virt_addr += 1024 * get_page_size();
+	}
+
+	/*
+	 * 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
+}
+
+

repos/base-sel4/src/core/spec/x86_32/platform_pd.cc

@@ -0,0 +1,35 @@
+/*
+ * \brief   Protection-domain facility
+ * \author  Norman Feske
+ * \date    2015-05-01
+ */
+
+/*
+ * Copyright (C) 2015-2017 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.
+ */
+
+/* core includes */
+#include <platform_pd.h>
+
+#include "arch_kernel_object.h"
+
+Genode::addr_t Genode::Platform_pd::_init_page_directory()
+{
+	addr_t const phys_addr = Untyped_memory::alloc_page(*platform()->ram_alloc());
+	seL4_Untyped const service = Untyped_memory::untyped_sel(phys_addr).value();
+
+	create<Page_directory_kobj>(service,
+	                            platform_specific()->core_cnode().sel(),
+	                            _page_directory_sel);
+
+	long ret = seL4_X86_ASIDPool_Assign(platform_specific()->asid_pool().value(),
+	                                    _page_directory_sel.value());
+
+	if (ret != seL4_NoError)
+		error("seL4_X86_ASIDPool_Assign returned ", ret);
+
+	return phys_addr;
+}

repos/base-sel4/src/core/spec/x86_32/thread.cc

@@ -0,0 +1,76 @@
+/*
+ * \brief  Utilities for thread creation on seL4
+ * \author Norman Feske
+ * \date   2015-05-12
+ *
+ * This file is used by both the core-specific implementation of the Thread API
+ * and the platform-thread implementation for managing threads outside of core.
+ */
+
+/*
+ * Copyright (C) 2015-2017 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.
+ */
+
+/* base includes */
+#include <base/thread_state.h>
+
+/* core includes */
+#include <thread_sel4.h>
+#include <platform_thread.h>
+
+void Genode::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp)
+{
+	/* set register values for the instruction pointer and stack pointer */
+	seL4_UserContext regs;
+	Genode::memset(&regs, 0, sizeof(regs));
+	size_t const num_regs = sizeof(regs)/sizeof(seL4_Word);
+
+	regs.eip = ip;
+	regs.esp = sp;
+	regs.fs  = IPCBUF_GDT_SELECTOR;
+
+	long const ret = seL4_TCB_WriteRegisters(tcb_sel.value(), false, 0,
+	                                         num_regs, &regs);
+	ASSERT(ret == 0);
+
+	seL4_TCB_Resume(tcb_sel.value());
+}
+
+Genode::Thread_state Genode::Platform_thread::state()
+{
+	seL4_TCB   const thread         = _info.tcb_sel.value();
+	seL4_Bool  const suspend_source = false;
+	seL4_Uint8 const arch_flags     = 0;
+	seL4_UserContext registers;
+	seL4_Word  const register_count = sizeof(registers) / sizeof(registers.eip);
+
+	long const ret = seL4_TCB_ReadRegisters(thread, suspend_source, arch_flags,
+	                                        register_count, &registers);
+	if (ret != seL4_NoError) {
+		error("reading thread state ", ret);
+		throw Cpu_thread::State_access_failed();
+	}
+
+	Thread_state state;
+	Genode::memset(&state, 0, sizeof(state));
+
+	state.ip     = registers.eip;
+	state.sp     = registers.esp;
+	state.edi    = registers.edi;
+	state.esi    = registers.esi;
+	state.ebp    = registers.ebp;
+	state.ebx    = registers.ebx;
+	state.edx    = registers.edx;
+	state.ecx    = registers.ecx;
+	state.eax    = registers.eax;
+	state.gs     = registers.gs;
+	state.fs     = registers.fs;
+	state.eflags = registers.eflags;
+	state.trapno = 0; /* XXX detect/track if in exception and report here */
+	/* registers.tls_base unused */
+
+	return state;
+}

repos/base-sel4/src/core/spec/x86_32/vm_space.cc

@@ -0,0 +1,61 @@
+/*
+ * \brief   Virtual-memory space
+ * \author  Norman Feske
+ * \date    2015-05-04
+ */
+
+/*
+ * Copyright (C) 2015-2017 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.
+ */
+
+/* core includes */
+#include <vm_space.h>
+
+#include "arch_kernel_object.h"
+
+static long map_page_table(Genode::Cap_sel const pagetable,
+                           Genode::Cap_sel const vroot,
+                           Genode::addr_t const virt)
+{
+	return seL4_X86_PageTable_Map(pagetable.value(), vroot.value(), virt,
+	                              seL4_X86_Default_VMAttributes);
+}
+
+long Genode::Vm_space::_map_page(Genode::Cap_sel const &idx,
+                                 Genode::addr_t const virt)
+{
+	seL4_X86_Page          const service = _idx_to_sel(idx.value());
+	seL4_X86_PageDirectory const pd      = _pd_sel.value();
+	seL4_CapRights_t       const rights  = seL4_AllRights;
+	seL4_X86_VMAttributes  const attr    = seL4_X86_Default_VMAttributes;
+
+	return seL4_X86_Page_Map(service, pd, virt, rights, attr);
+}
+
+long Genode::Vm_space::_unmap_page(Genode::Cap_sel const &idx)
+{
+	seL4_X86_Page const service = _idx_to_sel(idx.value());
+	return seL4_X86_Page_Unmap(service);
+}
+
+void Genode::Vm_space::unsynchronized_alloc_page_tables(addr_t const start,
+                                                        addr_t const size)
+{
+	addr_t constexpr PAGE_TABLE_AREA = 1UL << PAGE_TABLE_LOG2_SIZE;
+	addr_t virt = start & ~(PAGE_TABLE_AREA - 1);
+	for (; virt < start + size; virt += PAGE_TABLE_AREA) {
+
+		if (_page_table_registry.page_table_at(virt, PAGE_TABLE_LOG2_SIZE))
+			continue;
+
+		addr_t phys = 0;
+
+		/* 4 MB range - page table */
+		Cap_sel const pt = _alloc_and_map<Page_table_kobj>(virt, map_page_table, phys);
+		_page_table_registry.insert_page_table(virt, pt, phys,
+		                                       PAGE_TABLE_LOG2_SIZE);
+	}
+}

repos/base-sel4/src/core/spec/x86_64/arch_kernel_object.h

@@ -0,0 +1,53 @@
+/*
+ * \brief   Utilities for creating seL4 kernel objects
+ * \author  Norman Feske
+ * \date    2015-05-08
+ */
+
+/*
+ * Copyright (C) 2015-2017 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 _CORE__X86_64_ARCH_KERNEL_OBJECT_H_
+#define _CORE__X86_64_ARCH_KERNEL_OBJECT_H_
+
+#include <sel4/objecttype.h>
+
+namespace Genode {
+
+	enum {
+		PAGE_TABLE_LOG2_SIZE  = 21, /*   2M  region */
+		PAGE_DIR_LOG2_SIZE    = 30, /*   1GB region */
+		PAGE_PDPT_LOG2_SIZE   = 39  /* 512GB region */
+	};
+
+	struct Page_table_kobj
+	{
+		enum { SEL4_TYPE = seL4_X86_PageTableObject, SIZE_LOG2 = 12 };
+		static char const *name() { return "page table"; }
+	};
+
+
+	struct Page_directory_kobj
+	{
+		enum { SEL4_TYPE = seL4_X86_PageDirectoryObject, SIZE_LOG2 = 12 };
+		static char const *name() { return "page directory"; }
+	};
+
+	struct Page_pointer_table_kobj
+	{
+		enum { SEL4_TYPE = seL4_X86_PDPTObject, SIZE_LOG2 = 12 };
+		static char const *name() { return "page directory pointer table"; }
+	};
+
+	struct Page_map_kobj
+	{
+		enum { SEL4_TYPE = seL4_X64_PML4Object, SIZE_LOG2 = 12 };
+		static char const *name() { return "page-map level-4 table"; }
+	};
+};
+
+#endif /* _CORE__X86_64_ARCH_KERNEL_OBJECT_H_ */

repos/base-sel4/src/core/spec/x86_64/boot_info.cc

@@ -0,0 +1,30 @@
+/*
+ * \brief   Access to seL4 boot info
+ * \author  Norman Feske
+ * \date    2015-05-04
+ */
+
+/*
+ * Copyright (C) 2015-2017 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.
+ */
+
+/* Genode includes */
+#include <base/stdint.h>
+
+/* core includes */
+#include <sel4_boot_info.h>
+
+
+/* provided by the assembly startup code */
+extern Genode::addr_t __initial_di;
+
+/**
+ * Obtain seL4 boot info structure
+ */
+seL4_BootInfo const & Genode::sel4_boot_info()
+{
+	return *(seL4_BootInfo const *)__initial_di;
+}

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

@@ -0,0 +1,83 @@
+/*
+ * \brief   Platform interface implementation - x86_64 specific
+ * \author  Alexander Boettcher
+ * \date    2017-07-05
+ */
+
+/*
+ * Copyright (C) 2017 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.
+ */
+
+/* base includes */
+#include <base/internal/crt0.h>
+
+/* core includes */
+#include <boot_modules.h>
+#include <platform.h>
+
+#include "arch_kernel_object.h"
+
+seL4_Word Genode::Untyped_memory::smallest_page_type() { return seL4_X86_4K; }
+
+void Genode::Platform::init_sel4_ipc_buffer() { }
+
+long Genode::Platform::_unmap_page_frame(Cap_sel const &sel) {
+	return seL4_X86_Page_Unmap(sel.value()); }
+
+void Genode::Platform::_init_core_page_table_registry()
+{
+	seL4_BootInfo const &bi = sel4_boot_info();
+
+	addr_t virt_addr = (addr_t)(&_prog_img_beg);
+	unsigned sel     = bi.userImagePaging.start;
+
+	/* we don't know the physical location of some objects XXX */
+	enum { XXX_PHYS_UNKNOWN = ~0UL };
+
+	/*
+	 * Register initial pdpt and page directory
+	 */
+	_core_page_table_registry.insert_page_level3(virt_addr, Cap_sel(sel),
+	                                             XXX_PHYS_UNKNOWN,
+	                                             PAGE_PDPT_LOG2_SIZE);
+	_core_page_table_registry.insert_page_directory(virt_addr,
+	                                                Cap_sel(sel + 1),
+	                                                XXX_PHYS_UNKNOWN,
+	                                                PAGE_DIR_LOG2_SIZE);
+	sel += 2;
+
+	/*
+	 * Register initial page tables
+	 */
+	for (; sel < bi.userImagePaging.end; sel++) {
+		_core_page_table_registry.insert_page_table(virt_addr, Cap_sel(sel),
+		                                            XXX_PHYS_UNKNOWN,
+		                                            PAGE_TABLE_LOG2_SIZE);
+		virt_addr += 512 * get_page_size();
+	}
+
+	/*
+	 * 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
+}
+
+

repos/base-sel4/src/core/spec/x86_64/platform_pd.cc

@@ -0,0 +1,34 @@
+/*
+ * \brief   Protection-domain facility
+ * \author  Norman Feske
+ * \date    2015-05-01
+ */
+
+/*
+ * Copyright (C) 2015-2017 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.
+ */
+
+/* core includes */
+#include <platform_pd.h>
+
+#include "arch_kernel_object.h"
+
+Genode::addr_t Genode::Platform_pd::_init_page_directory()
+{
+	addr_t const phys_addr = Untyped_memory::alloc_page(*platform()->ram_alloc());
+	seL4_Untyped const service = Untyped_memory::untyped_sel(phys_addr).value();
+
+	create<Page_map_kobj>(service, platform_specific()->core_cnode().sel(),
+	                      _page_directory_sel);
+
+	long ret = seL4_X86_ASIDPool_Assign(platform_specific()->asid_pool().value(),
+	                                    _page_directory_sel.value());
+
+	if (ret != seL4_NoError)
+		error("seL4_X86_ASIDPool_Assign returned ", ret);
+
+	return phys_addr;
+}

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

@@ -0,0 +1,81 @@
+/*
+ * \brief  Utilities for thread creation on seL4
+ * \author Norman Feske
+ * \date   2015-05-12
+ *
+ * This file is used by both the core-specific implementation of the Thread API
+ * and the platform-thread implementation for managing threads outside of core.
+ */
+
+/*
+ * Copyright (C) 2015-2017 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.
+ */
+
+/* base includes */
+#include <base/thread_state.h>
+
+/* core includes */
+#include <thread_sel4.h>
+#include <platform_thread.h>
+
+void Genode::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp)
+{
+	/* set register values for the instruction pointer and stack pointer */
+	seL4_UserContext regs;
+	Genode::memset(&regs, 0, sizeof(regs));
+	size_t const num_regs = sizeof(regs)/sizeof(seL4_Word);
+
+	regs.rip = ip;
+	regs.rsp = sp;
+
+	long const ret = seL4_TCB_WriteRegisters(tcb_sel.value(), false, 0,
+	                                         num_regs, &regs);
+	ASSERT(ret == 0);
+
+	seL4_TCB_Resume(tcb_sel.value());
+}
+
+Genode::Thread_state Genode::Platform_thread::state()
+{
+	seL4_TCB   const thread         = _info.tcb_sel.value();
+	seL4_Bool  const suspend_source = false;
+	seL4_Uint8 const arch_flags     = 0;
+	seL4_UserContext registers;
+	seL4_Word  const register_count = sizeof(registers) / sizeof(registers.rip);
+
+	long const ret = seL4_TCB_ReadRegisters(thread, suspend_source, arch_flags,
+	                                        register_count, &registers);
+	if (ret != seL4_NoError) {
+		error("reading thread state ", ret);
+		throw Cpu_thread::State_access_failed();
+	}
+
+	Thread_state state;
+	Genode::memset(&state, 0, sizeof(state));
+
+	state.ip     = registers.rip;
+	state.sp     = registers.rsp;
+	state.rdi    = registers.rdi;
+	state.rsi    = registers.rsi;
+	state.rbp    = registers.rbp;
+	state.rbx    = registers.rbx;
+	state.rdx    = registers.rdx;
+	state.rcx    = registers.rcx;
+	state.rax    = registers.rax;
+	state.r8     = registers.r8;
+	state.r9     = registers.r9;
+	state.r10    = registers.r10;
+	state.r11    = registers.r11;
+	state.r12    = registers.r12;
+	state.r13    = registers.r13;
+	state.r14    = registers.r14;
+	state.r15    = registers.r15;
+	state.eflags = registers.rflags;
+	state.trapno = 0; /* XXX detect/track if in exception and report here */
+	/* registers.tls_base unused */
+
+	return state;
+}

repos/base-sel4/src/core/spec/x86_64/vm_space.cc

@@ -0,0 +1,87 @@
+/*
+ * \brief   Virtual-memory space
+ * \author  Norman Feske
+ * \date    2015-05-04
+ */
+
+/*
+ * Copyright (C) 2015-2017 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.
+ */
+
+/* core includes */
+#include <vm_space.h>
+
+#include "arch_kernel_object.h"
+
+static long map_page_table(Genode::Cap_sel const pagetable,
+                           Genode::Cap_sel const vroot,
+                           Genode::addr_t  const virt)
+{
+	return seL4_X86_PageTable_Map(pagetable.value(), vroot.value(), virt,
+	                              seL4_X86_Default_VMAttributes);
+}
+
+static long map_pdpt(Genode::Cap_sel const pdpt,
+                     Genode::Cap_sel const vroot,
+                     seL4_Word const virt)
+{
+	return seL4_X86_PDPT_Map(pdpt.value(), vroot.value(), virt,
+	                         seL4_X86_Default_VMAttributes);
+}
+
+static long map_directory(Genode::Cap_sel const pd,
+                          Genode::Cap_sel const vroot,
+                          seL4_Word const virt)
+{
+	return seL4_X86_PageDirectory_Map(pd.value(), vroot.value(), virt,
+	                                  seL4_X86_Default_VMAttributes);
+}
+
+long Genode::Vm_space::_map_page(Genode::Cap_sel const &idx,
+                                 Genode::addr_t const virt)
+{
+	seL4_X86_Page          const service = _idx_to_sel(idx.value());
+	seL4_X86_PageDirectory const pd      = _pd_sel.value();
+	seL4_CapRights_t       const rights  = seL4_AllRights;
+	seL4_X86_VMAttributes  const attr    = seL4_X86_Default_VMAttributes;
+
+	return seL4_X86_Page_Map(service, pd, virt, rights, attr);
+}
+
+long Genode::Vm_space::_unmap_page(Genode::Cap_sel const &idx)
+{
+	seL4_X86_Page const service = _idx_to_sel(idx.value());
+	return seL4_X86_Page_Unmap(service);
+}
+
+void Genode::Vm_space::unsynchronized_alloc_page_tables(addr_t const start,
+                                                        addr_t const size)
+{
+	addr_t constexpr PAGE_TABLE_AREA = 1UL << PAGE_TABLE_LOG2_SIZE;
+	addr_t virt = start & ~(PAGE_TABLE_AREA - 1);
+	for (; virt < start + size; virt += PAGE_TABLE_AREA) {
+		addr_t phys = 0;
+
+		if (!_page_table_registry.page_level3_at(virt, PAGE_PDPT_LOG2_SIZE)) {
+			/* 512 GB range - page directory pointer table */
+			Cap_sel const pd = _alloc_and_map<Page_pointer_table_kobj>(virt, map_pdpt, phys);
+			_page_table_registry.insert_page_level3(virt, pd, phys, PAGE_PDPT_LOG2_SIZE);
+		}
+		if (!_page_table_registry.page_directory_at(virt, PAGE_DIR_LOG2_SIZE)) {
+			/*   1 GB range - page directory */
+			Cap_sel const pd = _alloc_and_map<Page_directory_kobj>(virt, map_directory, phys);
+			_page_table_registry.insert_page_directory(virt, pd, phys,
+			                                           PAGE_DIR_LOG2_SIZE);
+		}
+
+		if (!_page_table_registry.page_table_at(virt, PAGE_TABLE_LOG2_SIZE)) {
+			/*   2 MB range - page table */
+			Cap_sel const pt = _alloc_and_map<Page_table_kobj>(virt, map_page_table, phys);
+			_page_table_registry.insert_page_table(virt, pt, phys,
+		                                           PAGE_TABLE_LOG2_SIZE);
+		}
+	}
+}

repos/base-sel4/src/core/thread_start.cc

@@ -52,9 +52,11 @@ void Thread::_init_platform_thread(size_t, Type type)
 
 	Platform &platform = *platform_specific();
 
+	seL4_CapData_t guard = seL4_CapData_Guard_new(0, CONFIG_WORD_SIZE - 32);
 	seL4_CapData_t no_cap_data = { { 0 } };
 	int const ret = seL4_TCB_SetSpace(native_thread().tcb_sel, 0,
-	                                  platform.top_cnode().sel().value(), no_cap_data,
+	                                  platform.top_cnode().sel().value(),
+	                                  guard,
 	                                  seL4_CapInitThreadPD, no_cap_data);
 	ASSERT(ret == seL4_NoError);
 

repos/base-sel4/src/include/base/internal/capability_space_sel4.h

@@ -103,7 +103,7 @@ namespace Genode
 
 	enum {
 		CSPACE_SIZE_LOG2_1ST      = 6,
-		CSPACE_SIZE_LOG2_2ND      = 8,
+		CSPACE_SIZE_LOG2_2ND      = (CONFIG_WORD_SIZE == 32) ? 8 : 7,
 		CSPACE_SIZE_LOG2          = CSPACE_SIZE_LOG2_1ST + CSPACE_SIZE_LOG2_2ND,
 		NUM_CORE_MANAGED_SEL_LOG2 = 8,
 	};

repos/base-sel4/src/lib/base/capability_space.cc

@@ -40,7 +40,7 @@ namespace {
 
 	struct Local_capability_space
 	:
-		Capability_space_sel4<15*1024, 1UL << NUM_CORE_MANAGED_SEL_LOG2,
+		Capability_space_sel4<8*1024, 1UL << NUM_CORE_MANAGED_SEL_LOG2,
 		                      Native_capability::Data>
 	{ };
 

repos/libports/run/nic_dump.run

@@ -85,7 +85,7 @@ proc server_bin { prot } {
 	if {$prot == "http"} { return "test-lwip_httpsrv_static" } }
 
 proc ram_quota { prot } {
-	if {$prot == "udp"}  { return 28M }
+	if {$prot == "udp"}  { return 29M }
 	if {$prot == "http"} { return 12M }
 }
 

repos/libports/run/nic_router.run

@@ -89,7 +89,7 @@ proc server_bin { prot } {
 	if {$prot == "http"} { return "test-lwip_httpsrv_static" } }
 
 proc ram_quota { prot } {
-	if {$prot == "udp"}  { return 28M }
+	if {$prot == "udp"}  { return 29M }
 	if {$prot == "http"} { return 12M }
 }
 

repos/os/run/blk_cache.run

@@ -41,7 +41,7 @@ install_config {
 		<provides><service name="Block"/></provides>
 	</start>
 	<start name="blk_cache">
-		<resource name="RAM" quantum="2304K" />
+		<resource name="RAM" quantum="2704K" />
 		<provides><service name="Block" /></provides>
 		<route>
 			<service name="Block"><child name="test-blk-srv" /></service>

repos/os/run/tar_rom.run

@@ -50,7 +50,7 @@ install_config {
 		</config>
 	</start>
 	<start name="init" caps="1000">
-		<resource name="RAM" quantum="2M"/>
+		<resource name="RAM" quantum="3M"/>
 		<config verbose="yes">
 			<parent-provides>
 				<service name="ROM"/>

repos/os/run/timer.run

@@ -26,7 +26,7 @@ install_config {
 	<default-route>
 		<any-service><parent/><any-child/></any-service>
 	</default-route>
-	<start name="timer" caps="60">
+	<start name="timer" caps="64">
 		<resource name="RAM" quantum="1M"/>
 		<provides><service name="Timer"/></provides>
 	</start>

tool/builddir/build.conf/run_kernel_x86_64

@@ -1,3 +1,3 @@
-# kernel to use (nova, hw, linux, or foc)
+# kernel to use (nova, hw, sel4, linux, or foc)
 #KERNEL ?= nova
 

tool/builddir/build.conf/run_opt_x86_64

@@ -1,6 +1,7 @@
 # local varible for run-tool arguments that depend on the used kernel
 KERNEL_RUN_OPT(nova)  := $(QEMU_RUN_OPT)
 KERNEL_RUN_OPT(hw)    := $(QEMU_RUN_OPT)
+KERNEL_RUN_OPT(sel4)  := $(QEMU_RUN_OPT)
 KERNEL_RUN_OPT(foc)   := $(QEMU_RUN_OPT)
 KERNEL_RUN_OPT(linux) := --include power_on/linux --include log/linux
 

tool/create_builddir

@@ -162,6 +162,7 @@ BUILD_CONF(hw_x86_64)       := run_kernel_hw        $(BUILD_CONF_X86_64)
 BUILD_CONF(foc_x86_32)      := run_kernel_foc       $(BUILD_CONF_X86_32)
 BUILD_CONF(foc_x86_64)      := run_kernel_foc       $(BUILD_CONF_X86_64)
 BUILD_CONF(sel4_x86_32)     := run_kernel_sel4      $(BUILD_CONF_X86_32)
+BUILD_CONF(sel4_x86_64)     := run_kernel_sel4      $(BUILD_CONF_X86_64)
 BUILD_CONF(hw_panda)        := ${BUILD_CONF(panda)}
 BUILD_CONF(foc_panda)       := run_kernel_foc run_boot_dir repos
 BUILD_CONF(hw_pbxa9)        := ${BUILD_CONF(pbxa9)}
@@ -244,6 +245,7 @@ SPECS(hw_x86_64)       := ${SPECS(x86_64)}
 SPECS(foc_x86_32)      := foc_x86_32 x86_32 acpi
 SPECS(foc_x86_64)      := foc_x86_64 x86_64 acpi
 SPECS(sel4_x86_32)     := sel4_x86_32 x86_32 acpi
+SPECS(sel4_x86_64)     := sel4_x86_64 x86_64 acpi
 SPECS(hw_panda)        := ${SPECS(panda)}
 SPECS(foc_panda)       := foc_panda panda
 SPECS(hw_pbxa9)        := ${SPECS(pbxa9)}