Hi All,
Now I am working on sel4test project. I know there is a process for sel4test-driver, and it will spawn new process which does the actual testing. But I want to know how the sel4test-driver process is created, especially how its memory and capability is set up. Could anyone show me the code for those stuff and it is great if give me some explanation or comments about it?
Thank you very much
Yuxin
I don't know the answer Yuxiz. But, please share it when yopu get one.
Thanks, Fred
On Mon, Oct 13, 2014 at 12:39 PM, Yuxin Ren ryx@gwmail.gwu.edu wrote:
Hi All,
Now I am working on sel4test project. I know there is a process for sel4test-driver, and it will spawn new process which does the actual testing. But I want to know how the sel4test-driver process is created, especially how its memory and capability is set up. Could anyone show me the code for those stuff and it is great if give me some explanation or comments about it?
Thank you very much
Yuxin
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
"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
Hello Yuxin et al.
The seL4 manual at http://sel4.systems/Docs/seL4-manual.pdf says a little about system initialisation in Chapter 8. It's a short summary, but it should be an easier reference than reading the code.
As Peter has said, the initial task's code is loaded into memory with the kernel, and the initial task's CSpace and VSpace are put into a "default" configuration by the kernel. The allocator libraries which have been released with the kernel assume that default configuration as a starting point.
I hope that helps.
Cheers, Thomas.
On 14/10/14 09:39, Peter Chubb wrote:
"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
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
-
Fred Seigneur -
Peter Chubb -
Thomas Sewell -
Yuxin Ren