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

[Alexander Boettcher]

Hello Alexander,

I think we have to clarify a few things.

The direct invocation of kernel syscalls is not encouraged on Genode
applications, since the whole point about Genode is to have a operating
system framework running _portable code_ across more than 7 microkernels
(seL4, Fiasco.OC, NOVA, Genode's hw-kernel and our retirees OKL4,
Pistachio and Fiasco/L4) and even Linux (base-linux). It is a
fundamental concern to be kernel-independent.

That being said, we avoid as far as possible to give Genode applications
kernel specific capabilities at hand. For Genode/seL4 we intentionally
don't give the seL4 thread capabilities to the applications. That means
you can't succeed in invoking seL4_TCB_ReadRegisters or
seL4_TCB_WriteRegisters syscalls directly. So, as pointed out above - it
is a feature, not a bug.

Instead, please consider the usage of Genode interfaces [1] and more
portable approaches [0] that work across kernels.

Best regards,

Alexander Boettcher.


[0] https://lists.genode.org/pipermail/users/2019-September/006931.html
[1] https://lists.genode.org/pipermail/users/2019-September/006930.html

On 27.09.19 12:05, Alexander Tormasov via users wrote:
> 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
> 
> 
> _______________________________________________
> Genode users mailing list
> users at lists.genode.org
> https://lists.genode.org/listinfo/users
> 

-- 
Alexander Boettcher
Genode Labs

https://www.genode-labs.com - https://www.genode.org

Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth