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
[email protected]
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
<[email protected]>
_______________________________________________
Genode users mailing list
[email protected]
https://lists.genode.org/listinfo/users
