Hi sever99,

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 seL4_TCB_Configure. 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 thread's VSpace.

You may find the threads tutorial [1] useful to refer as you try to understand how threads are created.

Additionally, we have some utility functions [2] that make it easier to create threads.

Regards, Damon

[1] https://docs.sel4.systems/Tutorials/threads.html [2] https://github.com/seL4/seL4_libs/blob/master/libsel4utils/include/sel4utils...