I trying to create my own sel4 based system, and
currently i cannot
understand next thing after calling seL4_Untyped_Retype i will be must
somehow put execution data in memory.
It can be implemented by using seL4_TCB_WriteRegisters.
After creating a TCB with seL4_Untyped_Retype, you will need to configure the TCB using
You may notice that you will need caps to a CSpace object, VSpace root object, and a frame
object that will act
as the thread's IPC buffer. You also will also need the address of the thread's
IPC buffer after mapping it into the
You may find the threads tutorial  useful to refer as you try to understand how threads
Additionally, we have some utility functions  that make it easier to create threads.