Thanks, that was of great help to me. I was just confused about the differences in core functionality.
Hi Sebastian,
The kernel sets up the initial threads TCB and address space, but it
is the responsibility of user space to manage all address spaces and
threads thereafter. In doing so, user space must call the kernel in
order to enforce strict marshaling of sensitive data structures.
The following library routine is an example of how threads are managed
from a user space application:
https://github.com/seL4/libsel4utils/blob/master/src/thread.c
- Alex
On Sun, 2015-03-01 at 04:31 +0000, Sebastian Lau wrote:
> Hi, sorry if this sounds stupid but are address spaces and threads
> directly managed by the kernel as in are they allocated and identified
> by the kernel or is there another that helps the kernel?
>
>
> _______________________________________________
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel
________________________________
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.