sel4: capability lifetime management

repos/base-sel4/include/base/native_types.h

@@ -19,40 +19,101 @@
 
 namespace Genode {
 
-	struct Cap_dst_policy
-	{
-		typedef int Dst;
-		static bool valid(Dst tid) { return false; }
-		static Dst  invalid()      { return true; }
-		static void copy(void* dst, Native_capability_tpl<Cap_dst_policy>* src);
-	};
-
-	class Platform_thread;
-
 	typedef int Native_thread_id;
 
 	struct Native_thread
 	{
 		unsigned tcb_sel = 0;
-
-		/**
-		 * Only used in core
-		 *
-		 * For 'Thread' objects created within core, 'pt' points to
-		 * the physical thread object, which is going to be destroyed
-		 * on destruction of the 'Thread'.
-		 */
-		Platform_thread *pt = nullptr;
+		unsigned ep_sel  = 0;
+		unsigned rcv_sel = 0;
 	};
 
-	typedef Native_capability_tpl<Cap_dst_policy> Native_capability;
+	class Native_capability
+	{
+		public:
+
+			/*
+			 * XXX remove dependency in 'process.cc' and 'core_env.h' from
+			 * 'Raw', 'Dst', and the 'dst' member.
+			 */
+			typedef int Dst;
+			struct Raw { Dst dst = 0; long local_name = 0; };
+			Dst dst() const { return 0; }
+
+			/**
+			 * Forward declaration of the platform-specific internal capability
+			 * representation
+			 */
+			class Data;
+
+		private:
+
+			Data *_data = nullptr;
+
+		protected:
+
+			void _inc();
+			void _dec();
+
+		public:
+
+			/**
+			 * Default constructor creates an invalid capability
+			 */
+			Native_capability() { }
+
+			/**
+			 * Copy constructor
+			 */
+			Native_capability(const Native_capability &other)
+			: _data(other._data) { _inc(); }
+
+			/**
+			 * Construct capability manually
+			 *
+			 * This constructor is used internally.
+			 *
+			 * \noapi
+			 */
+			Native_capability(Data &data) : _data(&data) { _inc(); }
+
+			/**
+			 * Destructor
+			 */
+			~Native_capability() { _dec(); }
+
+			Data const *data() const { return _data; }
+
+			/**
+			 * Overloaded comparision operator
+			 */
+			bool operator == (const Native_capability &o) const
+			{
+				return _data == o._data;
+			}
+
+			Native_capability& operator = (const Native_capability &o)
+			{
+				if (this == &o)
+					return *this;
+
+				_dec();
+				_data = o._data;
+				_inc();
+				return *this;
+			}
+
+			long local_name() const;
+
+			bool valid() const;
+	};
 
 	class Native_utcb
 	{
 		private:
 
 			/**
-			 * On seL4 the UTCB is called IPC buffer. We use one page
+			 * On seL4, the UTCB is called IPC buffer. We use one page
 			 * for each IPC buffer.
 			 */
 			enum { IPC_BUFFER_SIZE = 4096 };

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

@@ -24,8 +24,9 @@ SRC_CC += thread/trace.cc
 SRC_CC += thread/myself.cc
 SRC_CC += thread/context_allocator.cc
 SRC_CC += thread/thread_bootstrap.cc
-#SRC_CC += env/cap_map.cc
+SRC_CC += env/capability.cc
 
+INC_DIR +=  $(REP_DIR)/src/base
 INC_DIR +=  $(REP_DIR)/src/base/lock
 INC_DIR += $(BASE_DIR)/src/base/thread
 

repos/base-sel4/src/base/env/capability.cc

@@ -0,0 +1,48 @@
+/*
+ * \brief  Capability lifetime management
+ * \author Norman Feske
+ * \date   2015-05-06
+ */
+
+/*
+ * 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.
+ */
+
+/* base includes */
+#include <base/printf.h>
+
+/* base-internal includes */
+#include <internal/native_types.h>
+#include <internal/capability_space.h>
+
+using namespace Genode;
+
+
+void Native_capability::_inc()
+{
+	if (_data)
+		Capability_space::inc_ref(*_data);
+}
+
+
+void Native_capability::_dec()
+{
+	if (_data)
+		Capability_space::dec_ref(*_data);
+}
+
+
+long Native_capability::local_name() const
+{
+	return _data ? Capability_space::rpc_obj_key(*_data).value() : 0;
+}
+
+
+bool Native_capability::valid() const
+{
+	return _data != 0;
+}
+

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

@@ -0,0 +1,84 @@
+/*
+ * \brief  Instance of the component's local capability space
+ * \author Norman Feske
+ * \date   2015-05-08
+ */
+
+/*
+ * 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.
+ */
+
+/* base includes */
+#include <base/native_types.h>
+#include <base/printf.h>
+
+/* base-internal includes */
+#include <internal/capability_data.h>
+#include <internal/capability_space_sel4.h>
+
+
+/**
+ * Definition of capability meta data
+ */
+struct Genode::Native_capability::Data : Capability_data
+{
+	Data(Rpc_obj_key key) : Capability_data(key) { }
+
+	Data() { }
+};
+
+
+using namespace Genode;
+
+
+/**
+ * Singleton instance of core-specific capability space
+ */
+namespace {
+
+	struct Local_capability_space
+	:
+		Capability_space_sel4<8*1024, Native_capability::Data>
+	{ };
+
+	static Local_capability_space &local_capability_space()
+	{
+		static Local_capability_space capability_space;
+		return capability_space;
+	}
+}
+
+
+/******************************************************
+ ** Implementation of the Capability_space interface **
+ ******************************************************/
+
+Native_capability::Data &Capability_space::create_ep_cap(Thread_base &ep_thread)
+{
+	unsigned const ep_sel = ep_thread.tid().ep_sel;
+
+	return local_capability_space().create_capability(ep_sel,
+	                                                  Rpc_obj_key());
+}
+
+
+void Capability_space::dec_ref(Native_capability::Data &data)
+{
+	local_capability_space().dec_ref(data);
+}
+
+
+void Capability_space::inc_ref(Native_capability::Data &data)
+{
+	local_capability_space().inc_ref(data);
+}
+
+
+Rpc_obj_key Capability_space::rpc_obj_key(Native_capability::Data const &data)
+{
+	return local_capability_space().rpc_obj_key(data);
+}
+

repos/base-sel4/src/base/internal/capability_data.h

@@ -0,0 +1,47 @@
+/*
+ * \brief  Capability meta data that is common for core and non-core components
+ * \author Norman Feske
+ * \date   2015-05-06
+ */
+
+/*
+ * 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 _BASE__INTERNAL__CAPABILITY_DATA_H_
+#define _BASE__INTERNAL__CAPABILITY_DATA_H_
+
+/* base includes */
+#include <util/noncopyable.h>
+#include <util/avl_tree.h>
+
+/* base-internal includes */
+#include <internal/rpc_obj_key.h>
+
+namespace Genode { class Capability_data; }
+
+
+class Genode::Capability_data
+{
+	private:
+
+		uint8_t     _ref_cnt = 0;  /* reference counter */
+		Rpc_obj_key _rpc_obj_key;  /* key into RPC object pool */
+
+	public:
+
+		Capability_data(Rpc_obj_key rpc_obj_key)
+		: _rpc_obj_key(rpc_obj_key) { }
+
+		Capability_data() { }
+
+		Rpc_obj_key rpc_obj_key() const { return _rpc_obj_key; }
+
+		uint8_t inc_ref() { return ++_ref_cnt; }
+		uint8_t dec_ref() { return --_ref_cnt; }
+};
+
+#endif /* _BASE__INTERNAL__CAPABILITY_DATA_H_ */

repos/base-sel4/src/base/internal/capability_space.h

@@ -0,0 +1,51 @@
+/*
+ * \brief   Platform-agnostic interface for the local capability space
+ * \author  Norman Feske
+ * \date    2015-05-08
+ *
+ * Even though the capability space is implemented in a platform-specific way,
+ * all platforms have the same lifetime management in common, which uses this
+ * interface.
+ */
+
+/*
+ * 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 _BASE__INTERNAL__CAPABILITY_SPACE_H_
+#define _BASE__INTERNAL__CAPABILITY_SPACE_H_
+
+/* Genode includes */
+#include <base/native_types.h>
+#include <base/thread.h>
+
+/* base-internal includes */
+#include <internal/capability_data.h>
+
+namespace Genode { namespace Capability_space {
+
+	/**
+	 * Create capability for RPC entrypoint thread
+	 */
+	Native_capability create_ep_cap(Thread_base &ep_thread);
+
+	/**
+	 * Increment reference counter
+	 */
+	void dec_ref(Native_capability::Data &data);
+
+	/**
+	 * Decrement reference counter
+	 */
+	void inc_ref(Native_capability::Data &data);
+
+	/**
+	 * Obtain RPC object key
+	 */
+	Rpc_obj_key rpc_obj_key(Native_capability::Data const &data);
+} }
+
+#endif /* _BASE__INTERNAL__CAPABILITY_SPACE_H_ */

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

@@ -0,0 +1,209 @@
+/*
+ * \brief  seL4-specific capability-space management
+ * \author Norman Feske
+ * \date   2015-05-08
+ */
+
+/*
+ * 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 _BASE__INTERNAL__CAPABILITY_SPACE_SEL4_H_
+#define _BASE__INTERNAL__CAPABILITY_SPACE_SEL4_H_
+
+/* base includes */
+#include <util/avl_tree.h>
+#include <base/lock.h>
+
+/* base-internal includes */
+#include <internal/capability_space.h>
+#include <internal/assert.h>
+
+namespace Genode { template <unsigned, typename> class Capability_space_sel4; }
+
+
+/**
+ * Platform-specific supplement to the generic 'Capability_space' interface
+ */
+namespace Genode { namespace Capability_space {
+
+	/**
+	 * Information needed to transfer capability via the kernel's IPC mechanism
+	 */
+	struct Ipc_cap_data
+	{
+		Rpc_obj_key rpc_obj_key;
+		unsigned    sel;
+	};
+
+	/**
+	 * Retrieve IPC data for given capability
+	 */
+	Ipc_cap_data ipc_cap_data(Native_capability const &cap);
+
+	/**
+	 * Allocate unused selector for receiving a capability via IPC
+	 */
+	unsigned alloc_rcv_sel();
+
+} }
+
+
+/**
+ * Capability space template
+ *
+ * The capability space of core and non-core components differ in two ways.
+ *
+ * First, core must keep track of all capabilities of the system. Hence, its
+ * capability space must be dimensioned larger.
+ *
+ * Second, core has to maintain the information about the CAP session that
+ * was used to allocate the capability to prevent misbehaving clients from
+ * freeing capabilities allocated from another component. This information
+ * is part of the core-specific 'Native_capability::Data' structure.
+ */
+template <unsigned NUM_CAPS, typename CAP_DATA>
+class Genode::Capability_space_sel4
+{
+	public:
+
+		/*
+		 * The capability space consists of two parts. The lower part is
+		 * populated with statically-defined capabilities whereas the upper
+		 * part is dynamically managed by the component. The 'NUM_STATIC_CAPS'
+		 * defines the size of the first part.
+		 */
+		enum { NUM_STATIC_CAPS = 1024 };
+
+	private:
+
+		typedef CAP_DATA Data;
+
+		/**
+		 * Supplement Native_capability::Data with the meta data needed to
+		 * manage it in an AVL tree
+		 */
+		struct Tree_managed_data : Data, Avl_node<Tree_managed_data>
+		{
+			template <typename... ARGS>
+			Tree_managed_data(ARGS... args) : Data(args...) { }
+
+			Tree_managed_data() { }
+
+			bool higher(Tree_managed_data *data)
+			{
+				return data->rpc_obj_key().value() > rpc_obj_key().value();
+			}
+
+			Tree_managed_data *find_by_key(Rpc_obj_key key)
+			{
+				if (key.value() == rpc_obj_key().value()) return this;
+
+				Tree_managed_data *data =
+					this->child(key.value() > rpc_obj_key().value());
+
+				return data ? data->find_by_key(key) : nullptr;
+			}
+		};
+
+		Tree_managed_data           _caps_data[NUM_CAPS];
+		Avl_tree<Tree_managed_data> _tree;
+		Lock                        _lock;
+
+		/**
+		 * Calculate index into _caps_data for capability data object
+		 */
+		unsigned _index(Data const &data) const
+		{
+			addr_t const offset = (addr_t)&data - (addr_t)_caps_data;
+			return offset / sizeof(_caps_data[0]);
+		}
+
+		/**
+		 * Return true if capability is locally managed by the component
+		 */
+		bool _is_dynamic(Data &data) const
+		{
+			return _index(data) >= NUM_STATIC_CAPS;
+		}
+
+		void _remove(Native_capability::Data &data)
+		{
+			if (_caps_data[_index(data)].rpc_obj_key().valid())
+				_tree.remove(static_cast<Tree_managed_data *>(&data));
+
+			_caps_data[_index(data)] = Tree_managed_data();
+		}
+
+	public:
+
+		/*****************************************************
+		 ** Support for the Core_capability_space interface **
+		 *****************************************************/
+
+		/**
+		 * Create Genode capability for kernel cap selector 'sel'
+		 *
+		 * The arguments following the selector are passed to the constructor
+		 * of the 'Native_capability::Data' type.
+		 */
+		template <typename... ARGS>
+		Native_capability::Data &create_capability(unsigned sel, ARGS... args)
+		{
+			Lock::Guard guard(_lock);
+
+			ASSERT(!_caps_data[sel].rpc_obj_key().valid());
+			ASSERT(sel < NUM_CAPS);
+
+			_caps_data[sel] = Tree_managed_data(args...);
+
+			if (_caps_data[sel].rpc_obj_key().valid())
+				_tree.insert(&_caps_data[sel]);
+
+			return _caps_data[sel];
+		}
+
+		/**
+		 * Return kernel cap selector
+		 */
+		unsigned sel(Data const &data) const { return _index(data); }
+
+
+		/************************************************
+		 ** Support for the Capability_space interface **
+		 ************************************************/
+
+		void dec_ref(Data &data)
+		{
+			Lock::Guard guard(_lock);
+
+			if (_is_dynamic(data) && !data.dec_ref()) {
+				PDBG("remove cap");
+				_remove(data);
+			}
+		}
+
+		void inc_ref(Data &data)
+		{
+			Lock::Guard guard(_lock);
+
+			if (_is_dynamic(data))
+				data.inc_ref();
+		}
+
+		Rpc_obj_key rpc_obj_key(Data const &data) const
+		{
+			return data.rpc_obj_key();
+		}
+
+		Capability_space::Ipc_cap_data ipc_cap_data(Data const &data) const
+		{
+			return { rpc_obj_key(data), sel(data) };
+		}
+};
+
+
+#endif /* _BASE__INTERNAL__CAPABILITY_SPACE_SEL4_H_ */

repos/base-sel4/src/base/internal/native_types.h

@@ -0,0 +1,20 @@
+/*
+ * \brief  Platform-specific type and parameter definitions
+ * \author Norman Feske
+ * \date   2015-05-06
+ */
+
+/*
+ * 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 _BASE__INTERNAL__NATIVE_TYPES_H_
+#define _BASE__INTERNAL__NATIVE_TYPES_H_
+
+/* Genode includes */
+#include <base/native_types.h>
+
+#endif /* _BASE__INTERNAL__NATIVE_TYPES_H_ */

repos/base-sel4/src/base/internal/rpc_obj_key.h

@@ -0,0 +1,43 @@
+/*
+ * \brief  Key into RPC object pool
+ * \author Norman Feske
+ * \date   2015-05-08
+ */
+
+/*
+ * 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 _BASE__INTERNAL__RPC_OBJ_KEY_H_
+#define _BASE__INTERNAL__RPC_OBJ_KEY_H_
+
+/* base includes */
+#include <base/stdint.h>
+
+namespace Genode { struct Rpc_obj_key; }
+
+
+class Genode::Rpc_obj_key
+{
+	public:
+
+		enum { INVALID = ~0UL };
+
+	private:
+
+		uint32_t _value = INVALID;
+
+	public:
+
+		Rpc_obj_key() { }
+
+		explicit Rpc_obj_key(uint32_t value) : _value(value) { }
+
+		bool     valid() const { return _value != INVALID; }
+		uint32_t value() const { return _value; }
+};
+
+#endif /* _BASE__INTERNAL__RPC_OBJ_KEY_H_ */

repos/base-sel4/src/base/ipc/ipc.cc

@@ -15,8 +15,12 @@
 #include <base/ipc.h>
 #include <base/printf.h>
 #include <base/blocking.h>
+#include <base/thread.h>
 #include <util/misc_math.h>
 
+/* base-internal includes */
+#include <internal/capability_space.h>
+
 /* seL4 includes */
 #include <sel4/interfaces/sel4_client.h>
 
@@ -127,7 +131,23 @@ void Ipc_server::_prepare_next_reply_wait()
 void Ipc_server::_wait()
 {
 	/* wait for new server request */
-	try { Ipc_istream::_wait(); } catch (Blocking_canceled) { }
+	PDBG("called, do seL4_Wait");
+
+	seL4_MessageInfo_t const msg_info =
+		seL4_Wait(Thread_base::myself()->tid().ep_sel, nullptr);
+	PDBG("returned from seL4_Wait, call seL4_Reply");
+
+	PDBG("msg_info: got unwrapped  %d", seL4_MessageInfo_get_capsUnwrapped(msg_info));
+	PDBG("          got extra caps %d", seL4_MessageInfo_get_extraCaps(msg_info));
+	PDBG("          label          %d", seL4_MessageInfo_get_label(msg_info));
+
+	if (seL4_MessageInfo_get_capsUnwrapped(msg_info)) {
+		PDBG("          badge          %d", seL4_CapData_Badge_get_Badge(seL4_GetBadge(0)));
+	}
+
+	for (;;)
+		seL4_Yield();
+//	try { Ipc_istream::_wait(); } catch (Blocking_canceled) { }
 
 	_prepare_next_reply_wait();
 }
@@ -155,4 +175,6 @@ Ipc_server::Ipc_server(Msgbuf_base *snd_msg,
 :
 	Ipc_istream(rcv_msg), Ipc_ostream(Native_capability(), snd_msg),
 	_reply_needed(false)
-{ }
+{
+	*static_cast<Native_capability *>(this) = Native_capability(Capability_space::create_ep_cap(*Thread_base::myself()));
+}

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

@@ -56,14 +56,6 @@ Pager_capability Pager_entrypoint::manage(Pager_object *obj)
 	/* return invalid capability if no activation is present */
 	if (!_activation) return Pager_capability();
 
-	_activation->cap();
-
-	Untyped_capability cap = Native_capability(_activation->cap().dst(), obj->badge());
-
-	/* add server object to object pool */
-	obj->cap(cap);
-	insert(obj);
-
-	/* return capability that uses the object id as badge */
-	return reinterpret_cap_cast<Pager_object>(cap);
+	PDBG("not implemented");
+	return Pager_capability();
 }

repos/base-sel4/src/base/server/server.cc

@@ -0,0 +1,97 @@
+/*
+ * \brief  Default version of platform-specific part of server framework
+ * \author Norman Feske
+ * \author Stefan Kalkowski
+ * \date   2006-05-12
+ *
+ * This version is suitable for platforms similar to L4. Each platform
+ * for which this implementation is not suited contains a platform-
+ * specific version in its respective 'base-<platform>' repository.
+ */
+
+/*
+ * Copyright (C) 2006-2013 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.
+ */
+
+/* Genode includes */
+#include <base/rpc_server.h>
+
+using namespace Genode;
+
+
+/***********************
+ ** Server entrypoint **
+ ***********************/
+
+Untyped_capability Rpc_entrypoint::_manage(Rpc_object_base *obj)
+{
+	Untyped_capability new_obj_cap = _cap_session->alloc(_cap);
+
+	/* add server object to object pool */
+	obj->cap(new_obj_cap);
+	insert(obj);
+
+	/* return capability that uses the object id as badge */
+	return new_obj_cap;
+}
+
+
+void Rpc_entrypoint::entry()
+{
+	Ipc_server srv(&_snd_buf, &_rcv_buf);
+	_ipc_server = &srv;
+	_cap = srv;
+	_cap_valid.unlock();
+
+	/*
+	 * Now, the capability of the server activation is initialized
+	 * an can be passed around. However, the processing of capability
+	 * invocations should not happen until activation-using server
+	 * is completely initialized. Thus, we wait until the activation
+	 * gets explicitly unblocked by calling 'Rpc_entrypoint::activate()'.
+	 */
+	_delay_start.lock();
+
+	while (!_exit_handler.exit) {
+
+		int opcode = 0;
+
+		srv >> IPC_REPLY_WAIT >> opcode;
+
+		/* set default return value */
+		srv.ret(Ipc_client::ERR_INVALID_OBJECT);
+
+		/* check whether capability's label fits global id */
+		PDBG("not implemented");
+
+		/* atomically lookup and lock referenced object */
+		Object_pool<Rpc_object_base>::Guard curr_obj(lookup_and_lock(srv.badge()));
+		if (!curr_obj)
+			continue;
+
+		{
+			Lock::Guard lock_guard(_curr_obj_lock);
+			_curr_obj = curr_obj;
+		}
+
+		/* dispatch request */
+		try { srv.ret(_curr_obj->dispatch(opcode, srv, srv)); }
+		catch (Blocking_canceled) { }
+
+		{
+			Lock::Guard lock_guard(_curr_obj_lock);
+			_curr_obj = 0;
+		}
+	}
+
+	/* answer exit call, thereby wake up '~Rpc_entrypoint' */
+	srv << IPC_REPLY;
+
+	/* defer the destruction of 'Ipc_server' until '~Rpc_entrypoint' is ready */
+	_delay_exit.lock();
+
+
+}

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

@@ -0,0 +1,65 @@
+/*
+ * \brief  seL4-specific capability allocation
+ * \author Norman Feske
+ * \author Stefan Kalkowski
+ * \date   2015-05-08
+ *
+ * Based on base-foc/src/core/cap_session_component.cc
+ */
+
+/*
+ * 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.
+ */
+
+/* Genode includes */
+#include <base/capability.h>
+#include <util/misc_math.h>
+
+/* core includes */
+#include <cap_session_component.h>
+#include <platform.h>
+
+/* base-internal include */
+#include <core_capability_space.h>
+
+using namespace Genode;
+
+
+static unsigned unique_id_cnt;
+
+
+Native_capability Cap_session_component::alloc(Cap_session_component *session,
+                                               Native_capability ep)
+{
+	if (!ep.valid()) {
+		PWRN("Invalid entrypoint capability");
+		return Native_capability();
+	}
+
+	Rpc_obj_key const rpc_obj_key(++unique_id_cnt);
+
+	return Capability_space::create_rpc_obj_cap(ep, session, rpc_obj_key);
+}
+
+
+Native_capability Cap_session_component::alloc(Native_capability ep)
+{
+	return Cap_session_component::alloc(this, ep);
+}
+
+
+void Cap_session_component::free(Native_capability cap)
+{
+	if (!cap.valid())
+		return;
+
+	PDBG("not implemented");
+
+	/*
+	 * XXX check whether this CAP session has created the capability to delete.
+	 */
+}
+

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

@@ -0,0 +1,169 @@
+/*
+ * \brief  Instance of the core-local (Genode) capability space
+ * \author Norman Feske
+ * \date   2015-05-08
+ */
+
+/*
+ * 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.
+ */
+
+/* base includes */
+#include <base/native_types.h>
+#include <base/printf.h>
+
+/* base-internal includes */
+#include <internal/capability_data.h>
+#include <internal/capability_space_sel4.h>
+
+/* core includes */
+#include <core_capability_space.h>
+#include <platform.h>
+
+namespace Genode { class Cap_session; }
+
+
+/**
+ * Core-specific supplement of the capability meta data
+ */
+class Genode::Native_capability::Data : public Capability_data
+{
+	private:
+
+		Cap_session const *_cap_session = nullptr;
+
+	public:
+
+		Data(Cap_session const *cap_session, Rpc_obj_key key)
+		:
+			Capability_data(key), _cap_session(cap_session)
+		{ }
+
+		Data() { }
+
+		bool belongs_to(Cap_session const *session) const
+		{
+			return _cap_session == session;
+		}
+};
+
+
+using namespace Genode;
+
+
+/**
+ * Singleton instance of core-specific capability space
+ */
+namespace {
+
+	struct Local_capability_space
+	:
+		Capability_space_sel4<1UL << Core_cspace::NUM_CORE_SEL_LOG2,
+		                      Native_capability::Data>
+	{ };
+
+	static Local_capability_space &local_capability_space()
+	{
+		static Local_capability_space capability_space;
+		return capability_space;
+	}
+}
+
+
+/********************************************************************
+ ** Implementation of the core-specific Capability_space interface **
+ ********************************************************************/
+
+Native_capability
+Capability_space::create_rpc_obj_cap(Native_capability ep_cap,
+                                     Cap_session const *cap_session,
+                                     Rpc_obj_key rpc_obj_key)
+{
+	/* allocate core-local selector for RPC object */
+	unsigned const rpc_obj_sel = platform_specific()->alloc_core_sel();
+
+	/* create Genode capability */
+	Native_capability::Data &data =
+		local_capability_space().create_capability(rpc_obj_sel, cap_session,
+		                                           rpc_obj_key);
+
+	ASSERT(ep_cap.valid());
+
+	unsigned const ep_sel = local_capability_space().sel(*ep_cap.data());
+
+	/* mint endpoint capability into RPC object capability */
+	{
+		seL4_CNode     const service    = seL4_CapInitThreadCNode;
+		seL4_Word      const dest_index = rpc_obj_sel;
+		uint8_t        const dest_depth = 32;
+		seL4_CNode     const src_root   = seL4_CapInitThreadCNode;
+		seL4_Word      const src_index  = ep_sel;
+		uint8_t        const src_depth  = 32;
+		seL4_CapRights const rights     = seL4_AllRights;
+		seL4_CapData_t const badge      = seL4_CapData_Badge_new(rpc_obj_key.value());
+
+		int const ret = seL4_CNode_Mint(service,
+		                                dest_index,
+		                                dest_depth,
+		                                src_root,
+		                                src_index,
+		                                src_depth,
+		                                rights,
+		                                badge);
+		ASSERT(ret == 0);
+	}
+
+	return Native_capability(data);
+}
+
+
+/******************************************************
+ ** Implementation of the Capability_space interface **
+ ******************************************************/
+
+Native_capability Capability_space::create_ep_cap(Thread_base &ep_thread)
+{
+	unsigned const ep_sel = ep_thread.tid().ep_sel;
+
+	/* entrypoint capabilities are not allocated from a CAP session */
+	Cap_session const *cap_session = nullptr;
+
+	Native_capability::Data &data =
+		local_capability_space().create_capability(ep_sel, cap_session,
+		                                           Rpc_obj_key());
+
+	return Native_capability(data);
+}
+
+
+void Capability_space::dec_ref(Native_capability::Data &data)
+{
+	local_capability_space().dec_ref(data);
+}
+
+
+void Capability_space::inc_ref(Native_capability::Data &data)
+{
+	local_capability_space().inc_ref(data);
+}
+
+
+Rpc_obj_key Capability_space::rpc_obj_key(Native_capability::Data const &data)
+{
+	return local_capability_space().rpc_obj_key(data);
+}
+
+
+Capability_space::Ipc_cap_data Capability_space::ipc_cap_data(Native_capability const &cap)
+{
+	return local_capability_space().ipc_cap_data(*cap.data());
+}
+
+
+unsigned Capability_space::alloc_rcv_sel()
+{
+	return platform_specific()->alloc_core_rcv_sel();
+}

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

@@ -0,0 +1,35 @@
+/*
+ * \brief  Capability session service
+ * \author Norman Feske
+ * \date   2015-05-08
+ */
+
+/*
+ * 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__CAP_SESSION_COMPONENT_H_
+#define _CORE__INCLUDE__CAP_SESSION_COMPONENT_H_
+
+/* Genode includes */
+#include <base/rpc_server.h>
+#include <base/allocator.h>
+
+namespace Genode { class Cap_session_component; }
+
+struct Genode::Cap_session_component : Rpc_object<Cap_session>
+{
+	Cap_session_component(Allocator *md_alloc, const char *args) {}
+
+	Native_capability alloc(Native_capability ep);
+
+	void free(Native_capability cap);
+
+	static Native_capability alloc(Cap_session_component *session,
+	                               Native_capability ep);
+};
+
+#endif /* _CORE__INCLUDE__CAP_SESSION_COMPONENT_H_ */

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

@@ -0,0 +1,46 @@
+/*
+ * \brief  Definition of core-specific capability meta data
+ * \author Norman Feske
+ * \date   2015-05-08
+ */
+
+/*
+ * 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__CAPABILITY_CORE_DATA_H_
+#define _CORE__INCLUDE__CAPABILITY_CORE_DATA_H_
+
+/* base-internal includes */
+#include <internal/capability_data.h>
+
+namespace Genode {
+
+	class Cap_session;
+	class Core_capability_data;
+}
+
+
+class Genode::Core_capability_data : public Capability_data
+{
+	private:
+
+		Cap_session const *_cap_session;
+
+	public:
+
+		Capability_core_data(Cap_session const *cap_session, Rpc_obj_key key)
+		:
+			Capability_common_data(key), _cap_session(cap_session)
+		{ }
+
+		bool belongs_to(Cap_session const *session) const
+		{
+			return _cap_session == session;
+		}
+};
+
+#endif /* _CORE__INCLUDE__CAPABILITY_CORE_DATA_H_ */

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

@@ -0,0 +1,33 @@
+/*
+ * \brief  Core-specific interface to the local capability space
+ * \author Norman Feske
+ * \date   2015-05-08
+ */
+
+/*
+ * 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__CORE_CAPABILITY_SPACE_H_
+#define _CORE__INCLUDE__CORE_CAPABILITY_SPACE_H_
+
+/* base-internal includes */
+#include <internal/rpc_obj_key.h>
+
+namespace Genode { class Cap_session; }
+
+
+namespace Genode { namespace Capability_space {
+
+	/**
+	 * Create new RPC object capability for the specified entrypoint
+	 */
+	Native_capability create_rpc_obj_cap(Native_capability ep_cap,
+	                                     Cap_session const *,
+	                                     Rpc_obj_key);
+} }
+
+#endif /* _CORE__INCLUDE__CORE_CAPABILITY_SPACE_H_ */

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

@@ -137,6 +137,8 @@ class Genode::Platform : public Platform_generic
 		Vm_space &core_vm_space() { return _core_vm_space; }
 
 		unsigned alloc_core_sel();
+		unsigned alloc_core_rcv_sel();
+		void free_core_sel(unsigned sel);
 
 		void wait_for_exit();
 };

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

@@ -268,6 +268,24 @@ unsigned Platform::alloc_core_sel()
 }
 
 
+unsigned Platform::alloc_core_rcv_sel()
+{
+	unsigned rcv_sel = alloc_core_sel();
+
+	seL4_SetCapReceivePath(_core_cnode.sel(), rcv_sel, 0);
+
+	return rcv_sel;
+}
+
+
+void Platform::free_core_sel(unsigned sel)
+{
+	Lock::Guard guard(_core_sel_alloc_lock);
+
+	_core_sel_alloc.free(sel);
+}
+
+
 void Platform::wait_for_exit()
 {
 	sleep_forever();

repos/base-sel4/src/core/target.inc

@@ -28,12 +28,15 @@ SRC_CC      += \
                core_rm_session.cc \
                core_mem_alloc.cc \
                dump_alloc.cc \
-               context_area.cc
+               context_area.cc \
+               capability_space.cc
+
 
 LIBS        += core_printf base-common syscall
 
 INC_DIR     += $(REP_DIR)/src/core/include \
                $(GEN_CORE_DIR)/include \
+               $(REP_DIR)/src/base \
                $(BASE_DIR)/src/base/thread
 
 include $(GEN_CORE_DIR)/version.inc
@@ -41,7 +44,6 @@ include $(GEN_CORE_DIR)/version.inc
 vpath main.cc                     $(GEN_CORE_DIR)
 vpath ram_session_component.cc    $(GEN_CORE_DIR)
 vpath rom_session_component.cc    $(GEN_CORE_DIR)
-vpath cap_session_component.cc    $(GEN_CORE_DIR)
 vpath cpu_session_component.cc    $(GEN_CORE_DIR)
 vpath pd_session_component.cc     $(GEN_CORE_DIR)
 vpath rm_session_component.cc     $(GEN_CORE_DIR)

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

@@ -53,33 +53,37 @@ void Thread_base::_init_platform_thread(size_t, Type type)
 	Untyped_address const ipc_buffer =
 		create_and_map_ipc_buffer(phys_alloc, utcb_virt_addr);
 
-	/* allocate TCB selector within core's CNode */
-	unsigned const tcb_idx = platform.alloc_core_sel();
-
+	/* allocate TCB within core's CNode */
+	_tid.tcb_sel = platform.alloc_core_sel();
 	Kernel_object::create<Kernel_object::Tcb>(phys_alloc,
-	                                          platform.core_cnode().sel(), tcb_idx);
+	                                          platform.core_cnode().sel(),
+	                                          _tid.tcb_sel);
 
-	unsigned const tcb_sel = tcb_idx;
-	_tid.tcb_sel = tcb_sel;
+	/* allocate synchronous endpoint within core's CNode */
+	_tid.ep_sel = platform.alloc_core_sel();
+	Kernel_object::create<Kernel_object::Endpoint>(phys_alloc,
+	                                               platform.core_cnode().sel(),
+	                                               _tid.ep_sel);
 
 	/* assign IPC buffer to thread */
 	{
 		/* determine page frame selector of the allocated IPC buffer */
 		unsigned ipc_buffer_sel = Untyped_memory::frame_sel(ipc_buffer.phys());
 
-		int const ret = seL4_TCB_SetIPCBuffer(tcb_sel, utcb_virt_addr, ipc_buffer_sel);
+		int const ret = seL4_TCB_SetIPCBuffer(_tid.tcb_sel, utcb_virt_addr,
+		                                      ipc_buffer_sel);
 		if (ret != 0)
 			PDBG("seL4_TCB_SetIPCBuffer returned %d", ret);
 	}
 
 	/* set scheduling priority */
 	enum { PRIORITY_MAX = 0xff };
-	seL4_TCB_SetPriority(tcb_sel, PRIORITY_MAX);
+	seL4_TCB_SetPriority(_tid.tcb_sel, PRIORITY_MAX);
 
 	/* associate thread with core PD */
 	{
 		seL4_CapData_t no_cap_data = { { 0 } };
-		int const ret = seL4_TCB_SetSpace(tcb_sel, 0,
+		int const ret = seL4_TCB_SetSpace(_tid.tcb_sel, 0,
 		                  platform.top_cnode().sel(), no_cap_data,
 		                  seL4_CapInitThreadPD, no_cap_data);
 

repos/base-sel4/src/test/sel4/target.mk

@@ -23,7 +23,9 @@ SRC_CC += signal/signal.cc signal/common.cc
 SRC_CC += server/server.cc
 SRC_CC += thread/trace.cc
 SRC_CC += thread/context_allocator.cc
+SRC_CC += env/capability.cc env/capability_space.cc
 
+INC_DIR +=  $(REP_DIR)/src/base
 INC_DIR +=  $(REP_DIR)/src/base/lock
 INC_DIR += $(BASE_DIR)/src/base/lock
 INC_DIR += $(BASE_DIR)/src/base/thread