Thread switching in Genode/seL4 and registers and utcb access problem

Alexander Tormasov a.tormasov at innopolis.ru
Fri Sep 27 12:05:51 CEST 2019


Thank you for suggestion!
Will send them info that they need explicitly state that you can’t read local (own) thread registers in docs

While I I think that this is mostly bug in Genode - it return incorrect OK code (0) during such attempt while probably need to analyze response from seL4 more carefully

(May be this is seL4 library bug - it is still unclear for me why I haven’t the name used from seL4 documentation in the seL4 sources in Genode/contrib, suspect some linker tricks)

Отправлено с iPhone

27 сент. 2019 г., в 10:56, Adam Wiethuechter <wiethuat at critical.com> написал(а):

 Alex,

I would encourage passing what you found along (even the documentation improvement suggestion) to Data61. They are very open to any form of feedback with seL4.

On 9/26/2019 6:53 AM, Alexander Tormasov via users wrote:

Problem 2.
When I start trying to make a fast solution and try to read registers and some info from low level physical seL4 thread using seL4_TCB_ReadRegisters I found  that:
In returned successfully data rip register is always 0 for current thread, tcb selector myself.native_thread().tcb_sel also 0, and rsp  = 0x13!
Probably I can’t read myself?

Seems that I found answer in the seL4 code. They do not allow ReadReginster from myself:

In file object/tcb.c
exception_t
decodeReadRegisters(cap_t cap, word_t length, bool_t call,
                    word_t *buffer)
{
…
   thread = TCB_PTR(cap_thread_cap_get_capTCBPtr(cap));
    if (thread == NODE_STATE(ksCurThread)) {
        userError("TCB ReadRegisters: Attempted to read our own registers.");
        current_syscall_error.type = seL4_IllegalOperation;
        return EXCEPTION_SYSCALL_ERROR;
    }

Seems that this is my fault (while this is not anyhow specified in the docs, only some innuendo about stopped thread read)

So, the  function used from library seL4_TCB_ReadRegisters incorrectly return 0 - everything is ok while it is not.

Also seems that seL4_TCB_WriteRegisters do not work in such conditions as well - it return without errors and not changing rip to new function specified in appropriate field …




_______________________________________________
Genode users mailing list
users at lists.genode.org<mailto:users at lists.genode.org>
https://lists.genode.org/listinfo/users


--
73's,
Adam Wiethuechter, Junior Software Engineer
Critical Technologies Inc. (CTI)
Desk: (315)-793-0248 x157
Cell: (315)-552-4298
<adam.wiethuechter at critical.com><mailto:adam.wiethuechter at critical.com>

_______________________________________________
Genode users mailing list
users at lists.genode.org
https://lists.genode.org/listinfo/users
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.genode.org/pipermail/users/attachments/20190927/7ddaebdc/attachment.html>


More information about the users mailing list