diff --git a/repos/base-sel4/etc/specs.conf b/repos/base-sel4/etc/specs.conf
index 92a508fb14..7f8559a229 100644
--- a/repos/base-sel4/etc/specs.conf
+++ b/repos/base-sel4/etc/specs.conf
@@ -1 +1,5 @@
-SPECS += sel4 acpi
+SPECS += sel4
+
+ifneq ($(filter $(SPECS),x86_32 x86_64),)
+SPECS += acpi pci ps2 vesa framebuffer
+endif
diff --git a/repos/base-sel4/lib/mk/base-sel4.mk b/repos/base-sel4/lib/mk/base-sel4.inc
similarity index 77%
rename from repos/base-sel4/lib/mk/base-sel4.mk
rename to repos/base-sel4/lib/mk/base-sel4.inc
index 531615ffe7..b59644222b 100644
--- a/repos/base-sel4/lib/mk/base-sel4.mk
+++ b/repos/base-sel4/lib/mk/base-sel4.inc
@@ -5,4 +5,4 @@ SRC_CC += thread_start.cc thread_init.cc
SRC_CC += cache.cc
SRC_CC += signal_transmitter.cc signal.cc
-LIBS += syscall-sel4 base-sel4-common cxx timeout
+LIBS += syscall-sel4 base-sel4-common cxx
diff --git a/repos/base-sel4/lib/mk/spec/arm/base-sel4.mk b/repos/base-sel4/lib/mk/spec/arm/base-sel4.mk
new file mode 100644
index 0000000000..f692d40d62
--- /dev/null
+++ b/repos/base-sel4/lib/mk/spec/arm/base-sel4.mk
@@ -0,0 +1,3 @@
+LIBS += timeout-arm
+
+include $(REP_DIR)/lib/mk/base-sel4.inc
diff --git a/repos/base-sel4/lib/mk/spec/arm/ld-sel4.mk b/repos/base-sel4/lib/mk/spec/arm/ld-sel4.mk
new file mode 100644
index 0000000000..eec86f1bd5
--- /dev/null
+++ b/repos/base-sel4/lib/mk/spec/arm/ld-sel4.mk
@@ -0,0 +1,3 @@
+BASE_LIBS += base-sel4-common base-sel4
+
+include $(BASE_DIR)/lib/mk/spec/arm/ld-platform.inc
diff --git a/repos/base-sel4/lib/mk/spec/arm/startup-sel4.mk b/repos/base-sel4/lib/mk/spec/arm/startup-sel4.mk
new file mode 100644
index 0000000000..2683fd7761
--- /dev/null
+++ b/repos/base-sel4/lib/mk/spec/arm/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/arm/startup.inc
diff --git a/repos/base-sel4/lib/mk/spec/wand_quad/core-sel4.mk b/repos/base-sel4/lib/mk/spec/wand_quad/core-sel4.mk
new file mode 100644
index 0000000000..dfe0490054
--- /dev/null
+++ b/repos/base-sel4/lib/mk/spec/wand_quad/core-sel4.mk
@@ -0,0 +1,8 @@
+SRC_CC += $(addprefix spec/arm/, boot_info.cc thread.cc platform.cc irq.cc \
+ vm_space.cc)
+
+INC_DIR += $(REP_DIR)/src/core/spec/arm
+
+include $(REP_DIR)/lib/mk/core-sel4.inc
+
+vpath platform_services.cc $(GEN_CORE_DIR)
diff --git a/repos/base-sel4/lib/mk/spec/wand_quad/kernel-sel4.mk b/repos/base-sel4/lib/mk/spec/wand_quad/kernel-sel4.mk
new file mode 100644
index 0000000000..1b98ced9b5
--- /dev/null
+++ b/repos/base-sel4/lib/mk/spec/wand_quad/kernel-sel4.mk
@@ -0,0 +1,33 @@
+SEL4_DIR := $(call select_from_ports,sel4)/src/kernel/sel4
+ELFLOADER_DIR := $(call select_from_ports,sel4_elfloader)/src/tool/elfloader
+
+#
+# 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
+
+elfloader/elfloader.o:
+ $(VERBOSE)cp -rf $(ELFLOADER_DIR) elfloader && \
+ cd elfloader && \
+ sed -i "s/define UART_PPTR.*IMX6_UART2_PADDR/define UART_PPTR IMX6_UART1_PADDR/" src/arch-arm/plat-imx6/platform.h && \
+ $(MAKE) \
+ TOOLPREFIX=$(CROSS_DEV_PREFIX) \
+ NK_ASFLAGS=-DARMV7_A \
+ ARCH=arm PLAT=imx6 ARMV=armv7-a \
+ SEL4_COMMON=$(LIB_CACHE_DIR)/$(LIB)/elfloader \
+ SOURCE_DIR=$(LIB_CACHE_DIR)/$(LIB)/elfloader \
+ STAGE_DIR=$(LIB_CACHE_DIR)/$(LIB)/elfloader \
+ srctree=$(LIB_CACHE_DIR)/$(LIB)/elfloader
+
+build_kernel: elfloader/elfloader.o
+ $(VERBOSE)$(MAKE) \
+ TOOLPREFIX=$(CROSS_DEV_PREFIX) \
+ BOARD=wand_quad ARCH=arm PLAT=imx6 CPU=cortex-a9 ARMV=armv7-a DEBUG=1 \
+ SOURCE_ROOT=$(SEL4_DIR) -f$(SEL4_DIR)/Makefile
+
diff --git a/repos/base-sel4/lib/mk/spec/wand_quad/syscall-sel4.mk b/repos/base-sel4/lib/mk/spec/wand_quad/syscall-sel4.mk
new file mode 100644
index 0000000000..0d52f37977
--- /dev/null
+++ b/repos/base-sel4/lib/mk/spec/wand_quad/syscall-sel4.mk
@@ -0,0 +1,8 @@
+PLAT := imx6
+ARCH := arm
+
+SEL4_ARCH := aarch32
+PLAT_BOARD := /wand_quad
+SEL4_WORDBITS := 32
+
+include $(REP_DIR)/lib/mk/syscall-sel4.inc
diff --git a/repos/base-sel4/lib/mk/spec/x86/base-sel4.mk b/repos/base-sel4/lib/mk/spec/x86/base-sel4.mk
new file mode 100644
index 0000000000..caae7797e1
--- /dev/null
+++ b/repos/base-sel4/lib/mk/spec/x86/base-sel4.mk
@@ -0,0 +1,3 @@
+LIBS += timeout
+
+include $(REP_DIR)/lib/mk/base-sel4.inc
diff --git a/repos/base-sel4/lib/mk/spec/x86_32/core-sel4.mk b/repos/base-sel4/lib/mk/spec/x86_32/core-sel4.mk
index 9818959342..378580ed16 100644
--- a/repos/base-sel4/lib/mk/spec/x86_32/core-sel4.mk
+++ b/repos/base-sel4/lib/mk/spec/x86_32/core-sel4.mk
@@ -1,9 +1,12 @@
SRC_CC += $(addprefix spec/x86_32/, boot_info.cc thread.cc platform.cc \
platform_pd.cc vm_space.cc)
+SRC_CC += $(addprefix spec/x86/, irq.cc vm_space.cc)
SRC_CC += io_port_session_component.cc
SRC_CC += io_port_session_support.cc
+INC_DIR += $(REP_DIR)/src/core/spec/x86
+
include $(REP_DIR)/lib/mk/core-sel4.inc
vpath io_port_session_component.cc $(GEN_CORE_DIR)/spec/x86
diff --git a/repos/base-sel4/lib/mk/spec/x86_64/core-sel4.mk b/repos/base-sel4/lib/mk/spec/x86_64/core-sel4.mk
index 7dbc71203a..002efd8095 100644
--- a/repos/base-sel4/lib/mk/spec/x86_64/core-sel4.mk
+++ b/repos/base-sel4/lib/mk/spec/x86_64/core-sel4.mk
@@ -1,9 +1,12 @@
SRC_CC += $(addprefix spec/x86_64/, boot_info.cc thread.cc platform.cc \
platform_pd.cc vm_space.cc)
+SRC_CC += $(addprefix spec/x86/, irq.cc vm_space.cc)
SRC_CC += io_port_session_component.cc
SRC_CC += io_port_session_support.cc
+INC_DIR += $(REP_DIR)/src/core/spec/x86
+
include $(REP_DIR)/lib/mk/core-sel4.inc
vpath io_port_session_component.cc $(GEN_CORE_DIR)/spec/x86
diff --git a/repos/base-sel4/lib/mk/syscall-sel4.inc b/repos/base-sel4/lib/mk/syscall-sel4.inc
index 6231fdac49..37a32d1373 100644
--- a/repos/base-sel4/lib/mk/syscall-sel4.inc
+++ b/repos/base-sel4/lib/mk/syscall-sel4.inc
@@ -30,7 +30,7 @@ SEL4_ARCH_INCLUDES += simple_types.h types.h constants.h objecttype.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
+ 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 \
diff --git a/repos/base-sel4/patches/arm_cache.patch b/repos/base-sel4/patches/arm_cache.patch
new file mode 100644
index 0000000000..3ea96e9eb1
--- /dev/null
+++ b/repos/base-sel4/patches/arm_cache.patch
@@ -0,0 +1,10 @@
+--- src/kernel/sel4/libsel4/arch_include/arm/sel4/arch/types.h
++++ src/kernel/sel4/libsel4/arch_include/arm/sel4/arch/types.h
+@@ -24,6 +24,7 @@
+ typedef seL4_CPtr seL4_ARM_IOPageTable;
+
+ typedef enum {
++ seL4_ARM_Uncacheable = 0x00,
+ seL4_ARM_PageCacheable = 0x01,
+ seL4_ARM_ParityEnabled = 0x02,
+ seL4_ARM_Default_VMAttributes = 0x03,
diff --git a/repos/base-sel4/patches/noise.patch b/repos/base-sel4/patches/noise.patch
index 9f3e337bcc..6ee65e7b6a 100644
--- a/repos/base-sel4/patches/noise.patch
+++ b/repos/base-sel4/patches/noise.patch
@@ -78,3 +78,32 @@
#endif /* __ASSEMBLER__ */
#define seL4_FastMessageRegisters 4
+--- src/kernel/sel4/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h
++++ src/kernel/sel4/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h
+@@ -40,7 +40,7 @@
+ /* length of an unknown syscall message */
+ seL4_UnknownSyscall_Length,
+ SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg),
+-} seL4_UnknownSyscall_Msg;
++}; // seL4_UnknownSyscall_Msg;
+
+ /* format of a user exception message */
+ enum {
+@@ -52,7 +52,7 @@
+ /* length of a user exception */
+ seL4_UserException_Length,
+ SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg),
+-} seL4_UserException_Msg;
++}; // seL4_UserException_Msg;
+
+ /* format of a vm fault message */
+ enum {
+@@ -62,7 +62,7 @@
+ seL4_VMFault_FSR,
+ seL4_VMFault_Length,
+ SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg),
+-} seL4_VMFault_Msg;
++}; // seL4_VMFault_Msg;
+
+ #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
+ enum {
diff --git a/repos/base-sel4/patches/wand_quad.config b/repos/base-sel4/patches/wand_quad.config
new file mode 100644
index 0000000000..ffede51129
--- /dev/null
+++ b/repos/base-sel4/patches/wand_quad.config
@@ -0,0 +1,27 @@
+--- src/kernel/sel4/configs/imx6/wand_quad/autoconf.h
++++ src/kernel/sel4/configs/imx6/wand_quad/autoconf.h
+@@ -41,6 +41,7 @@
+ #define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1
+ #define CONFIG_LIB_SEL4_UTILS 1
+ #define CONFIG_LIB_SEL4_VSPACE 1
++#define CONFIG_PRINTING 1
+ #define CONFIG_LIB_PLATSUPPORT 1
+ #define CONFIG_LIB_SEL4_ALLOCMAN 1
+ #define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1
+@@ -71,14 +71,14 @@
+ #define CONFIG_HAVE_LIB_SEL4_SIMPLE 1
+ #define CONFIG_ARCH_ARM 1
+ #define CONFIG_HAVE_LIB_ELF 1
+-#define CONFIG_PLAT_SABRE 1
++#define CONFIG_PLAT_WANDQ 1
+ #define CONFIG_HAVE_LIB_PLATSUPPORT 1
+ #define CONFIG_NUM_DOMAINS 16
+ #define CONFIG_HAVE_LIB_UTILS 1
+ #define CONFIG_USER_OPTIMISATION_O2 1
+ #define CONFIG_LIB_CPIO 1
+ #define CONFIG_RETYPE_FAN_OUT_LIMIT 256
+-#define CONFIG_ROOT_CNODE_SIZE_BITS 12
++#define CONFIG_ROOT_CNODE_SIZE_BITS 14
+ #define CONFIG_NUM_PRIORITIES 256
+ #define CONFIG_TESTPRINTER_REGEX ".*"
+ #define CONFIG_APP_SEL4TEST 1
diff --git a/repos/base-sel4/ports/sel4.hash b/repos/base-sel4/ports/sel4.hash
index 2e76e74022..a30910bb3b 100644
--- a/repos/base-sel4/ports/sel4.hash
+++ b/repos/base-sel4/ports/sel4.hash
@@ -1 +1 @@
-3858de13ad9db6b4fa5e21c8a246180aec74571c
+7dc762b776af1721d742d70f6394f6177436817a
diff --git a/repos/base-sel4/ports/sel4.port b/repos/base-sel4/ports/sel4.port
index 3926358def..db5ac535be 100644
--- a/repos/base-sel4/ports/sel4.port
+++ b/repos/base-sel4/ports/sel4.port
@@ -19,3 +19,6 @@ default: $(DOWNLOADS)
$(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
+ $(VERBOSE)mkdir -p src/kernel/sel4/configs/imx6/wand_quad
+ $(VERBOSE)mv src/kernel/sel4/configs/imx6/autoconf.h src/kernel/sel4/configs/imx6/wand_quad/autoconf.h
+ $(VERBOSE)patch -p0 <$(REP_DIR)/patches/wand_quad.config
diff --git a/repos/base-sel4/ports/sel4_elfloader.hash b/repos/base-sel4/ports/sel4_elfloader.hash
new file mode 100644
index 0000000000..3c9bd134d4
--- /dev/null
+++ b/repos/base-sel4/ports/sel4_elfloader.hash
@@ -0,0 +1 @@
+cf90c5aba6d10a0582d53ada6aed06c96ec585b5
diff --git a/repos/base-sel4/ports/sel4_elfloader.port b/repos/base-sel4/ports/sel4_elfloader.port
new file mode 100644
index 0000000000..bd389839ae
--- /dev/null
+++ b/repos/base-sel4/ports/sel4_elfloader.port
@@ -0,0 +1,12 @@
+LICENSE := GPLv2
+VERSION := git
+DOWNLOADS := sel4_elfloader.git
+
+URL(sel4_elfloader) := https://github.com/alex-ab/elfloader-tool.git
+# genode branch
+REV(sel4_elfloader) := 5a12b40ef6be2e71a005e822d17a0b3af8c309bd
+DIR(sel4_elfloader) := src/tool/elfloader
+
+$(call check_tool,python)
+
+PATCHES := $(wildcard $(REP_DIR)/patches/elfloader/*.patch)
diff --git a/repos/base-sel4/src/core/include/core_cspace.h b/repos/base-sel4/src/core/include/core_cspace.h
index 40ac8764a4..9cf3534a01 100644
--- a/repos/base-sel4/src/core/include/core_cspace.h
+++ b/repos/base-sel4/src/core/include/core_cspace.h
@@ -38,8 +38,9 @@ class Genode::Core_cspace
static inline unsigned long core_pad_cnode_sel() { return top_cnode_sel() + 1; }
static inline unsigned long core_cnode_sel() { return core_pad_cnode_sel() + 1; }
static inline unsigned long phys_cnode_sel() { return core_cnode_sel() + 1; }
- static inline unsigned long untyped_cnode_sel() { return phys_cnode_sel() + 1; }
- static unsigned long core_static_sel_end() { return untyped_cnode_sel() + 1; }
+ static inline unsigned long untyped_cnode_4k() { return phys_cnode_sel() + 1; }
+ static inline unsigned long untyped_cnode_16k() { return untyped_cnode_4k() + 1; }
+ static unsigned long core_static_sel_end() { return untyped_cnode_16k() + 1; }
/* indices within top-level CNode */
enum Top_cnode_idx {
@@ -47,8 +48,9 @@ class Genode::Core_cspace
/* XXX mark last index usable for PDs */
- TOP_CNODE_UNTYPED_IDX = 0xffe, /* untyped memory pages */
- TOP_CNODE_PHYS_IDX = 0xfff /* phyical page frames */
+ TOP_CNODE_UNTYPED_16K = 0xffd, /* untyped objects 16K */
+ TOP_CNODE_UNTYPED_4K = 0xffe, /* untyped objects 4K */
+ TOP_CNODE_PHYS_IDX = 0xfff /* physical page frames */
};
enum { CORE_VM_ID = 1 };
diff --git a/repos/base-sel4/src/core/include/install_mapping.h b/repos/base-sel4/src/core/include/install_mapping.h
index c4583474c7..8fb62c33a7 100644
--- a/repos/base-sel4/src/core/include/install_mapping.h
+++ b/repos/base-sel4/src/core/include/install_mapping.h
@@ -20,7 +20,7 @@
namespace Genode {
- void install_mapping(Mapping const &mapping, unsigned long pager_object_badge);
+ bool install_mapping(Mapping const &mapping, unsigned long pager_object_badge);
}
#endif /* _CORE__INCLUDE__INSTALL_MAPPING_H_ */
diff --git a/repos/base-sel4/src/core/include/ipc_pager.h b/repos/base-sel4/src/core/include/ipc_pager.h
index d359cd2a07..995f8a3b78 100644
--- a/repos/base-sel4/src/core/include/ipc_pager.h
+++ b/repos/base-sel4/src/core/include/ipc_pager.h
@@ -18,16 +18,22 @@
#include
#include
+namespace Genode { class Ipc_pager; }
+
namespace Genode {
class Mapping
{
+ friend class Ipc_pager;
+
private:
- addr_t _from_phys_addr;
- addr_t _to_virt_addr;
- size_t _num_pages;
- bool _writeable;
+ addr_t _from_phys_addr;
+ addr_t _to_virt_addr;
+ Cache_attribute _attr;
+ size_t _num_pages;
+ bool _writeable;
+ addr_t _fault_type = { 0 };
enum { PAGE_SIZE_LOG2 = 12 };
@@ -43,6 +49,7 @@ namespace Genode {
:
_from_phys_addr(src_addr),
_to_virt_addr(dst_addr),
+ _attr(cacheability),
_num_pages(1 << (l2size - PAGE_SIZE_LOG2)),
_writeable(rw)
{ }
@@ -64,6 +71,8 @@ namespace Genode {
addr_t to_virt() const { return _to_virt_addr; }
size_t num_pages() const { return _num_pages; }
bool writeable() const { return _writeable; }
+ Cache_attribute cacheability() const { return _attr; }
+ addr_t fault_type() const { return _fault_type; }
};
@@ -74,11 +83,12 @@ namespace Genode {
{
private:
- addr_t _last; /* faulted thread ID */
+ addr_t _badge; /* faulted badge of thread */
addr_t _reply_sel; /* selector to save reply cap */
addr_t _pf_addr; /* page-fault address */
addr_t _pf_ip; /* instruction pointer of faulter */
bool _pf_write; /* true on write fault */
+ addr_t _fault_type; /* type of fault */
Mapping _reply_mapping;
@@ -112,7 +122,11 @@ namespace Genode {
/**
* Set parameters for next reply
*/
- void set_reply_mapping(Mapping m) { _reply_mapping = m; }
+ void set_reply_mapping(Mapping m)
+ {
+ _reply_mapping = m;
+ _reply_mapping._fault_type = _fault_type;
+ }
/**
* Set destination for next reply
@@ -122,7 +136,7 @@ namespace Genode {
/**
* Return badge for faulting thread
*/
- unsigned long badge() const { return _last; }
+ unsigned long badge() const { return _badge; }
/**
* Return true if page fault was a write fault
diff --git a/repos/base-sel4/src/core/include/irq_object.h b/repos/base-sel4/src/core/include/irq_object.h
index f46a800d8b..c261d4ef6f 100644
--- a/repos/base-sel4/src/core/include/irq_object.h
+++ b/repos/base-sel4/src/core/include/irq_object.h
@@ -15,6 +15,7 @@
#define _CORE__INCLUDE__IRQ_OBJECT_H_
#include
+#include
#include
namespace Genode { class Irq_object; }
@@ -33,6 +34,9 @@ class Genode::Irq_object : public Thread_deprecated<4096> {
void entry() override;
+ long _associate(Irq_session::Trigger const &irq_trigger,
+ Irq_session::Polarity const &irq_polarity);
+
public:
Irq_object(unsigned irq);
diff --git a/repos/base-sel4/src/core/include/map_local.h b/repos/base-sel4/src/core/include/map_local.h
index 937ebac567..43aee5e4cc 100644
--- a/repos/base-sel4/src/core/include/map_local.h
+++ b/repos/base-sel4/src/core/include/map_local.h
@@ -36,11 +36,12 @@ namespace Genode {
inline bool map_local(addr_t from_phys, addr_t to_virt, size_t num_pages,
Platform * platform = nullptr)
{
- enum { DONT_FLUSH = false };
+ enum { DONT_FLUSH = false, WRITEABLE = true };
try {
platform = platform ? platform : platform_specific();
platform->core_vm_space().map(from_phys, to_virt, num_pages,
- DONT_FLUSH);
+ Cache_attribute::CACHED,
+ WRITEABLE, DONT_FLUSH);
} catch (Page_table_registry::Mapping_cache_full) {
return false;
}
diff --git a/repos/base-sel4/src/core/include/page_table_registry.h b/repos/base-sel4/src/core/include/page_table_registry.h
index be16b29421..d87d4d147c 100644
--- a/repos/base-sel4/src/core/include/page_table_registry.h
+++ b/repos/base-sel4/src/core/include/page_table_registry.h
@@ -213,6 +213,8 @@ class Genode::Page_table_registry
error("still entries in page table registry in destruction");
}
+ bool page_frame_at(addr_t const vaddr) {
+ return Frame::lookup(_frames, vaddr, LEVEL_0); }
bool page_table_at(addr_t const vaddr, addr_t const level_log2) {
return Table::lookup(_level1, vaddr, level_log2); }
bool page_directory_at(addr_t const vaddr, addr_t const level_log2) {
diff --git a/repos/base-sel4/src/core/include/platform.h b/repos/base-sel4/src/core/include/platform.h
index f070793aa7..3bc98efece 100644
--- a/repos/base-sel4/src/core/include/platform.h
+++ b/repos/base-sel4/src/core/include/platform.h
@@ -144,16 +144,21 @@ class Genode::Platform : public Platform_generic
Cnode_index(Core_cspace::phys_cnode_sel()),
Core_cspace::NUM_PHYS_SEL_LOG2, _initial_untyped_pool };
- /* allocate 2nd-level CNode for storing cap selectors for untyped pages */
+ /* allocate 2nd-level CNode for storing cap selectors for untyped 4k objects */
Cnode _untyped_cnode { Cap_sel(seL4_CapInitThreadCNode),
- Cnode_index(Core_cspace::untyped_cnode_sel()),
+ Cnode_index(Core_cspace::untyped_cnode_4k()),
Core_cspace::NUM_PHYS_SEL_LOG2, _initial_untyped_pool };
+ /* allocate 2nd-level CNode for storing cap selectors for untyped 16k objects */
+ Cnode _untyped_cnode_16k { Cap_sel(seL4_CapInitThreadCNode),
+ Cnode_index(Core_cspace::untyped_cnode_16k()),
+ Core_cspace::NUM_PHYS_SEL_LOG2, _initial_untyped_pool };
+
/*
* XXX Consider making Bit_allocator::_reserve public so that we can
* turn the bit allocator into a private member of 'Core_sel_alloc'.
*/
- typedef Bit_allocator<1 << Core_cspace::NUM_PHYS_SEL_LOG2> Core_sel_bit_alloc;
+ typedef Bit_allocator<1 << Core_cspace::NUM_CORE_SEL_LOG2> Core_sel_bit_alloc;
struct Core_sel_alloc : Cap_sel_alloc, private Core_sel_bit_alloc
{
diff --git a/repos/base-sel4/src/core/include/platform_pd.h b/repos/base-sel4/src/core/include/platform_pd.h
index dce64a4b69..8b52557b51 100644
--- a/repos/base-sel4/src/core/include/platform_pd.h
+++ b/repos/base-sel4/src/core/include/platform_pd.h
@@ -121,7 +121,7 @@ class Genode::Platform_pd : public Address_space
size_t cspace_size_log2() { return CSPACE_SIZE_LOG2; }
- void install_mapping(Mapping const &mapping);
+ bool install_mapping(Mapping const &mapping, const char * thread_name);
};
#endif /* _CORE__INCLUDE__PLATFORM_PD_H_ */
diff --git a/repos/base-sel4/src/core/include/platform_thread.h b/repos/base-sel4/src/core/include/platform_thread.h
index 6dbbecf4bf..11b3acc747 100644
--- a/repos/base-sel4/src/core/include/platform_thread.h
+++ b/repos/base-sel4/src/core/include/platform_thread.h
@@ -180,7 +180,7 @@ class Genode::Platform_thread : public List::Element
Cap_sel tcb_sel() const { return _info.tcb_sel; }
- void install_mapping(Mapping const &mapping);
+ bool install_mapping(Mapping const &mapping);
};
#endif /* _CORE__INCLUDE__PLATFORM_THREAD_H_ */
diff --git a/repos/base-sel4/src/core/include/untyped_memory.h b/repos/base-sel4/src/core/include/untyped_memory.h
index c675a225df..1c7fc5b969 100644
--- a/repos/base-sel4/src/core/include/untyped_memory.h
+++ b/repos/base-sel4/src/core/include/untyped_memory.h
@@ -63,10 +63,11 @@ struct Genode::Untyped_memory
* Local utility solely used by 'untyped_sel' and 'frame_sel'
*/
static inline Cap_sel _core_local_sel(Core_cspace::Top_cnode_idx top_idx,
- addr_t phys_addr)
+ addr_t phys_addr,
+ addr_t size_log2 = get_page_size_log2())
{
unsigned const upper_bits = top_idx << Core_cspace::NUM_PHYS_SEL_LOG2;
- unsigned const lower_bits = phys_addr >> get_page_size_log2();
+ unsigned const lower_bits = phys_addr >> size_log2;
return Cap_sel(upper_bits | lower_bits);
}
@@ -77,7 +78,7 @@ struct Genode::Untyped_memory
*/
static inline Cap_sel untyped_sel(addr_t phys_addr)
{
- return _core_local_sel(Core_cspace::TOP_CNODE_UNTYPED_IDX, phys_addr);
+ return _core_local_sel(Core_cspace::TOP_CNODE_UNTYPED_4K, phys_addr);
}
diff --git a/repos/base-sel4/src/core/include/vm_space.h b/repos/base-sel4/src/core/include/vm_space.h
index ab3cc88c5b..2bc0341643 100644
--- a/repos/base-sel4/src/core/include/vm_space.h
+++ b/repos/base-sel4/src/core/include/vm_space.h
@@ -155,8 +155,22 @@ class Genode::Vm_space
*/
addr_t _idx_to_sel(addr_t idx) const { return (_id << 20) | idx; }
- bool _map_frame(addr_t from_phys, addr_t to_virt, bool flush_support)
+ bool _map_frame(addr_t const from_phys, addr_t const to_virt,
+ Cache_attribute const cacheability,
+ bool const writable, bool const flush_support)
{
+ if (_page_table_registry.page_frame_at(to_virt)) {
+ /*
+ * Valid behaviour if multiple threads concurrently
+ * causing the same page-fault. For the first thread the
+ * fault will be resolved, and the next thread will/would do
+ * it again. We just skip this attempt in order to avoid
+ * wasting of resources (idx selectors, creating kernel
+ * capabilities, causing kernel warning ...).
+ */
+ return false;
+ }
+
/* allocate page-table entry selector */
addr_t pte_idx = _sel_alloc.alloc();
@@ -213,7 +227,8 @@ class Genode::Vm_space
/*
* Insert copy of page-frame selector into page table
*/
- long ret = _map_page(Cap_sel(pte_idx), to_virt);
+ long ret = _map_page(Cap_sel(pte_idx), to_virt, cacheability,
+ writable);
if (ret != seL4_NoError) {
error("seL4_*_Page_Map ", Hex(from_phys), "->",
Hex(to_virt), " returned ", ret);
@@ -225,7 +240,8 @@ class Genode::Vm_space
/**
* Platform specific map/unmap of a page frame
*/
- long _map_page(Genode::Cap_sel const &idx, Genode::addr_t const virt);
+ long _map_page(Genode::Cap_sel const &idx, Genode::addr_t const virt,
+ Cache_attribute const cacheability, bool const write);
long _unmap_page(Genode::Cap_sel const &idx);
class Alloc_page_table_failed : Exception { };
@@ -356,8 +372,9 @@ class Genode::Vm_space
_cap_sel_alloc.free(_vm_pad_cnode.sel());
}
- void map(addr_t from_phys, addr_t to_virt, size_t num_pages,
- bool flush_support = true)
+ void map(addr_t const from_phys, addr_t const to_virt,
+ size_t const num_pages, Cache_attribute const cacheability,
+ bool const writable, bool flush_support)
{
Lock::Guard guard(_lock);
@@ -365,7 +382,7 @@ class Genode::Vm_space
off_t const offset = i << get_page_size_log2();
if (!_map_frame(from_phys + offset, to_virt + offset,
- flush_support))
+ cacheability, writable, flush_support))
error("mapping failed ", Hex(from_phys + offset),
" -> ", Hex(to_virt + offset));
}
@@ -402,6 +419,8 @@ class Genode::Vm_space
Lock::Guard guard(_lock);
unsynchronized_alloc_page_tables(start, size);
}
+
+ Session_label const & pd_label() const { return _pd_label; }
};
#endif /* _CORE__INCLUDE__VM_SPACE_H_ */
diff --git a/repos/base-sel4/src/core/irq_session_component.cc b/repos/base-sel4/src/core/irq_session_component.cc
index 78be43194f..336fd5d633 100644
--- a/repos/base-sel4/src/core/irq_session_component.cc
+++ b/repos/base-sel4/src/core/irq_session_component.cc
@@ -39,27 +39,8 @@ bool Irq_object::associate(Irq_session::Trigger const irq_trigger,
_kernel_notify_sel);
}
- enum { IRQ_EDGE = 0, IRQ_LEVEL = 1 };
- enum { IRQ_HIGH = 0, IRQ_LOW = 1 };
-
- seL4_Word level = (_irq < 16) ? IRQ_EDGE : IRQ_LEVEL;
- seL4_Word polarity = (_irq < 16) ? IRQ_HIGH : IRQ_LOW;
-
- if (irq_trigger != Irq_session::TRIGGER_UNCHANGED)
- level = (irq_trigger == Irq_session::TRIGGER_LEVEL) ? IRQ_LEVEL : IRQ_EDGE;
-
- if (irq_polarity != Irq_session::POLARITY_UNCHANGED)
- polarity = (irq_polarity == Irq_session::POLARITY_HIGH) ? IRQ_HIGH : IRQ_LOW;
-
- /* setup irq */
- seL4_CNode root = seL4_CapInitThreadCNode;
- seL4_Word index = _kernel_irq_sel.value();
- seL4_Uint8 depth = 32;
- seL4_Word ioapic = 0;
- seL4_Word pin = _irq ? _irq : 2;
- seL4_Word vector = _irq;
- int res = seL4_IRQControl_GetIOAPIC(seL4_CapIRQControl, root, index, depth,
- ioapic, pin, level, polarity, vector);
+ /* setup IRQ platform specific */
+ long res = _associate(irq_trigger, irq_polarity);
if (res != seL4_NoError)
return false;
diff --git a/repos/base-sel4/src/core/pager.cc b/repos/base-sel4/src/core/pager.cc
index d574c00526..fd0f07c840 100644
--- a/repos/base-sel4/src/core/pager.cc
+++ b/repos/base-sel4/src/core/pager.cc
@@ -20,28 +20,13 @@
/* base-internal includes */
#include
+#include "fault_info.h"
+
/* seL4 includes */
#include
-#include
using namespace Genode;
-
-struct Fault_info
-{
- addr_t ip = 0;
- addr_t pf = 0;
- bool write = 0;
-
- Fault_info(seL4_MessageInfo_t msg_info)
- :
- ip(seL4_GetMR(0)),
- pf(seL4_GetMR(1)),
- write(seL4_GetMR(3) & 0x2)
- { }
-};
-
-
/***************
** IPC pager **
***************/
@@ -49,7 +34,7 @@ struct Fault_info
void Ipc_pager::wait_for_fault()
{
- if (_last && _reply_sel) {
+ if (_badge && _reply_sel) {
seL4_CNode const service = seL4_CapInitThreadCNode;
seL4_Word const index = _reply_sel;
uint8_t const depth = 32;
@@ -58,21 +43,21 @@ void Ipc_pager::wait_for_fault()
Genode::error("saving reply cap failed with ", ret);
}
_reply_sel = 0;
- _last = 0;
+ _badge = 0;
reply_and_wait_for_fault();
}
void Ipc_pager::reply_and_wait_for_fault()
{
- if (_last)
- install_mapping(_reply_mapping, _last);
+ if (_badge)
+ _badge = install_mapping(_reply_mapping, _badge);
seL4_Word badge = Rpc_obj_key::INVALID;
seL4_MessageInfo_t page_fault_msg_info;
- if (_last) {
+ if (_badge) {
seL4_MessageInfo_t const reply_msg = seL4_MessageInfo_new(0, 0, 0, 0);
@@ -86,15 +71,16 @@ void Ipc_pager::reply_and_wait_for_fault()
Fault_info const fault_info(page_fault_msg_info);
- _pf_ip = fault_info.ip;
- _pf_addr = fault_info.pf;
- _pf_write = fault_info.write;
+ _pf_ip = fault_info.ip;
+ _pf_addr = fault_info.pf;
+ _pf_write = fault_info.write;
+ _fault_type = seL4_MessageInfo_get_label(page_fault_msg_info);
- _last = badge;
+ _badge = badge;
}
-Ipc_pager::Ipc_pager() : _last(0), _reply_sel(0) { }
+Ipc_pager::Ipc_pager() : _badge(0), _reply_sel(0) { }
/******************
diff --git a/repos/base-sel4/src/core/platform.cc b/repos/base-sel4/src/core/platform.cc
index 6281ea55ef..800d726c09 100644
--- a/repos/base-sel4/src/core/platform.cc
+++ b/repos/base-sel4/src/core/platform.cc
@@ -98,7 +98,7 @@ void Platform::_init_allocators()
*/
/* turn remaining untyped memory ranges into untyped pages */
- _initial_untyped_pool.turn_into_untyped_object(Core_cspace::TOP_CNODE_UNTYPED_IDX,
+ _initial_untyped_pool.turn_into_untyped_object(Core_cspace::TOP_CNODE_UNTYPED_4K,
[&] (addr_t const phys, addr_t const size, bool const device) {
/* register to physical or iomem memory allocator */
@@ -169,6 +169,7 @@ void Platform::_switch_to_core_cspace()
_core_cnode.move(initial_cspace, Cnode_index(seL4_CapIRQControl)); /* cannot be copied */
_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapASIDControl));
_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapInitThreadASIDPool));
+ /* XXX io port not available on ARM, causes just a kernel warning XXX */
_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapIOPort));
_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapBootInfoFrame));
_core_cnode.copy(initial_cspace, Cnode_index(seL4_CapInitThreadIPCBuffer));
@@ -235,8 +236,12 @@ void Platform::_switch_to_core_cspace()
Cnode_index(Core_cspace::TOP_CNODE_PHYS_IDX));
/* insert 2nd-level untyped-pages CNode into 1st-level CNode */
- _top_cnode.copy(initial_cspace, Cnode_index(Core_cspace::untyped_cnode_sel()),
- Cnode_index(Core_cspace::TOP_CNODE_UNTYPED_IDX));
+ _top_cnode.copy(initial_cspace, Cnode_index(Core_cspace::untyped_cnode_4k()),
+ Cnode_index(Core_cspace::TOP_CNODE_UNTYPED_4K));
+
+ /* insert 2nd-level untyped-pages CNode into 1st-level CNode */
+ _top_cnode.move(initial_cspace, Cnode_index(Core_cspace::untyped_cnode_16k()),
+ Cnode_index(Core_cspace::TOP_CNODE_UNTYPED_16K));
/* activate core's CSpace */
{
diff --git a/repos/base-sel4/src/core/platform_pd.cc b/repos/base-sel4/src/core/platform_pd.cc
index 05038f6745..a7ec2a9213 100644
--- a/repos/base-sel4/src/core/platform_pd.cc
+++ b/repos/base-sel4/src/core/platform_pd.cc
@@ -89,8 +89,10 @@ bool Platform_pd::bind_thread(Platform_thread *thread)
*/
addr_t const utcb = (thread->_utcb) ? thread->_utcb : thread->INITIAL_IPC_BUFFER_VIRT;
+ enum { WRITABLE = true, ONE_PAGE = 1, FLUSHABLE = true };
_vm_space.alloc_page_tables(utcb, get_page_size());
- _vm_space.map(thread->_info.ipc_buffer_phys, utcb, 1);
+ _vm_space.map(thread->_info.ipc_buffer_phys, utcb, ONE_PAGE,
+ Cache_attribute::CACHED, WRITABLE, FLUSHABLE);
return true;
}
@@ -145,14 +147,48 @@ void Platform_pd::free_sel(Cap_sel sel)
}
-void Platform_pd::install_mapping(Mapping const &mapping)
+bool Platform_pd::install_mapping(Mapping const &mapping,
+ const char *thread_name)
{
+ enum { FLUSHABLE = true };
+
try {
- _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());
+ if (mapping.fault_type() != seL4_Fault_VMFault)
+ throw 1;
+
+ _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(), mapping.cacheability(),
+ mapping.writeable(), FLUSHABLE);
+ return true;
} catch (...) {
+ char const * fault_name = "unknown";
+
+ switch (mapping.fault_type()) {
+ case seL4_Fault_NullFault:
+ fault_name = "seL4_Fault_NullFault";
+ break;
+ case seL4_Fault_CapFault:
+ fault_name = "seL4_Fault_CapFault";
+ break;
+ case seL4_Fault_UnknownSyscall:
+ fault_name = "seL4_Fault_UnknownSyscall";
+ break;
+ case seL4_Fault_UserException:
+ fault_name = "seL4_Fault_UserException";
+ break;
+ case seL4_Fault_VMFault:
+ fault_name = "seL4_Fault_VMFault";
+ break;
+ }
+
/* pager ep would die when we re-throw - let core survive */
- Genode::error("unexpected exception during page fault handling");
+ Genode::error("unexpected exception during fault '", fault_name, "'",
+ " - thread '", thread_name, "' in pd '",
+ _vm_space.pd_label(),"' stopped");
+ return false;
}
}
diff --git a/repos/base-sel4/src/core/platform_thread.cc b/repos/base-sel4/src/core/platform_thread.cc
index 756e585b9f..34aae8df19 100644
--- a/repos/base-sel4/src/core/platform_thread.cc
+++ b/repos/base-sel4/src/core/platform_thread.cc
@@ -51,14 +51,29 @@ class Platform_thread_registry : Noncopyable
_threads.remove(&thread);
}
- void install_mapping(Mapping const &mapping, unsigned long pager_object_badge)
+ bool install_mapping(Mapping const &mapping, unsigned long pager_object_badge)
{
+ unsigned installed = 0;
+ bool result = true;
+
Lock::Guard guard(_lock);
for (Platform_thread *t = _threads.first(); t; t = t->next()) {
- if (t->pager_object_badge() == pager_object_badge)
- t->install_mapping(mapping);
+ if (t->pager_object_badge() == pager_object_badge) {
+ bool ok = t->install_mapping(mapping);
+ if (!ok)
+ result = false;
+ installed ++;
+ }
}
+
+ if (installed != 1) {
+ Genode::error("install mapping is wrong ", installed,
+ " result=", result);
+ result = false;
+ }
+
+ return result;
}
};
@@ -70,9 +85,9 @@ Platform_thread_registry &platform_thread_registry()
}
-void Genode::install_mapping(Mapping const &mapping, unsigned long pager_object_badge)
+bool Genode::install_mapping(Mapping const &mapping, unsigned long pager_object_badge)
{
- platform_thread_registry().install_mapping(mapping, pager_object_badge);
+ return platform_thread_registry().install_mapping(mapping, pager_object_badge);
}
@@ -193,9 +208,9 @@ Weak_ptr Platform_thread::address_space()
}
-void Platform_thread::install_mapping(Mapping const &mapping)
+bool Platform_thread::install_mapping(Mapping const &mapping)
{
- _pd->install_mapping(mapping);
+ return _pd->install_mapping(mapping, name());
}
diff --git a/repos/base-sel4/src/core/spec/arm/arch_kernel_object.h b/repos/base-sel4/src/core/spec/arm/arch_kernel_object.h
new file mode 100644
index 0000000000..83951b2817
--- /dev/null
+++ b/repos/base-sel4/src/core/spec/arm/arch_kernel_object.h
@@ -0,0 +1,40 @@
+/*
+ * \brief Utilities for creating seL4 kernel objects
+ * \author Alexander Boettcher
+ * \date 2017-07-06
+ */
+
+/*
+ * 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.
+ */
+
+#ifndef _CORE__X86_ARM_ARCH_KERNEL_OBJECT_H_
+#define _CORE__X86_ARM_ARCH_KERNEL_OBJECT_H_
+
+#include
+
+namespace Genode {
+
+ enum {
+ PAGE_TABLE_LOG2_SIZE = 20 /* 1M region */
+ };
+
+ struct Page_table_kobj
+ {
+ enum { SEL4_TYPE = seL4_ARM_PageTableObject, SIZE_LOG2 = 12 };
+ static char const *name() { return "page table"; }
+ };
+
+
+ struct Page_directory_kobj
+ {
+ enum { SEL4_TYPE = seL4_ARM_PageDirectoryObject, SIZE_LOG2 = 14 };
+ static char const *name() { return "page directory"; }
+ };
+
+};
+
+#endif /* _CORE__ARM_ARCH_KERNEL_OBJECT_H_ */
diff --git a/repos/base-sel4/src/core/spec/arm/boot_info.cc b/repos/base-sel4/src/core/spec/arm/boot_info.cc
new file mode 100644
index 0000000000..dc30965ae6
--- /dev/null
+++ b/repos/base-sel4/src/core/spec/arm/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
+
+/* core includes */
+#include
+
+
+/* provided by the assembly startup code */
+extern Genode::addr_t __initial_r0;
+
+/**
+ * Obtain seL4 boot info structure
+ */
+seL4_BootInfo const & Genode::sel4_boot_info()
+{
+ return *(seL4_BootInfo const *)__initial_r0;
+}
diff --git a/repos/base-sel4/src/core/spec/arm/fault_info.h b/repos/base-sel4/src/core/spec/arm/fault_info.h
new file mode 100644
index 0000000000..22f65438d3
--- /dev/null
+++ b/repos/base-sel4/src/core/spec/arm/fault_info.h
@@ -0,0 +1,29 @@
+/*
+ * \brief ARM specific fault info
+ * \author Alexander Boettcher
+ * \date 2017-07-11
+ */
+
+/*
+ * 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.
+ */
+
+struct Fault_info
+{
+ Genode::addr_t ip = 0;
+ Genode::addr_t pf = 0;
+ bool data_abort = 0;
+ bool write = 0;
+
+ Fault_info(seL4_MessageInfo_t msg_info)
+ :
+ ip(seL4_GetMR(0)),
+ pf(seL4_GetMR(1)),
+ data_abort(seL4_GetMR(2) != 1),
+ /* Instruction Fault Status Register (IFSR) resp. Data FSR (DFSR) */
+ write(data_abort && (seL4_GetMR(3) & (1 << 11)))
+ { }
+};
diff --git a/repos/base-sel4/src/core/spec/arm/irq.cc b/repos/base-sel4/src/core/spec/arm/irq.cc
new file mode 100644
index 0000000000..05eab2a132
--- /dev/null
+++ b/repos/base-sel4/src/core/spec/arm/irq.cc
@@ -0,0 +1,19 @@
+/*
+ * \brief Implementation of the platform specific IRQ association
+ * \author Alexander Boettcher
+ * \date 2017-07-07
+ */
+
+#include
+
+#include
+
+long Genode::Irq_object::_associate(Irq_session::Trigger const &,
+ Irq_session::Polarity const &)
+{
+ seL4_CNode const root = seL4_CapInitThreadCNode;
+ seL4_Word const index = _kernel_irq_sel.value();
+ seL4_Uint8 const depth = 32;
+
+ return seL4_IRQControl_Get(seL4_CapIRQControl, _irq, root, index, depth);
+}
diff --git a/repos/base-sel4/src/core/spec/arm/platform.cc b/repos/base-sel4/src/core/spec/arm/platform.cc
new file mode 100644
index 0000000000..2034cba0ac
--- /dev/null
+++ b/repos/base-sel4/src/core/spec/arm/platform.cc
@@ -0,0 +1,96 @@
+/*
+ * \brief Platform interface implementation - ARM 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
+
+/* core includes */
+#include
+#include
+
+#include "arch_kernel_object.h"
+
+using Genode::Phys_allocator;
+using Genode::Allocator;
+
+static Phys_allocator &phys_alloc_16k(Allocator * core_mem_alloc = nullptr)
+{
+ static Genode::Phys_allocator phys_alloc_16k(core_mem_alloc);
+ return phys_alloc_16k;
+}
+
+seL4_Word Genode::Untyped_memory::smallest_page_type() {
+ return seL4_ARM_SmallPageObject; }
+
+void Genode::Platform::init_sel4_ipc_buffer() { }
+
+long Genode::Platform::_unmap_page_frame(Cap_sel const &sel) {
+ return seL4_ARM_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 += 256 * get_page_size();
+ }
+
+ /* initialize 16k memory allocator */
+ phys_alloc_16k(core_mem_alloc());
+
+ /* reserve some memory for page directory construction - must be 16k on ARM */
+ enum { MAX_PROCESS_COUNT = 32 };
+ addr_t const max_pd_mem = MAX_PROCESS_COUNT * (1UL << Page_directory_kobj::SIZE_LOG2);
+
+ _initial_untyped_pool.turn_into_untyped_object(Core_cspace::TOP_CNODE_UNTYPED_16K,
+ [&] (addr_t const phys, addr_t const size, bool const device) {
+ phys_alloc_16k().add_range(phys, size);
+ _unused_phys_alloc.remove_range(phys, size);
+ },
+ Page_directory_kobj::SIZE_LOG2, max_pd_mem);
+
+ log(":phys_mem_16k: ", phys_alloc_16k());
+}
+
+Genode::addr_t Genode::Platform_pd::_init_page_directory()
+{
+ /* page directory table contains 4096 elements of 32bits -> 16k required */
+ enum { PAGES_16K = (1UL << Page_directory_kobj::SIZE_LOG2) / 4096 };
+
+ addr_t const phys_addr = Untyped_memory::alloc_pages(phys_alloc_16k(), PAGES_16K);
+ seL4_Untyped const service = Untyped_memory::_core_local_sel(Core_cspace::TOP_CNODE_UNTYPED_16K, phys_addr, Page_directory_kobj::SIZE_LOG2).value();
+
+ create(service,
+ platform_specific()->core_cnode().sel(),
+ _page_directory_sel);
+
+ long ret = seL4_ARM_ASIDPool_Assign(platform_specific()->asid_pool().value(),
+ _page_directory_sel.value());
+
+ if (ret != seL4_NoError)
+ error("seL4_ARM_ASIDPool_Assign returned ", ret);
+
+ return phys_addr;
+}
diff --git a/repos/base-sel4/src/core/spec/arm/thread.cc b/repos/base-sel4/src/core/spec/arm/thread.cc
new file mode 100644
index 0000000000..8db331b48f
--- /dev/null
+++ b/repos/base-sel4/src/core/spec/arm/thread.cc
@@ -0,0 +1,79 @@
+/*
+ * \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
+
+/* core includes */
+#include
+#include
+
+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(®s, 0, sizeof(regs));
+ size_t const num_regs = sizeof(regs)/sizeof(seL4_Word);
+
+ regs.pc = ip;
+ regs.sp = sp;
+
+ long const ret = seL4_TCB_WriteRegisters(tcb_sel.value(), false, 0,
+ num_regs, ®s);
+ 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.pc);
+
+ long const ret = seL4_TCB_ReadRegisters(thread, suspend_source, arch_flags,
+ register_count, ®isters);
+ 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.r0 = registers.r0;
+ state.r1 = registers.r1;
+ state.r2 = registers.r2;
+ state.r3 = registers.r3;
+ state.r4 = registers.r4;
+ state.r5 = registers.r5;
+ state.r6 = registers.r6;
+ state.r7 = registers.r7;
+ state.r8 = registers.r8;
+ state.r9 = registers.r9;
+ state.r10 = registers.r10;
+ state.r11 = registers.r11;
+ state.r12 = registers.r12;
+ state.sp = registers.sp;
+ state.lr = registers.r14;
+ state.ip = registers.pc;
+ state.cpsr = registers.cpsr;
+ state.cpu_exception = 0; /* XXX detect/track if in exception and report here */
+
+ return state;
+}
diff --git a/repos/base-sel4/src/core/spec/arm/vm_space.cc b/repos/base-sel4/src/core/spec/arm/vm_space.cc
new file mode 100644
index 0000000000..1b9d2e35f9
--- /dev/null
+++ b/repos/base-sel4/src/core/spec/arm/vm_space.cc
@@ -0,0 +1,66 @@
+/*
+ * \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
+
+#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_ARM_PageTable_Map(pagetable.value(), vroot.value(), virt,
+ seL4_ARM_Default_VMAttributes);
+}
+
+long Genode::Vm_space::_map_page(Genode::Cap_sel const &idx,
+ Genode::addr_t const virt,
+ Cache_attribute const cacheability,
+ bool const writable)
+{
+ seL4_ARM_Page const service = _idx_to_sel(idx.value());
+ seL4_ARM_PageDirectory const pd = _pd_sel.value();
+ seL4_CapRights_t const rights = writable ? seL4_ReadWrite : seL4_CanRead;
+ seL4_ARM_VMAttributes attr = seL4_ARM_Default_VMAttributes;
+
+ if (cacheability == UNCACHED)
+ attr = seL4_ARM_Uncacheable;
+
+ return seL4_ARM_Page_Map(service, pd, virt, rights, attr);
+}
+
+long Genode::Vm_space::_unmap_page(Genode::Cap_sel const &idx)
+{
+ seL4_ARM_Page const service = _idx_to_sel(idx.value());
+ return seL4_ARM_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;
+
+ /* 1 MB range - page table */
+ Cap_sel const pt = _alloc_and_map(virt, map_page_table, phys);
+ _page_table_registry.insert_page_table(virt, pt, phys,
+ PAGE_TABLE_LOG2_SIZE);
+ }
+}
diff --git a/repos/base-sel4/src/core/spec/x86/fault_info.h b/repos/base-sel4/src/core/spec/x86/fault_info.h
new file mode 100644
index 0000000000..fae42e868e
--- /dev/null
+++ b/repos/base-sel4/src/core/spec/x86/fault_info.h
@@ -0,0 +1,38 @@
+/*
+ * \brief x86 specific fault info
+ * \author Alexander Boettcher
+ * \date 2017-07-11
+ */
+
+/*
+ * 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.
+ */
+
+struct Fault_info
+{
+ Genode::addr_t ip = 0;
+ Genode::addr_t pf = 0;
+ bool write = 0;
+
+ /*
+ * Intel manual: 6.15 EXCEPTION AND INTERRUPT REFERENCE
+ * Interrupt 14—Page-Fault Exception (#PF)
+ */
+ enum {
+ ERR_I = 1 << 4,
+ ERR_R = 1 << 3,
+ ERR_U = 1 << 2,
+ ERR_W = 1 << 1,
+ ERR_P = 1 << 0,
+ };
+
+ Fault_info(seL4_MessageInfo_t msg_info)
+ :
+ ip(seL4_GetMR(0)),
+ pf(seL4_GetMR(1)),
+ write(seL4_GetMR(3) & ERR_W)
+ { }
+};
diff --git a/repos/base-sel4/src/core/spec/x86/irq.cc b/repos/base-sel4/src/core/spec/x86/irq.cc
new file mode 100644
index 0000000000..2ea442911a
--- /dev/null
+++ b/repos/base-sel4/src/core/spec/x86/irq.cc
@@ -0,0 +1,34 @@
+/*
+ * \brief Implementation of the platform specific IRQ association
+ * \author Alexander Boettcher
+ * \date 2017-07-07
+ */
+
+#include
+
+#include
+
+long Genode::Irq_object::_associate(Irq_session::Trigger const &irq_trigger,
+ Irq_session::Polarity const &irq_polarity)
+{
+ enum { IRQ_EDGE = 0, IRQ_LEVEL = 1 };
+ enum { IRQ_HIGH = 0, IRQ_LOW = 1 };
+
+ seL4_Word level = (_irq < 16) ? IRQ_EDGE : IRQ_LEVEL;
+ seL4_Word polarity = (_irq < 16) ? IRQ_HIGH : IRQ_LOW;
+
+ if (irq_trigger != Irq_session::TRIGGER_UNCHANGED)
+ level = (irq_trigger == Irq_session::TRIGGER_LEVEL) ? IRQ_LEVEL : IRQ_EDGE;
+
+ if (irq_polarity != Irq_session::POLARITY_UNCHANGED)
+ polarity = (irq_polarity == Irq_session::POLARITY_HIGH) ? IRQ_HIGH : IRQ_LOW;
+
+ seL4_CNode const root = seL4_CapInitThreadCNode;
+ seL4_Word const index = _kernel_irq_sel.value();
+ seL4_Uint8 const depth = 32;
+ seL4_Word const ioapic = 0;
+ seL4_Word const pin = _irq ? _irq : 2;
+ seL4_Word const vector = _irq;
+ return seL4_IRQControl_GetIOAPIC(seL4_CapIRQControl, root, index, depth,
+ ioapic, pin, level, polarity, vector);
+}
diff --git a/repos/base-sel4/src/core/spec/x86/vm_space.cc b/repos/base-sel4/src/core/spec/x86/vm_space.cc
new file mode 100644
index 0000000000..34f6d89e09
--- /dev/null
+++ b/repos/base-sel4/src/core/spec/x86/vm_space.cc
@@ -0,0 +1,40 @@
+/*
+ * \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
+
+long Genode::Vm_space::_map_page(Genode::Cap_sel const &idx,
+ Genode::addr_t const virt,
+ Cache_attribute const cacheability,
+ bool const writable)
+{
+ seL4_X86_Page const service = _idx_to_sel(idx.value());
+ seL4_X86_PageDirectory const pd = _pd_sel.value();
+ seL4_CapRights_t const rights = writable ? seL4_ReadWrite : seL4_CanRead;
+ seL4_X86_VMAttributes attr = seL4_X86_Default_VMAttributes;
+
+ if (cacheability == UNCACHED)
+ attr = seL4_X86_Uncacheable;
+ else
+ if (cacheability == WRITE_COMBINED)
+ attr = seL4_X86_WriteCombining;
+
+ 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);
+}
diff --git a/repos/base-sel4/src/core/spec/x86_32/vm_space.cc b/repos/base-sel4/src/core/spec/x86_32/vm_space.cc
index 8c470a601a..c67a953e01 100644
--- a/repos/base-sel4/src/core/spec/x86_32/vm_space.cc
+++ b/repos/base-sel4/src/core/spec/x86_32/vm_space.cc
@@ -18,29 +18,12 @@
static long map_page_table(Genode::Cap_sel const pagetable,
Genode::Cap_sel const vroot,
- Genode::addr_t const virt)
+ 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)
{
diff --git a/repos/base-sel4/src/core/spec/x86_64/vm_space.cc b/repos/base-sel4/src/core/spec/x86_64/vm_space.cc
index b1d156f339..de206eeaa1 100644
--- a/repos/base-sel4/src/core/spec/x86_64/vm_space.cc
+++ b/repos/base-sel4/src/core/spec/x86_64/vm_space.cc
@@ -40,23 +40,6 @@ static long map_directory(Genode::Cap_sel const pd,
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)
{
diff --git a/repos/base/run/slab.run b/repos/base/run/slab.run
index d96b8c3124..1c9a55f1ba 100644
--- a/repos/base/run/slab.run
+++ b/repos/base/run/slab.run
@@ -22,7 +22,7 @@ install_config {
-
+
diff --git a/repos/dde_rump/run/rump_ext2.run b/repos/dde_rump/run/rump_ext2.run
index 3b8bc9d929..510890e5e1 100644
--- a/repos/dde_rump/run/rump_ext2.run
+++ b/repos/dde_rump/run/rump_ext2.run
@@ -84,7 +84,7 @@ install_config $config
set boot_modules {
core ld.lib.so init timer test-libc_vfs ram_blk
rump.lib.so rump_fs.lib.so rump_fs
- ext2.raw libc.lib.so libm.lib.so
+ ext2.raw libc.lib.so
}
build_boot_image $boot_modules
diff --git a/repos/gems/run/cpu_sampler.run b/repos/gems/run/cpu_sampler.run
index 48a82af46a..994eead6a6 100644
--- a/repos/gems/run/cpu_sampler.run
+++ b/repos/gems/run/cpu_sampler.run
@@ -27,6 +27,7 @@ install_config {
+
diff --git a/repos/gems/run/cpu_sampler_noux.run b/repos/gems/run/cpu_sampler_noux.run
index a0e40e927d..f37ccdcc7f 100644
--- a/repos/gems/run/cpu_sampler_noux.run
+++ b/repos/gems/run/cpu_sampler_noux.run
@@ -6,7 +6,7 @@ if { ![have_spec foc] && ![have_spec nova] &&
set build_components {
core init drivers/timer noux/minimal lib/libc_noux
- drivers/framebuffer drivers/input
+ drivers/input
server/terminal server/ram_fs
server/log_terminal
test/libports/ncurses
@@ -15,6 +15,8 @@ set build_components {
test/cpu_sampler
}
+lappend_if [have_spec framebuffer] build_components drivers/framebuffer
+
if {[have_spec foc] || [have_spec nova]} {
lappend build_components lib/cpu_sampler_platform-$::env(KERNEL)
} else {
diff --git a/repos/os/run/fb_bench.run b/repos/os/run/fb_bench.run
index 10dec62dd9..4d4bf9f7b5 100644
--- a/repos/os/run/fb_bench.run
+++ b/repos/os/run/fb_bench.run
@@ -72,7 +72,7 @@ append_if [have_spec sdl] config {
append_platform_drv_config
append_if [have_spec framebuffer] config {
-
+
}
diff --git a/repos/os/run/fs_log.run b/repos/os/run/fs_log.run
index dd2c9d0a97..a4720811c7 100644
--- a/repos/os/run/fs_log.run
+++ b/repos/os/run/fs_log.run
@@ -20,6 +20,7 @@ set config {
+
diff --git a/repos/os/run/sd_card_bench.run b/repos/os/run/sd_card_bench.run
index 1a468ba61f..70f07a20d1 100644
--- a/repos/os/run/sd_card_bench.run
+++ b/repos/os/run/sd_card_bench.run
@@ -3,7 +3,8 @@
#
if {[have_spec pl180]} { set buffer_size_kib [expr 12 * 1024]
-} elseif {[have_spec imx6]} { set buffer_size_kib [expr 1024]
+} elseif {[have_spec imx6] &&
+ ![have_spec sel4]} { set buffer_size_kib [expr 1024]
} elseif {[have_spec imx53] &&
![have_spec foc]} { set buffer_size_kib [expr 1024]
} elseif {[have_spec rpi]} { set buffer_size_kib [expr 4 * 1024]
diff --git a/tool/builddir/build.conf/run_kernel_wand_quad b/tool/builddir/build.conf/run_kernel_wand_quad
new file mode 100644
index 0000000000..96b6f17cf4
--- /dev/null
+++ b/tool/builddir/build.conf/run_kernel_wand_quad
@@ -0,0 +1,3 @@
+# kernel to use (hw, sel4)
+# KERNEL ?= hw
+
diff --git a/tool/create_builddir b/tool/create_builddir
index c91b40c56b..2f903d2d43 100755
--- a/tool/create_builddir
+++ b/tool/create_builddir
@@ -142,7 +142,7 @@ BUILD_CONF(arndale) := run_kernel_hw_foc run_boot_dir repos
BUILD_CONF(imx53_qsb) := run_kernel_hw run_boot_dir repos
BUILD_CONF(imx53_qsb_tz) := run_kernel_hw run_boot_dir repos
BUILD_CONF(usb_armory) := run_kernel_hw run_boot_dir repos
-BUILD_CONF(wand_quad) := run_kernel_hw run_boot_dir repos
+BUILD_CONF(wand_quad) := run_kernel_wand_quad run_boot_dir repos
BUILD_CONF(odroid_xu) := run_kernel_hw run_boot_dir repos
BUILD_CONF(odroid_x2) := run_kernel_foc run_boot_dir repos
BUILD_CONF(zynq_qemu) := run_kernel_hw run_qemu run_opt_hw run_boot_dir qemu_opt_arm repos
diff --git a/tool/run/boot_dir/sel4 b/tool/run/boot_dir/sel4
index 5efb321810..d4d7a29025 100644
--- a/tool/run/boot_dir/sel4
+++ b/tool/run/boot_dir/sel4
@@ -1,13 +1,19 @@
proc binary_name_ld_lib_so { } { return "ld-sel4.lib.so" }
proc binary_name_core_o { } { return "core-sel4.o" }
-proc binary_name_timer { } { return "pit_timer_drv" }
+proc binary_name_timer { } {
+ if {[have_spec wand_quad]} { return "wand_quad_timer_drv" }
+ if {[have_spec x86]} { return "pit_timer_drv" }
+ puts "unknown platform - no timer driver"
+ exit -1
+}
proc kernel_files { } { return sel4 }
-proc run_boot_string { } { return "\n\rStarting node #0" }
+proc run_boot_string { } { return "\n\rBooting all finished, dropped to user space" }
proc core_link_address { } { return "0x02000000" }
+proc sel4_elfloader_dir { } { return "[pwd]/var/libcache/kernel-sel4/elfloader" }
##
# Populate boot directory with binaries on hw
@@ -59,9 +65,35 @@ proc run_boot_dir {binaries} {
close $fh
}
+ #
+ # Use seL4 elfloader tool to generate bootable image on ARM
+ #
+ if {[have_spec arm]} {
+ if {![have_spec imx6]} {
+ puts "abort - unknown ARM board"
+ exit 1
+ }
+ # keep Genode image.elf as genode.elf
+ exec mv [run_dir]/image.elf [run_dir]/genode.elf
+
+ # call seL4 elfloader tool to generate image.elf bootable by uboot with 'bootelf' command
+ set ::env(PLAT) imx6
+ set ::env(TOOLPREFIX) [cross_dev_prefix]
+ exec [sel4_elfloader_dir]/gen_boot_image.sh [run_dir]/sel4 [run_dir]/genode.elf [run_dir]/image.elf
+ }
+
run_image [run_dir]/image.elf
- if {[have_include "load/tftp"]} {
+ # set symbolic link to image.elf file in TFTP directory for PXE boot
+ if {[have_spec arm] && [have_include "load/tftp"]} {
+ exec ln -sf [pwd]/[run_dir]/image.elf [load_tftp_base_dir][load_tftp_offset_dir]
+
+ if {[have_include "image/uboot"]} {
+ exec ln -sf [pwd]/[run_dir]/uImage [load_tftp_base_dir][load_tftp_offset_dir]
+ }
+ }
+
+ if {[have_spec x86] && [have_include "load/tftp"]} {
#
# Install PXE bootloader pulsar
#
@@ -79,7 +111,7 @@ proc run_boot_dir {binaries} {
generate_tftp_config
}
- if {[have_include "load/ipxe"]} {
+ if {[have_spec x86] && [have_include "load/ipxe"]} {
create_ipxe_iso_config
update_ipxe_boot_dir
create_symlink_for_iso