From 3cc7774fe491e2c413e54e519940b89ae31c23d7 Mon Sep 17 00:00:00 2001 From: Martin Stein Date: Thu, 25 Apr 2019 02:45:03 +0200 Subject: [PATCH] base-hw: Ada/SPARK-friendly Ipc_node interface 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 --- repos/base-hw/src/core/kernel/ipc_node.cc | 12 ++------ repos/base-hw/src/core/kernel/ipc_node.h | 18 +++++------ repos/base-hw/src/core/kernel/thread.cc | 37 ++++++++++++----------- 3 files changed, 29 insertions(+), 38 deletions(-) diff --git a/repos/base-hw/src/core/kernel/ipc_node.cc b/repos/base-hw/src/core/kernel/ipc_node.cc index a55858594..c7648e24f 100644 --- a/repos/base-hw/src/core/kernel/ipc_node.cc +++ b/repos/base-hw/src/core/kernel/ipc_node.cc @@ -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; } diff --git a/repos/base-hw/src/core/kernel/ipc_node.h b/repos/base-hw/src/core/kernel/ipc_node.h index 631b2955e..4750e0712 100644 --- a/repos/base-hw/src/core/kernel/ipc_node.h +++ b/repos/base-hw/src/core/kernel/ipc_node.h @@ -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 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_ */ diff --git a/repos/base-hw/src/core/kernel/thread.cc b/repos/base-hw/src/core/kernel/thread.cc index 3a0b9ccf4..843c00dea 100644 --- a/repos/base-hw/src/core/kernel/thread.cc +++ b/repos/base-hw/src/core/kernel/thread.cc @@ -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); }