diff --git a/repos/base-sel4/src/core/include/cnode.h b/repos/base-sel4/src/core/include/cnode.h
new file mode 100644
index 000000000..550570e24
--- /dev/null
+++ b/repos/base-sel4/src/core/include/cnode.h
@@ -0,0 +1,181 @@
+/*
+ * \brief Utilities for manipulating seL4 CNodes
+ * \author Norman Feske
+ * \date 2015-05-04
+ */
+
+/*
+ * Copyright (C) 2015 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#ifndef _CORE__INCLUDE__CNODE_H_
+#define _CORE__INCLUDE__CNODE_H_
+
+/* Genode includes */
+#include
+#include
+
+/* core includes */
+#include
+
+namespace Genode {
+
+ class Cnode_base;
+ class Cnode;
+}
+
+
+class Genode::Cnode_base
+{
+ private:
+
+ unsigned const _sel;
+ size_t const _size_log2;
+
+ public:
+
+ unsigned sel() const { return _sel; }
+ size_t size_log2() const { return _size_log2; }
+
+ /**
+ * Return size of underlying backing store in bytes
+ *
+ * One cnode entry takes 16 (2^4) bytes.
+ */
+ size_t mem_size_log2() const { return _size_log2 + 4; }
+
+ /**
+ * Copy selector from another CNode
+ */
+ void copy(Cnode_base const &from, unsigned from_idx, unsigned to_idx)
+ {
+ seL4_CNode const service = sel();
+ seL4_Word const dest_index = to_idx;
+ uint8_t const dest_depth = size_log2();
+ seL4_CNode const src_root = from.sel();
+ seL4_Word const src_index = from_idx;
+ uint8_t const src_depth = from.size_log2();
+ seL4_CapRights const rights = seL4_AllRights;
+
+ int const ret = seL4_CNode_Copy(service, dest_index, dest_depth,
+ src_root, src_index, src_depth, rights);
+ if (ret != 0) {
+ PWRN("%s: seL4_CNode_Copy (0x%x) returned %d", __FUNCTION__,
+ from_idx, ret);
+ }
+ }
+
+ void copy(Cnode_base const &from, unsigned idx) { copy(from, idx, idx); }
+
+ /**
+ * Move selector from another CNode
+ */
+ void move(Cnode_base const &from, unsigned from_idx, unsigned to_idx)
+ {
+ seL4_CNode const service = sel();
+ seL4_Word const dest_index = to_idx;
+ uint8_t const dest_depth = size_log2();
+ seL4_CNode const src_root = from.sel();
+ seL4_Word const src_index = from_idx;
+ uint8_t const src_depth = from.size_log2();
+
+ int const ret = seL4_CNode_Move(service, dest_index, dest_depth,
+ src_root, src_index, src_depth);
+ if (ret != 0) {
+ PWRN("%s: seL4_CNode_Move (0x%x) returned %d", __FUNCTION__,
+ from_idx, ret);
+ }
+ }
+
+ void move(Cnode_base const &from, unsigned idx) { move(from, idx, idx); }
+
+ /**
+ * Constructor
+ */
+ Cnode_base(unsigned sel, size_t size_log2)
+ : _sel(sel), _size_log2(size_log2) { }
+};
+
+
+class Genode::Cnode : public Cnode_base
+{
+ public:
+
+ class Phys_alloc_failed : Exception { };
+ class Untyped_lookup_failed : Exception { };
+ class Retype_untyped_failed : Exception { };
+
+ /**
+ * Constructor
+ *
+ * \param dst_sel designated selector referring to the created
+ * CNode
+ * \param size_log2 number of entries in CNode
+ * \param phys_alloc physical-memory allocator used for allocating
+ * the CNode backing store
+ *
+ * \throw Phys_alloc_failed
+ * \throw Untyped_address::Lookup_failed
+ */
+ Cnode(unsigned dst_sel, size_t size_log2, Range_allocator &phys_alloc)
+ :
+ Cnode_base(dst_sel, size_log2)
+ {
+ /*
+ * Allocate natually-aligned physical memory for cnode
+ *
+ * The natual alignment is needed to ensure that the backing store is
+ * contained in a single untyped memory region.
+ */
+ void *out_ptr = nullptr;
+ size_t const mem_size = 1UL << mem_size_log2();
+ Range_allocator::Alloc_return alloc_ret =
+ phys_alloc.alloc_aligned(mem_size, &out_ptr, mem_size_log2());
+ addr_t const phys_addr = (addr_t)out_ptr;
+
+ if (alloc_ret.is_error()) {
+ PERR("%s: allocation of backing store for cnode failed", __FUNCTION__);
+ throw Phys_alloc_failed();
+ }
+
+ Untyped_address const untyped_addr(phys_addr, mem_size);
+
+ seL4_Untyped const service = untyped_addr.sel();
+ int const type = seL4_CapTableObject;
+ int const offset = untyped_addr.offset();
+ int const size_bits = size_log2;
+ seL4_CNode const root = seL4_CapInitThreadCNode;
+ int const node_index = 0;
+ int const node_depth = 0;
+ int const node_offset = dst_sel;
+ int const num_objects = 1;
+
+ int const ret = seL4_Untyped_RetypeAtOffset(service,
+ type,
+ offset,
+ size_bits,
+ root,
+ node_index,
+ node_depth,
+ node_offset,
+ num_objects);
+ if (ret != 0) {
+ PERR("seL4_Untyped_RetypeAtOffset (CapTable) returned %d", ret);
+ throw Retype_untyped_failed();
+ }
+ }
+
+ ~Cnode()
+ {
+ /* convert CNode back to untyped memory */
+
+ /* revert phys allocation */
+
+ PDBG("not implemented");
+ }
+};
+
+#endif /* _CORE__INCLUDE__CNODE_H_ */
diff --git a/repos/base-sel4/src/core/include/untyped_address.h b/repos/base-sel4/src/core/include/untyped_address.h
new file mode 100644
index 000000000..d31ad5069
--- /dev/null
+++ b/repos/base-sel4/src/core/include/untyped_address.h
@@ -0,0 +1,98 @@
+/*
+ * \brief Utilities for manipulating seL4 CNodes
+ * \author Norman Feske
+ * \date 2015-05-04
+ */
+
+/*
+ * Copyright (C) 2015 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#ifndef _CORE__INCLUDE__UNTYPED_ADDRESS_H_
+#define _CORE__INCLUDE__UNTYPED_ADDRESS_H_
+
+/* seL4 includes */
+#include
+#include
+
+namespace Genode { struct Untyped_address; }
+
+
+/**
+ * Obtain seL4 boot info structure
+ */
+static inline seL4_BootInfo const &sel4_boot_info()
+{
+ extern Genode::addr_t __initial_bx;
+ return *(seL4_BootInfo const *)__initial_bx;
+}
+
+
+/**
+ * Untuped memory address
+ *
+ * When referring to physical memory in seL4 system-call arguments, a memory
+ * address is specified as a tuple of an untyped memory range selector and the
+ * offset relative to the base address of the untyped memory range.
+ */
+class Genode::Untyped_address
+{
+ private:
+
+ seL4_Untyped _sel = 0;
+ addr_t _offset = 0;
+
+ void _init(seL4_BootInfo const &bi, addr_t phys_addr, size_t size,
+ unsigned const start_idx, unsigned const num_idx)
+ {
+
+ for (unsigned i = start_idx; i < start_idx + num_idx; i++) {
+
+ /* index into 'untypedPaddrList' and 'untypedSizeBitsList' */
+ unsigned const k = i - bi.untyped.start;
+
+ addr_t const untyped_base = bi.untypedPaddrList[k];
+ size_t const untyped_size = 1UL << bi.untypedSizeBitsList[k];
+
+ if (phys_addr >= untyped_base
+ && phys_addr + size - 1 <= untyped_base + untyped_size - 1) {
+
+ _sel = i;
+ _offset = phys_addr - untyped_base;
+ return;
+ }
+ }
+ }
+
+ public:
+
+ class Lookup_failed { };
+
+ /**
+ * Construct untyped address for given physical address range
+ *
+ * \throw Lookup_failed
+ */
+ Untyped_address(addr_t phys_addr, size_t size)
+ {
+ seL4_BootInfo const &bi = sel4_boot_info();
+ _init(bi, phys_addr, size, bi.untyped.start,
+ bi.untyped.end - bi.untyped.start);
+
+ /* XXX handle untyped device addresses */
+
+ if (_sel == 0) {
+ PERR("could not find untyped address for 0x%lx", phys_addr);
+ throw Lookup_failed();
+ }
+ }
+
+ unsigned sel() const { return _sel; }
+ addr_t offset() const { return _offset; }
+};
+
+
+#endif /* _CORE__INCLUDE__UNTYPED_ADDRESS_H_ */
diff --git a/repos/base-sel4/src/core/platform.cc b/repos/base-sel4/src/core/platform.cc
index 200a353b4..50dca3153 100644
--- a/repos/base-sel4/src/core/platform.cc
+++ b/repos/base-sel4/src/core/platform.cc
@@ -20,10 +20,7 @@
#include
#include
#include
-
-/* seL4 includes */
-#include
-#include
+#include
using namespace Genode;
@@ -61,17 +58,6 @@ bool Core_mem_allocator::Mapped_mem_allocator::_unmap_local(addr_t virt_addr,
** Platform interface **
************************/
-
-/**
- * Obtain seL4 boot info structure
- */
-static seL4_BootInfo const &sel4_boot_info()
-{
- extern Genode::addr_t __initial_bx;
- return *(seL4_BootInfo const *)__initial_bx;
-}
-
-
/**
* Initialize allocator with untyped memory ranges according to the boot info
*/
@@ -91,6 +77,112 @@ static void init_allocator(Range_allocator &alloc, seL4_BootInfo const &bi,
}
+static inline void init_sel4_ipc_buffer()
+{
+ asm volatile ("movl %0, %%gs" :: "r"(IPCBUF_GDT_SELECTOR) : "memory");
+}
+
+
+/* CNode dimensions */
+enum {
+ NUM_TOP_SEL_LOG2 = 12UL,
+ NUM_CORE_SEL_LOG2 = 14UL,
+ NUM_PHYS_SEL_LOG2 = 20UL,
+};
+
+
+/* selectors for statically created CNodes */
+enum Static_cnode_sel {
+ TOP_CNODE_SEL = 0x200,
+ CORE_PAD_CNODE_SEL = 0x201,
+ CORE_CNODE_SEL = 0x202,
+ PHYS_CNODE_SEL = 0x203
+};
+
+
+/* indices within top-level CNode */
+enum Top_cnode_idx {
+ TOP_CNODE_CORE_IDX = 0,
+ TOP_CNODE_PHYS_IDX = 0xfff
+};
+
+
+/**
+ * Replace initial CSpace with custom CSpace layout
+ */
+static void switch_to_core_cspace(Range_allocator &phys_alloc)
+{
+ Cnode_base const initial_cspace(seL4_CapInitThreadCNode, 32);
+
+ /* allocate 1st-level CNode */
+ static Cnode top_cnode(TOP_CNODE_SEL, NUM_TOP_SEL_LOG2, phys_alloc);
+
+ /* allocate 2nd-level CNode to align core's CNode with the LSB of the CSpace*/
+ static Cnode core_pad_cnode(CORE_PAD_CNODE_SEL,
+ 32UL - NUM_TOP_SEL_LOG2 - NUM_CORE_SEL_LOG2,
+ phys_alloc);
+
+ /* allocate 3rd-level CNode for core's objects */
+ static Cnode core_cnode(CORE_CNODE_SEL, NUM_CORE_SEL_LOG2, phys_alloc);
+
+ /* copy initial selectors to core's CNode */
+ core_cnode.copy(initial_cspace, seL4_CapInitThreadTCB);
+ core_cnode.copy(initial_cspace, seL4_CapInitThreadCNode);
+ core_cnode.copy(initial_cspace, seL4_CapInitThreadPD);
+ core_cnode.move(initial_cspace, seL4_CapIRQControl); /* cannot be copied */
+ core_cnode.copy(initial_cspace, seL4_CapIOPort);
+ core_cnode.copy(initial_cspace, seL4_CapBootInfoFrame);
+ core_cnode.copy(initial_cspace, seL4_CapArchBootInfoFrame);
+ core_cnode.copy(initial_cspace, seL4_CapInitThreadIPCBuffer);
+ core_cnode.copy(initial_cspace, seL4_CapIPI);
+ core_cnode.copy(initial_cspace, seL4_CapDomain);
+
+ /* copy untyped memory selectors to core's CNode */
+ seL4_BootInfo const &bi = sel4_boot_info();
+
+ for (unsigned sel = bi.untyped.start; sel < bi.untyped.end; sel++)
+ core_cnode.copy(initial_cspace, sel);
+
+ for (unsigned sel = bi.deviceUntyped.start; sel < bi.deviceUntyped.end; sel++)
+ core_cnode.copy(initial_cspace, sel);
+
+ /* copy statically created CNode selectors to core's CNode */
+ core_cnode.copy(initial_cspace, TOP_CNODE_SEL);
+ core_cnode.copy(initial_cspace, CORE_PAD_CNODE_SEL);
+ core_cnode.copy(initial_cspace, CORE_CNODE_SEL);
+
+ /*
+ * Construct CNode hierarchy of core's CSpace
+ */
+
+ /* insert 3rd-level core CNode into 2nd-level core-pad CNode */
+ core_pad_cnode.copy(initial_cspace, CORE_CNODE_SEL, 0);
+
+ /* insert 2nd-level core-pad CNode into 1st-level CNode */
+ top_cnode.copy(initial_cspace, CORE_PAD_CNODE_SEL, TOP_CNODE_CORE_IDX);
+
+ /* allocate 2nd-level CNode for storing page-frame cap selectors */
+ static Cnode phys_cnode(PHYS_CNODE_SEL, NUM_PHYS_SEL_LOG2, phys_alloc);
+
+ /* insert 2nd-level phys-mem CNode into 1st-level CNode */
+ top_cnode.copy(initial_cspace, PHYS_CNODE_SEL, TOP_CNODE_PHYS_IDX);
+
+ /* activate core's CSpace */
+ {
+ seL4_CapData_t null_data = { { 0 } };
+
+ int const ret = seL4_TCB_SetSpace(seL4_CapInitThreadTCB,
+ seL4_CapNull, /* fault_ep */
+ TOP_CNODE_SEL, null_data,
+ seL4_CapInitThreadPD, null_data);
+
+ if (ret != 0) {
+ PERR("%s: seL4_TCB_SetSpace returned %d", __FUNCTION__, ret);
+ }
+ }
+}
+
+
Platform::Platform()
:
_io_mem_alloc(core_mem_alloc()), _io_port_alloc(core_mem_alloc()),
@@ -134,6 +226,18 @@ Platform::Platform()
_core_mem_alloc.virt_alloc()->remove_range(Native_config::context_area_virtual_base(),
Native_config::context_area_virtual_size());
+ /*
+ * Until this point, no interaction with the seL4 kernel was needed.
+ * However, the next steps involve the invokation of system calls and
+ * the use of kernel services. To use the kernel bindings, we first
+ * need to initialize the TLS mechanism that is used to find the IPC
+ * buffer for the calling thread.
+ */
+ init_sel4_ipc_buffer();
+
+ /* initialize core's capability space */
+ switch_to_core_cspace(*_core_mem_alloc.phys_alloc());
+
/* add boot modules to ROM fs */
/*