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@lists.genode.org https://lists.genode.org/listinfo/users