ExternalVendorCode/genode
1
0
Fork 0
mirror of https://github.com/genodelabs/genode.git synced 2025-01-29 15:44:02 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

base-hw: Ada/SPARK-friendly Ipc_node interface

Browse Source 
This prevents the use of C++ features in the public method interface of the
synchronous-IPC module that would be impractical for the in-place
translation of the module into Ada in the context of the Spunky project.

* Get rid of thread accessor.
* Get rid of non-const functions with return values.
* Get rid of pointer return-values.

Ref #3308
This commit is contained in:
Martin Stein 2019-04-25 02:45:03 +02:00 committed by Christian Helmuth
parent a04243aaf4
commit 3cc7774fe4
3 changed files with 29 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
repos/base-hw/src/core/kernel/ipc_node.cc
View File

@ -122,8 +122,8 @@ void Ipc_node::send_request(Ipc_node &callee, bool help)
}
Ipc_node * Ipc_node::helping_sink() {
return _helps_outbuf_dst() ? _callee->helping_sink() : this; }
Thread &Ipc_node::helping_sink() {
return _helps_outbuf_dst() ? _callee->helping_sink() : _thread; }
bool Ipc_node::can_await_request()
@ -132,18 +132,12 @@ bool Ipc_node::can_await_request()
}
bool Ipc_node::await_request()
void Ipc_node::await_request()
{
/* if no request announced then wait */
bool announced = false;
_state = AWAIT_REQUEST;
/* if anybody already announced a request receive it */
_request_queue.dequeue([&] (Queue_item &item) {
_receive_request(item.object());
announced = true;
});
return announced;
}

18
repos/base-hw/src/core/kernel/ipc_node.h
View File

@ -124,12 +124,13 @@ class Kernel::Ipc_node
* \param help wether the request implies a helping relationship
*/
bool can_send_request();
void send_request(Ipc_node &callee, bool help);
void send_request(Ipc_node &callee,
bool help);
/**
* Return root destination of the helping-relation tree we are in
*/
Ipc_node * helping_sink();
Thread &helping_sink();
/**
* Call function 'f' of type 'void (Ipc_node *)' for each helper
@ -137,12 +138,12 @@ class Kernel::Ipc_node
template <typename F> void for_each_helper(F f)
{
/* if we have a helper in the receive buffer, call 'f' for it */
if (_caller && _caller->_help) f(*_caller);
if (_caller && _caller->_help) f(_caller->_thread);
/* call 'f' for each helper in our request queue */
_request_queue.for_each([f] (Queue_item &item) {
Ipc_node &node { item.object() };
if (node._help) f(node);
if (node._help) f(node._thread);
});
}
@ -152,7 +153,7 @@ class Kernel::Ipc_node
* \return wether a request could be received already
*/
bool can_await_request();
bool await_request();
void await_request();
/**
* Reply to last request if there's any
@ -164,12 +165,7 @@ class Kernel::Ipc_node
*/
void cancel_waiting();
/***************
** Accessors **
***************/
Thread &thread() { return _thread; }
bool awaits_request() const { return _state == AWAIT_REQUEST; }
};
#endif /* _CORE__KERNEL__IPC_NODE_H_ */

37
repos/base-hw/src/core/kernel/thread.cc
View File

@ -217,15 +217,15 @@ void Thread::ipc_await_request_failed()
void Thread::_deactivate_used_shares()
{
Cpu_job::_deactivate_own_share();
_ipc_node.for_each_helper([&] (Ipc_node &ipc_node) {
ipc_node.thread()._deactivate_used_shares(); });
_ipc_node.for_each_helper([&] (Thread &thread) {
thread._deactivate_used_shares(); });
}
void Thread::_activate_used_shares()
{
Cpu_job::_activate_own_share();
_ipc_node.for_each_helper([&] (Ipc_node &ipc_node) {
ipc_node.thread()._activate_used_shares(); });
_ipc_node.for_each_helper([&] (Thread &thread) {
thread._activate_used_shares(); });
}
void Thread::_become_active()
@ -246,7 +246,7 @@ void Thread::_die() { _become_inactive(DEAD); }
Cpu_job * Thread::helping_sink() {
return &_ipc_node.helping_sink()->thread(); }
return &_ipc_node.helping_sink(); }
size_t Thread::_core_to_kernel_quota(size_t const quota) const
@ -405,22 +405,23 @@ void Thread::_call_delete_thread()
void Thread::_call_await_request_msg()
{
if (!_ipc_node.can_await_request()) {
if (_ipc_node.can_await_request()) {
unsigned const rcv_caps = user_arg_1();
Genode::Allocator &slab = pd().platform_pd().capability_slab();
for (unsigned i = 0; i < rcv_caps; i++)
_obj_id_ref_ptr[i] = slab.alloc(sizeof(Object_identity_reference));
_ipc_rcv_caps = rcv_caps;
_ipc_node.await_request();
if (_ipc_node.awaits_request()) {
_become_inactive(AWAITS_IPC);
} else {
user_arg_0(0);
}
} else {
Genode::raw("IPC await request: bad state");
user_arg_0(0);
return;
}
unsigned const rcv_caps = user_arg_1();
Genode::Allocator &slab = pd().platform_pd().capability_slab();
for (unsigned i = 0; i < rcv_caps; i++)
_obj_id_ref_ptr[i] = slab.alloc(sizeof(Object_identity_reference));
_ipc_rcv_caps = rcv_caps;
if (_ipc_node.await_request()) {
user_arg_0(0);
return;
}
_become_inactive(AWAITS_IPC);
}