"Yuxin" == Yuxin Ren ryx@gwmail.gwu.edu writes:
Yuxin> Now I am working on sel4test project. I know there is a Yuxin> process for sel4test-driver, and it will spawn new process Yuxin> which does the actual testing. But I want to know how the Yuxin> sel4test-driver process is created, especially how its memory Yuxin> and capability is set up. Could anyone show me the code for Yuxin> those stuff and it is great if give me some explanation or Yuxin> comments about
The initial task is hand-crafted by the kernel. Take a look in the seL4 kernel source, arch/arm/kernel/boot.c function try_init_kernel().
The elfloader loads the kernel and the first user task into one-to-one mapped memory, and passes the addresses to the kernel.
try_init_kernel(), after doing any platform-specific initialisation, creates the initial capability tree, and a bootinfo frame that describes resources available to the first user process.
It then creates the idle thread, and sets up and creates the first user thread. When it returns, in head.S the context is switched to the TCB pointed to by ksCurThread -- which will be the first user thread created -- and the return-from-exception at the end of _start transfers control to the new thread.
Peter C