sel4: add Wandboard Quad (iMX6) support

Issue #2451

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

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

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

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

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

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)

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
+

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

repos/base-sel4/lib/mk/spec/x86/base-sel4.mk

@@ -0,0 +1,3 @@
+LIBS += timeout
+
+include $(REP_DIR)/lib/mk/base-sel4.inc

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

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

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 \

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,

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 {

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

repos/base-sel4/ports/sel4.hash

@@ -1 +1 @@
-3858de13ad9db6b4fa5e21c8a246180aec74571c
+7dc762b776af1721d742d70f6394f6177436817a

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

repos/base-sel4/ports/sel4_elfloader.hash

@@ -0,0 +1 @@
+cf90c5aba6d10a0582d53ada6aed06c96ec585b5

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)

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 inline unsigned long untyped_cnode_4k()   { return phys_cnode_sel() + 1; }
-		static unsigned long core_static_sel_end()       { return untyped_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_UNTYPED_16K = 0xffd, /* untyped objects 16K  */
-			TOP_CNODE_PHYS_IDX    = 0xfff  /* phyical page frames */
+			TOP_CNODE_UNTYPED_4K  = 0xffe, /* untyped objects  4K  */
+			TOP_CNODE_PHYS_IDX    = 0xfff  /* physical page frames */
 		};
 
 		enum { CORE_VM_ID = 1 };

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_ */

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

@@ -18,16 +18,22 @@
 #include <base/ipc.h>
 #include <base/stdint.h>
 
+namespace Genode { class Ipc_pager; }
+
 namespace Genode {
 
 	class Mapping
 	{
+		friend class Ipc_pager;
+
 		private:
 
-			addr_t _from_phys_addr;
+			addr_t          _from_phys_addr;
-			addr_t _to_virt_addr;
+			addr_t          _to_virt_addr;
-			size_t _num_pages;
+			Cache_attribute _attr;
-			bool   _writeable;
+			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

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

@@ -15,6 +15,7 @@
 #define _CORE__INCLUDE__IRQ_OBJECT_H_
 
 #include <base/thread.h>
+#include <base/internal/capability_space_sel4.h>
 #include <irq_session/irq_session.h>
 
 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);

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;
 		}

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) {

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
 		{

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_ */

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

@@ -180,7 +180,7 @@ class Genode::Platform_thread : public List<Platform_thread>::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_ */

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);
 	}
 
 

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,
+		void map(addr_t const from_phys, addr_t const to_virt,
-		         bool flush_support = true)
+		         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_ */

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 };
+	/* setup IRQ platform specific */
-	enum { IRQ_HIGH = 0, IRQ_LOW = 1 };
+	long res = _associate(irq_trigger, irq_polarity);
-
-	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);
 	if (res != seL4_NoError)
 		return false;
 

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

@@ -20,28 +20,13 @@
 /* base-internal includes */
 #include <base/internal/capability_space_sel4.h>
 
+#include "fault_info.h"
+
 /* seL4 includes */
 #include <sel4/sel4.h>
-#include <sel4/arch/pfIPC.h>
 
 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)
+	if (_badge)
-		install_mapping(_reply_mapping, _last);
+		_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_ip      = fault_info.ip;
-	_pf_addr  = fault_info.pf;
+	_pf_addr    = fault_info.pf;
-	_pf_write = fault_info.write;
+	_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) { }
 
 
 /******************

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()),
+	_top_cnode.copy(initial_cspace, Cnode_index(Core_cspace::untyped_cnode_4k()),
-	                                Cnode_index(Core_cspace::TOP_CNODE_UNTYPED_IDX));
+	                                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 */
 	{

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());
+		if (mapping.fault_type() != seL4_Fault_VMFault)
-		_vm_space.map(mapping.from_phys(), mapping.to_virt(), mapping.num_pages());
+			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;
 	}
 }
 

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)
+				if (t->pager_object_badge() == pager_object_badge) {
-					t->install_mapping(mapping);
+					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<Address_space> 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());
 }
 
 

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 <sel4/objecttype.h>
+
+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_ */

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 <base/stdint.h>
+
+/* core includes */
+#include <sel4_boot_info.h>
+
+
+/* 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;
+}

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)))
+	{ }
+};

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 <irq_object.h>
+
+#include <sel4/sel4.h>
+
+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);
+}

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 <base/internal/crt0.h>
+
+/* core includes */
+#include <platform.h>
+#include <platform_pd.h>
+
+#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<Page_directory_kobj>(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;
+}

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 <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.pc = ip;
+	regs.sp = 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.pc);
+
+	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.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;
+}

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 <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_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<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/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)
+	{ }
+};

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 <irq_object.h>
+
+#include <sel4/sel4.h>
+
+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);
+}

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 <vm_space.h>
+
+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);
+}

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)
 {

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)
 {

repos/base/run/slab.run

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

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

repos/gems/run/cpu_sampler.run

@@ -27,6 +27,7 @@ install_config {
 		<parent-provides>
 			<service name="CPU"/>
 			<service name="IO_PORT"/>
+			<service name="IO_MEM"/>
 			<service name="IRQ"/>
 			<service name="LOG"/>
 			<service name="PD"/>

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 {

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 {
-	<start name="fb_drv">
+	<start name="fb_drv" caps="150">
 		<resource name="RAM" quantum="20M"/>
 		<provides><service name="Framebuffer"/></provides>
 	</start>}

repos/os/run/fs_log.run

@@ -20,6 +20,7 @@ set config {
 		<service name="RM"/>
 		<service name="ROM"/>
 		<service name="IO_PORT"/>
+		<service name="IO_MEM"/>
 		<service name="IRQ"/>
 	</parent-provides>
 	<default-route>

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]

tool/builddir/build.conf/run_kernel_wand_quad

@@ -0,0 +1,3 @@
+# kernel to use (hw, sel4)
+# KERNEL ?= hw
+

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

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