From 6ffba0e47362f627e88ebe1148844306bb9065a6 Mon Sep 17 00:00:00 2001 From: Norman Feske Date: Mon, 11 May 2015 08:43:43 +0200 Subject: [PATCH] sel4: IPC implementation --- repos/base-sel4/include/base/ipc_msgbuf.h | 220 ++++++++------ .../src/base/env/capability_space.cc | 35 +++ .../src/base/internal/capability_space_sel4.h | 51 +++- repos/base-sel4/src/base/ipc/ipc.cc | 283 +++++++++++++++--- repos/base-sel4/src/base/server/server.cc | 3 - repos/base-sel4/src/core/capability_space.cc | 29 +- repos/base-sel4/src/core/include/platform.h | 1 + repos/base-sel4/src/core/platform.cc | 8 +- 8 files changed, 484 insertions(+), 146 deletions(-) diff --git a/repos/base-sel4/include/base/ipc_msgbuf.h b/repos/base-sel4/include/base/ipc_msgbuf.h index 380b6d5e25..d38db66b6d 100644 --- a/repos/base-sel4/include/base/ipc_msgbuf.h +++ b/repos/base-sel4/include/base/ipc_msgbuf.h @@ -1,11 +1,11 @@ /* - * \brief seL4-specific layout of IPC message buffer + * \brief IPC message buffer layout * \author Norman Feske - * \date 2014-10-14 + * \date 2015-05-10 */ /* - * Copyright (C) 2014 Genode Labs GmbH + * 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. @@ -14,99 +14,133 @@ #ifndef _INCLUDE__BASE__IPC_MSGBUF_H_ #define _INCLUDE__BASE__IPC_MSGBUF_H_ +#include + namespace Genode { - /** - * IPC message buffer layout - */ - class Msgbuf_base - { - public: - - enum { MAX_CAPS_PER_MSG = 8 }; - - protected: - - /* - * Capabilities to be transferred - */ - int _caps[MAX_CAPS_PER_MSG]; - Genode::size_t _used_caps; - Genode::size_t _read_cap_index; - - /** - * Maximum size of plain-data message payload - */ - Genode::size_t _size; - - /** - * Actual size of plain-data message payload - */ - Genode::size_t _used_size; - - char _msg_start[]; /* symbol marks start of message buffer data */ - - /* - * No member variables are allowed beyond this point! - */ - - public: - - char buf[]; - - Msgbuf_base() { reset_caps(); } - - /** - * Return size of message buffer - */ - inline Genode::size_t size() const { return _size; }; - - /** - * Return address of message buffer - */ - inline void *addr() { return &_msg_start[0]; }; - - void reset_caps() { _used_caps = 0; _read_cap_index = 0; } - - bool append_cap(int cap) - { - if (_used_caps == MAX_CAPS_PER_MSG) - return false; - - _caps[_used_caps++] = cap; - return true; - } - - int read_cap() - { - if (_read_cap_index == _used_caps) - return -1; - - return _caps[_read_cap_index++]; - } - - size_t used_caps() const { return _used_caps; } - - int cap(unsigned index) const - { - return index < _used_caps ? _caps[index] : -1; - } - }; - - - /** - * Pump up IPC message buffer to specified buffer size - */ - template - class Msgbuf : public Msgbuf_base - { - public: - - char buf[BUF_SIZE]; - - Msgbuf() { _size = BUF_SIZE; } - }; + class Msgbuf_base; + template struct Msgbuf; } +class Genode::Msgbuf_base +{ + public: + + enum { MAX_CAPS_PER_MSG = 3 }; + + protected: + + /* + * Resolve ambiguity if the header is included from a libc-using + * program. + */ + typedef Genode::size_t size_t; + + /* + * Capabilities to be transferred + */ + Native_capability _caps[MAX_CAPS_PER_MSG]; + size_t _used_caps = 0; + size_t _read_cap_index = 0; + + /** + * Maximum size of plain-data message payload + */ + size_t const _size; + + /** + * Actual size of plain-data message payload + */ + size_t _used_size = 0; + + char _msg_start[]; /* symbol marks start of message buffer data */ + + /* + * No member variables are allowed beyond this point! + */ + + Msgbuf_base(size_t size) : _size(size) { } + + public: + + char buf[]; + + /** + * Return size of message buffer + */ + size_t size() const { return _size; }; + + void reset_caps() + { + for (Genode::size_t i = 0; i < _used_caps; i++) + _caps[i] = Native_capability(); + + _used_caps = 0; + } + + void reset_read_cap_index() + { + _read_cap_index = 0; + } + + /** + * Return pointer to start of message-buffer content + */ + void const *data() const { return &_msg_start[0]; }; + void *data() { return &_msg_start[0]; }; + + /** + * Exception type + */ + class Too_many_caps : public Exception { }; + + /** + * Called from '_marshal_capability' + */ + void append_cap(Native_capability const &cap) + { + if (_used_caps == MAX_CAPS_PER_MSG) + throw Too_many_caps(); + + _caps[_used_caps++] = cap; + } + + /** + * Called from '_unmarshal_capability' + */ + Native_capability extract_cap() + { + if (_read_cap_index == _used_caps) + return Native_capability(); + + return _caps[_read_cap_index++]; + } + + /** + * Return number of marshalled capabilities + */ + size_t used_caps() const { return _used_caps; } + + Native_capability &cap(unsigned index) + { + return _caps[index]; + } +}; + + +template +struct Genode::Msgbuf : Msgbuf_base +{ + /** + * Pump up IPC message buffer to specified buffer size + * + * XXX remove padding of 16 + */ + char buf[BUF_SIZE + 16]; + + Msgbuf() : Msgbuf_base(BUF_SIZE) { } +}; + + #endif /* _INCLUDE__BASE__IPC_MSGBUF_H_ */ diff --git a/repos/base-sel4/src/base/env/capability_space.cc b/repos/base-sel4/src/base/env/capability_space.cc index bb43309f59..d1019937d6 100644 --- a/repos/base-sel4/src/base/env/capability_space.cc +++ b/repos/base-sel4/src/base/env/capability_space.cc @@ -82,3 +82,38 @@ 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()); +} + + +Native_capability Capability_space::lookup(Rpc_obj_key rpc_obj_key) +{ + Native_capability::Data *data = local_capability_space().lookup(rpc_obj_key); + + return data ? Native_capability(*data) : Native_capability(); +} + + +unsigned Capability_space::alloc_rcv_sel() +{ + PDBG("not implemented"); + for (;;); + return 0; +} + + +void Capability_space::reset_sel(unsigned sel) +{ + PDBG("not implemented"); +} + + +Native_capability Capability_space::import(Ipc_cap_data ipc_cap_data) +{ + PDBG("not implemented"); + + return Native_capability(); +} diff --git a/repos/base-sel4/src/base/internal/capability_space_sel4.h b/repos/base-sel4/src/base/internal/capability_space_sel4.h index 1785204611..af0701360d 100644 --- a/repos/base-sel4/src/base/internal/capability_space_sel4.h +++ b/repos/base-sel4/src/base/internal/capability_space_sel4.h @@ -22,7 +22,7 @@ #include #include -namespace Genode { template class Capability_space_sel4; } +namespace Genode { template class Capability_space_sel4; } /** @@ -37,6 +37,9 @@ namespace Genode { namespace Capability_space { { Rpc_obj_key rpc_obj_key; unsigned sel; + + Ipc_cap_data(Rpc_obj_key rpc_obj_key, unsigned sel) + : rpc_obj_key(rpc_obj_key), sel(sel) { } }; /** @@ -49,6 +52,23 @@ namespace Genode { namespace Capability_space { */ unsigned alloc_rcv_sel(); + /** + * Delete selector but retain allocation + * + * This function is used when a delegated capability selector is replaced + * with an already known selector. The delegated selector is discarded. + */ + void reset_sel(unsigned sel); + + /** + * Lookup capability by its RPC object key + */ + Native_capability lookup(Rpc_obj_key key); + + /** + * Import capability into the component's capability space + */ + Native_capability import(Ipc_cap_data ipc_cap_data); } } @@ -65,7 +85,7 @@ namespace Genode { namespace Capability_space { * freeing capabilities allocated from another component. This information * is part of the core-specific 'Native_capability::Data' structure. */ -template +template class Genode::Capability_space_sel4 { public: @@ -73,10 +93,10 @@ class Genode::Capability_space_sel4 /* * 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. + * part is dynamically managed by the component. The + * 'NUM_CORE_MANAGED_CAPS' defines the size of the first part. */ - enum { NUM_STATIC_CAPS = 1024 }; + enum { NUM_CORE_MANAGED_CAPS = _NUM_CORE_MANAGED_CAPS }; private: @@ -111,7 +131,7 @@ class Genode::Capability_space_sel4 Tree_managed_data _caps_data[NUM_CAPS]; Avl_tree _tree; - Lock _lock; + Lock mutable _lock; /** * Calculate index into _caps_data for capability data object @@ -125,9 +145,9 @@ class Genode::Capability_space_sel4 /** * Return true if capability is locally managed by the component */ - bool _is_dynamic(Data &data) const + bool _is_core_managed(Data &data) const { - return _index(data) >= NUM_STATIC_CAPS; + return _index(data) < NUM_CORE_MANAGED_CAPS; } void _remove(Native_capability::Data &data) @@ -180,7 +200,7 @@ class Genode::Capability_space_sel4 { Lock::Guard guard(_lock); - if (_is_dynamic(data) && !data.dec_ref()) { + if (!_is_core_managed(data) && !data.dec_ref()) { PDBG("remove cap"); _remove(data); } @@ -190,8 +210,9 @@ class Genode::Capability_space_sel4 { Lock::Guard guard(_lock); - if (_is_dynamic(data)) + if (!_is_core_managed(data)) { data.inc_ref(); + } } Rpc_obj_key rpc_obj_key(Data const &data) const @@ -203,6 +224,16 @@ class Genode::Capability_space_sel4 { return { rpc_obj_key(data), sel(data) }; } + + Data *lookup(Rpc_obj_key key) const + { + Lock::Guard guard(_lock); + + if (!_tree.first()) + return nullptr; + + return _tree.first()->find_by_key(key); + } }; diff --git a/repos/base-sel4/src/base/ipc/ipc.cc b/repos/base-sel4/src/base/ipc/ipc.cc index 0204b15f94..3390c3bd3a 100644 --- a/repos/base-sel4/src/base/ipc/ipc.cc +++ b/repos/base-sel4/src/base/ipc/ipc.cc @@ -19,7 +19,8 @@ #include /* base-internal includes */ -#include +#include +#include /* seL4 includes */ #include @@ -27,19 +28,216 @@ using namespace Genode; +/** + * Message-register definitions + */ +enum { + MR_IDX_NUM_CAPS = 0, + MR_IDX_CAPS = 1, + MR_IDX_DATA = MR_IDX_CAPS + Msgbuf_base::MAX_CAPS_PER_MSG, +}; + + +/** + * Convert Genode::Msgbuf_base content into seL4 message + * + * \param msg source message buffer + * \param data_length size of message data in bytes + */ +static seL4_MessageInfo_t new_seL4_message(Msgbuf_base &msg, + size_t const data_length) +{ + /* + * Supply capabilities to kernel IPC message + */ + seL4_SetMR(MR_IDX_NUM_CAPS, msg.used_caps()); + size_t sel4_sel_cnt = 0; + for (size_t i = 0; i < msg.used_caps(); i++) { + + Native_capability &cap = msg.cap(i); + + if (cap.valid()) { + Capability_space::Ipc_cap_data const ipc_cap_data = + Capability_space::ipc_cap_data(cap); + + seL4_SetMR(MR_IDX_CAPS + i, ipc_cap_data.rpc_obj_key.value()); + seL4_SetCap(sel4_sel_cnt++, ipc_cap_data.sel); + } else { + seL4_SetMR(MR_IDX_CAPS + i, Rpc_obj_key::INVALID); + } + } + + /* + * Pad unused capability slots with invalid capabilities to avoid + * leakage of any information that happens to be in the IPC buffer. + */ + for (size_t i = msg.used_caps(); i < Msgbuf_base::MAX_CAPS_PER_MSG; i++) + seL4_SetMR(MR_IDX_CAPS + i, Rpc_obj_key::INVALID); + + /* + * Allocate and define receive selector + */ + Native_thread &thread = Thread_base::myself()->tid(); + + if (!thread.rcv_sel) + thread.rcv_sel = Capability_space::alloc_rcv_sel(); + + /* + * Supply data payload + */ + size_t const num_data_mwords = + align_natural(data_length) / sizeof(umword_t); + + umword_t const *src = (umword_t const *)msg.data(); + for (size_t i = 0; i < num_data_mwords; i++) + seL4_SetMR(MR_IDX_DATA + i, *src++); + + seL4_MessageInfo_t const msg_info = + seL4_MessageInfo_new(0, 0, sel4_sel_cnt, + MR_IDX_DATA + num_data_mwords); + return msg_info; +} + + +/** + * Convert seL4 message into Genode::Msgbuf_base + */ +static void decode_seL4_message(umword_t badge, + seL4_MessageInfo_t const &msg_info, + Msgbuf_base &dst_msg) +{ + /* + * Extract Genode capabilities from seL4 IPC message + */ + dst_msg.reset_caps(); + size_t const num_caps = seL4_GetMR(MR_IDX_NUM_CAPS); + size_t curr_sel4_cap_idx = 0; + + for (size_t i = 0; i < num_caps; i++) { + + Rpc_obj_key const rpc_obj_key(seL4_GetMR(MR_IDX_CAPS + i)); + + if (!rpc_obj_key.valid()) { + dst_msg.append_cap(Native_capability()); + continue; + } + + /* + * RPC object key as contained in the message data is valid. + */ + + unsigned const unwrapped = + seL4_MessageInfo_get_capsUnwrapped(msg_info) & + (1 << curr_sel4_cap_idx); + + /* distinguish unwrapped from delegated cap */ + if (unwrapped) { + + /* + * Received unwrapped capability + * + * This means that the capability argument belongs to our endpoint. + * So it is already present within the capability space. + */ + + unsigned const arg_badge = + seL4_CapData_Badge_get_Badge(seL4_GetBadge(curr_sel4_cap_idx)); + + if (arg_badge != rpc_obj_key.value()) { + PWRN("argument badge (%d) != RPC object key (%d)", + arg_badge, rpc_obj_key.value()); + } + + Native_capability arg_cap = Capability_space::lookup(rpc_obj_key); + + dst_msg.append_cap(arg_cap); + + } else { + + /* + * Received delegated capability + * + * We have either received a capability that is foreign to us, + * or an alias for a capability that we already posses. The + * latter can happen in the following circumstances: + * + * - We forwarded a selector that was created by another + * component. We cannot re-identify such a capability when + * handed back because seL4's badge mechanism works only for + * capabilities belonging to the IPC destination endpoint. + * + * - We received a selector on the IPC reply path, where seL4's + * badge mechanism is not in effect. + */ + + bool const delegated = seL4_MessageInfo_get_extraCaps(msg_info); + + ASSERT(delegated); + + Native_thread &thread = Thread_base::myself()->tid(); + + Native_capability arg_cap = Capability_space::lookup(rpc_obj_key); + + if (arg_cap.valid()) { + + /* + * Discard the received selector and keep using the already + * present one. + * + * XXX We'd need to find out if both the received and the + * looked-up selector refer to the same endpoint. + * Unfortunaltely, seL4 lacks such a comparison operation. + */ + + Capability_space::reset_sel(thread.rcv_sel); + + dst_msg.append_cap(arg_cap); + + } else { + + Capability_space::Ipc_cap_data const + ipc_cap_data(rpc_obj_key, thread.rcv_sel); + + dst_msg.append_cap(Capability_space::import(ipc_cap_data)); + + /* + * Since we keep using the received selector, we need to + * allocate a fresh one for the next incoming delegation. + */ + thread.rcv_sel = Capability_space::alloc_rcv_sel(); + } + } + curr_sel4_cap_idx++; + } + + /* + * Extract message data payload + */ + + umword_t *dst = (umword_t *)dst_msg.data(); + for (size_t i = 0; i < seL4_MessageInfo_get_length(msg_info); i++) + *dst++ = seL4_GetMR(MR_IDX_DATA + i); + + /* + * Store RPC object key of invoked object to be picked up by server.cc + */ + *(long *)dst_msg.data() = badge; +} + + /***************************** ** IPC marshalling support ** *****************************/ void Ipc_ostream::_marshal_capability(Native_capability const &cap) { - PDBG("not implemented"); + _snd_msg->append_cap(cap); } void Ipc_istream::_unmarshal_capability(Native_capability &cap) { - PDBG("not implemented"); + cap = _rcv_msg->extract_cap(); } @@ -49,16 +247,15 @@ void Ipc_istream::_unmarshal_capability(Native_capability &cap) void Ipc_ostream::_send() { - PDBG("not implemented"); + ASSERT(false); _write_offset = sizeof(umword_t); } - Ipc_ostream::Ipc_ostream(Native_capability dst, Msgbuf_base *snd_msg) : - Ipc_marshaller((char *)snd_msg->addr(), snd_msg->size()), + Ipc_marshaller((char *)snd_msg->data(), snd_msg->size()), _snd_msg(snd_msg), _dst(dst) { _write_offset = sizeof(umword_t); @@ -71,19 +268,13 @@ Ipc_ostream::Ipc_ostream(Native_capability dst, Msgbuf_base *snd_msg) void Ipc_istream::_wait() { - PDBG("not implemented"); - - for (;;) - seL4_Yield(); - - - _read_offset = sizeof(umword_t); + ASSERT(false); } Ipc_istream::Ipc_istream(Msgbuf_base *rcv_msg) : - Ipc_unmarshaller((char *)rcv_msg->addr(), rcv_msg->size()), + Ipc_unmarshaller((char *)rcv_msg->data(), rcv_msg->size()), _rcv_msg(rcv_msg) { _read_offset = sizeof(umword_t); @@ -99,7 +290,20 @@ Ipc_istream::~Ipc_istream() { } void Ipc_client::_call() { - PDBG("not implemented"); + if (!Ipc_ostream::_dst.valid()) { + PERR("Trying to invoke an invalid capability, stop."); + kernel_debugger_panic("IPC destination is invalid"); + } + + seL4_MessageInfo_t const request_msg_info = + new_seL4_message(*_snd_msg, _write_offset); + + unsigned const dst_sel = Capability_space::ipc_cap_data(_dst).sel; + + seL4_MessageInfo_t const reply_msg_info = + seL4_Call(dst_sel, request_msg_info); + + decode_seL4_message(0, reply_msg_info, *_rcv_msg); _write_offset = _read_offset = sizeof(umword_t); } @@ -125,29 +329,19 @@ void Ipc_server::_prepare_next_reply_wait() /* receive buffer offset */ _read_offset = sizeof(umword_t); + + _rcv_msg->reset_read_cap_index(); + _snd_msg->reset_caps(); } void Ipc_server::_wait() { - /* wait for new server request */ - PDBG("called, do seL4_Wait"); - + seL4_Word badge = Rpc_obj_key::INVALID; seL4_MessageInfo_t const msg_info = - seL4_Wait(Thread_base::myself()->tid().ep_sel, nullptr); - PDBG("returned from seL4_Wait, call seL4_Reply"); + seL4_Wait(Thread_base::myself()->tid().ep_sel, &badge); - 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) { } + decode_seL4_message(badge, msg_info, *_rcv_msg); _prepare_next_reply_wait(); } @@ -155,18 +349,30 @@ void Ipc_server::_wait() void Ipc_server::_reply() { - try { _send(); } catch (Ipc_error) { } - - _prepare_next_reply_wait(); + ASSERT(false); } void Ipc_server::_reply_wait() { - if (_reply_needed) - _reply(); + if (!_reply_needed) { - _wait(); + _wait(); + + } else { + + seL4_Word badge = Rpc_obj_key::INVALID; + seL4_MessageInfo_t const reply_msg_info = + new_seL4_message(*_snd_msg, _write_offset); + + seL4_MessageInfo_t const request_msg_info = + seL4_ReplyWait(Thread_base::myself()->tid().ep_sel, + reply_msg_info, &badge); + + decode_seL4_message(badge, request_msg_info, *_rcv_msg); + } + + _prepare_next_reply_wait(); } @@ -176,5 +382,6 @@ Ipc_server::Ipc_server(Msgbuf_base *snd_msg, Ipc_istream(rcv_msg), Ipc_ostream(Native_capability(), snd_msg), _reply_needed(false) { - *static_cast(this) = Native_capability(Capability_space::create_ep_cap(*Thread_base::myself())); + *static_cast(this) = + Native_capability(Capability_space::create_ep_cap(*Thread_base::myself())); } diff --git a/repos/base-sel4/src/base/server/server.cc b/repos/base-sel4/src/base/server/server.cc index 4b7e286aa1..0d7d3daf29 100644 --- a/repos/base-sel4/src/base/server/server.cc +++ b/repos/base-sel4/src/base/server/server.cc @@ -64,9 +64,6 @@ void Rpc_entrypoint::entry() /* 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::Guard curr_obj(lookup_and_lock(srv.badge())); if (!curr_obj) diff --git a/repos/base-sel4/src/core/capability_space.cc b/repos/base-sel4/src/core/capability_space.cc index 112c461fc2..14f0ce27b0 100644 --- a/repos/base-sel4/src/core/capability_space.cc +++ b/repos/base-sel4/src/core/capability_space.cc @@ -61,7 +61,7 @@ namespace { struct Local_capability_space : - Capability_space_sel4<1UL << Core_cspace::NUM_CORE_SEL_LOG2, + Capability_space_sel4<1UL << Core_cspace::NUM_CORE_SEL_LOG2, 0UL, Native_capability::Data> { }; @@ -163,7 +163,34 @@ Capability_space::Ipc_cap_data Capability_space::ipc_cap_data(Native_capability } +Native_capability Capability_space::lookup(Rpc_obj_key rpc_obj_key) +{ + Native_capability::Data *data = local_capability_space().lookup(rpc_obj_key); + + return data ? Native_capability(*data) : Native_capability(); +} + + unsigned Capability_space::alloc_rcv_sel() { return platform_specific()->alloc_core_rcv_sel(); } + + +void Capability_space::reset_sel(unsigned sel) +{ + return platform_specific()->reset_sel(sel); +} + + +Native_capability Capability_space::import(Ipc_cap_data ipc_cap_data) +{ + /* imported capabilities are not associated with a CAP session */ + Cap_session const *cap_session = nullptr; + + Native_capability::Data &data = + local_capability_space().create_capability(ipc_cap_data.sel, cap_session, + ipc_cap_data.rpc_obj_key); + + return Native_capability(data); +} diff --git a/repos/base-sel4/src/core/include/platform.h b/repos/base-sel4/src/core/include/platform.h index 01cda78e61..6d9d23cef4 100644 --- a/repos/base-sel4/src/core/include/platform.h +++ b/repos/base-sel4/src/core/include/platform.h @@ -138,6 +138,7 @@ class Genode::Platform : public Platform_generic unsigned alloc_core_sel(); unsigned alloc_core_rcv_sel(); + void reset_sel(unsigned sel); void free_core_sel(unsigned sel); void wait_for_exit(); diff --git a/repos/base-sel4/src/core/platform.cc b/repos/base-sel4/src/core/platform.cc index 463d0f3b83..3eeabfdf03 100644 --- a/repos/base-sel4/src/core/platform.cc +++ b/repos/base-sel4/src/core/platform.cc @@ -272,12 +272,18 @@ unsigned Platform::alloc_core_rcv_sel() { unsigned rcv_sel = alloc_core_sel(); - seL4_SetCapReceivePath(_core_cnode.sel(), rcv_sel, 0); + seL4_SetCapReceivePath(_core_cnode.sel(), rcv_sel, _core_cnode.size_log2()); return rcv_sel; } +void Platform::reset_sel(unsigned sel) +{ + _core_cnode.remove(sel); +} + + void Platform::free_core_sel(unsigned sel) { Lock::Guard guard(_core_sel_alloc_lock);