Hi, I have a question about kernel lock in seL4. I have read all the code in sel4 kernel,but I just find one file(kernel\include\arch\ia32\kernel\lock.h) related to the lock in the sel4. I also find that the lock here is used to debug.So I think there does not exist a lock in the sel4kernel.But if the lock really does not exist ,that means the sel4 kernel is non-reentrant, does it? does seL4 really not need the lock ?
------------------ Original ------------------ From: "devel-request";devel-request@sel4.systems; Date: Wed, Nov 4, 2015 01:33 AM To: "devel"devel@sel4.systems;
Subject: Devel Digest, Vol 18, Issue 4
Send Devel mailing list submissions to devel@sel4.systems
To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, via email, send a message with subject or body 'help' to devel-request@sel4.systems
You can reach the person managing the list at devel-owner@sel4.systems
When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..."
Today's Topics:
1. Re: How is network stack implemented in sel4 (Tim Newsham) 2. Re: How is network stack implemented in sel4 (Raymond Jennings) 3. Re: How is network stack implemented in sel4 (Gernot Heiser) 4. Re: How is network stack implemented in sel4 (Raymond Jennings) 5. Re: How is network stack implemented in sel4 (Gernot Heiser) 6. Re: How is network stack implemented in sel4 (Yuxin Ren)
----------------------------------------------------------------------
Message: 1 Date: Mon, 2 Nov 2015 15:48:02 -1000 From: Tim Newsham tim.newsham+sel4@gmail.com To: Yuxin Ren ryx@gwmail.gwu.edu Cc: "devel@sel4.systems" devel@sel4.systems Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: CAGSRWbhESa8qAwNzWjVKzo7Unh=GeGWNTVTBACXbkMA=TbsVQg@mail.gmail.com Content-Type: text/plain; charset="utf-8"
seL4 does not provide a network stack or even network device drivers. An OS on top of seL4 would have to provide their own drivers and stack and is free to put them in a single server or in different servers and choose how to communicate between them.
On Mon, Nov 2, 2015 at 2:38 PM, Yuxin Ren ryx@gwmail.gwu.edu wrote:
Hi,
I have a few questions about network stack in sel4.
Is network stack implemented in the kernel or user level? If in user level, are different protocols (IP/TCP) implemented in a single server or different servers? If in different servers, how do they communicate with each other?
Is there any example code to show how to use network? How to send and receive TCP or UDP packets? How can I set up the network environment on bare metal machine? Is there documentation or instruction?
Thanks a lot! Yuxin
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
-------------- next part -------------- An HTML attachment was scrubbed... URL: http://sel4.systems/pipermail/devel/attachments/20151102/34f3782d/attachment-0001.html
------------------------------
Message: 2 Date: Mon, 2 Nov 2015 17:58:11 -0800 From: Raymond Jennings shentino@gmail.com To: Tim Newsham tim.newsham+sel4@gmail.com Cc: "devel@sel4.systems" devel@sel4.systems Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: CAGDaZ_qNsZd+VcH8wwvPcjcq_mQR=xefgKMaR45-L4SO9VBrLQ@mail.gmail.com Content-Type: text/plain; charset="utf-8"
So basically L4 grants IO caps to the network card's io ports to whatever task acts as the network driver, and it's the driver task's job to bang on the card's I/O and hook up with whatever other tasks represent packet/protocol/whatever layers of the ISO 7 layer stack.
On Mon, Nov 2, 2015 at 5:48 PM, Tim Newsham tim.newsham+sel4@gmail.com wrote:
seL4 does not provide a network stack or even network device drivers. An OS on top of seL4 would have to provide their own drivers and stack and is free to put them in a single server or in different servers and choose how to communicate between them.
On Mon, Nov 2, 2015 at 2:38 PM, Yuxin Ren ryx@gwmail.gwu.edu wrote:
Hi,
I have a few questions about network stack in sel4.
Is network stack implemented in the kernel or user level? If in user level, are different protocols (IP/TCP) implemented in a single server or different servers? If in different servers, how do they communicate with each other?
Is there any example code to show how to use network? How to send and receive TCP or UDP packets? How can I set up the network environment on bare metal machine? Is there documentation or instruction?
Thanks a lot! Yuxin
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
-------------- next part -------------- An HTML attachment was scrubbed... URL: http://sel4.systems/pipermail/devel/attachments/20151102/24c77488/attachment-0001.html
------------------------------
Message: 3 Date: Tue, 3 Nov 2015 03:05:37 +0000 From: Gernot Heiser gernot@nicta.com.au To: Raymond Jennings shentino@gmail.com Cc: "devel@sel4.systems" devel@sel4.systems Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: E4936E28-39AA-44E9-B202-FB37401E22F9@nicta.com.au Content-Type: text/plain; charset="us-ascii"
On 3 Nov 2015, at 12:58 , Raymond Jennings <shentino@gmail.commailto:shentino@gmail.com> wrote:
So basically L4 grants IO caps to the network card's io ports to whatever task acts as the network driver, and it's the driver task's job to bang on the card's I/O and hook up with whatever other tasks represent packet/protocol/whatever layers of the ISO 7 layer stack.
More precisely: seL4 hands all rights to all resources to the initial process, whose job is then to initialise the desired system. It would be that process that hands caps to drivers etc.
Gernot
________________________________
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. -------------- next part -------------- An HTML attachment was scrubbed... URL: http://sel4.systems/pipermail/devel/attachments/20151103/a3a78ad4/attachment-0001.html
------------------------------
Message: 4 Date: Mon, 2 Nov 2015 19:46:14 -0800 From: Raymond Jennings shentino@gmail.com To: Gernot Heiser gernot@nicta.com.au Cc: "devel@sel4.systems" devel@sel4.systems Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: CAGDaZ_q=98W1c91dFMNN+zL4P1p3+iE-ETAMbfOc51ybxvFwrg@mail.gmail.com Content-Type: text/plain; charset="utf-8"
So the kernel itself doesn't actually "own" any capabilities, just does the bookkeeping and enforcement?
On Mon, Nov 2, 2015 at 7:05 PM, Gernot Heiser gernot@nicta.com.au wrote:
On 3 Nov 2015, at 12:58 , Raymond Jennings shentino@gmail.com wrote:
So basically L4 grants IO caps to the network card's io ports to whatever task acts as the network driver, and it's the driver task's job to bang on the card's I/O and hook up with whatever other tasks represent packet/protocol/whatever layers of the ISO 7 layer stack.
More precisely: seL4 hands all rights to all resources to the initial process, whose job is then to initialise the desired system. It would be that process that hands caps to drivers etc.
Gernot
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.
-------------- next part -------------- An HTML attachment was scrubbed... URL: http://sel4.systems/pipermail/devel/attachments/20151102/528f68fb/attachment-0001.html
------------------------------
Message: 5 Date: Tue, 3 Nov 2015 03:54:58 +0000 From: Gernot Heiser gernot@nicta.com.au To: Raymond Jennings shentino@gmail.com Cc: "devel@sel4.systems" devel@sel4.systems Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: 418AEC27-5994-4EAB-8AEB-2D12A7D031A7@nicta.com.au Content-Type: text/plain; charset="utf-8"
On 3 Nov 2015, at 14:46 , Raymond Jennings shentino@gmail.com wrote:
So the kernel itself doesn't actually "own" any capabilities, just does the bookkeeping and enforcement?
Caps are like keys: they authenticate access. The kernel doesn?t need them for its own purposes. However, our integrity and confidentiality proofs show that the kernel will not on its own access user memory, unless on behalf of a thread who demonstrates that it is authorised by presenting an appropriate caps.
Gernot
________________________________
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.
------------------------------
Message: 6 Date: Tue, 3 Nov 2015 12:32:44 -0500 From: Yuxin Ren ryx@gwmail.gwu.edu To: Gernot Heiser gernot@nicta.com.au Cc: "devel@sel4.systems" devel@sel4.systems Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: CAAKbDrdNod7_M8h+ufyZCkdJ9bDmKeXNpRD-PpKMSCYUnwpLQQ@mail.gmail.com Content-Type: text/plain; charset=UTF-8
Thank you all.
But are there any projects on top of sel4 microkernel which implement network functionality? I don't think I need to build the whole network stack from bare metal. It is best for me to just refer some existing projects and run simple network application on top of it.
Yuxin
On Mon, Nov 2, 2015 at 10:54 PM, Gernot Heiser gernot@nicta.com.au wrote:
On 3 Nov 2015, at 14:46 , Raymond Jennings shentino@gmail.com wrote:
So the kernel itself doesn't actually "own" any capabilities, just does the bookkeeping and enforcement?
Caps are like keys: they authenticate access. The kernel doesn?t need them for its own purposes. However, our integrity and confidentiality proofs show that the kernel will not on its own access user memory, unless on behalf of a thread who demonstrates that it is authorised by presenting an appropriate caps.
Gernot
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. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
------------------------------
Subject: Digest Footer
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
------------------------------
End of Devel Digest, Vol 18, Issue 4 ************************************
The kernel is indeed not reentrant and always runs with interrupts disabled whilst in the kernel. This lock is an old artifact from an experiment where seL4 was ran as a multikernel across multiple CPU nodes.
In this case, despite the kernel having no actual shared state, it was convenient to use a single serial port for the output for all the nodes. This made the serial port a shared resource, and hence the presence of this lock, which only protected serial output. As the kernels serial output only exists if the kernel is built in debug mode, the lock only needs to be built for that reason.
Adrian
On Wed 04-Nov-2015 1:41 PM, ぷ风过无痕?? wrote:
Hi, I have a question about kernel lock in seL4. I have read all the code in sel4 kernel,but I just find one file(kernel\include\arch\ia32\kernel\lock.h) related to the lock in the sel4. I also find that the lock here is used to debug.So I think there does not exist a lock in the sel4kernel.But if the lock really does not exist ,that means the sel4 kernel is non-reentrant, does it? does seL4 really not need the lock ?
------------------ Original ------------------ *From: * "devel-request";devel-request@sel4.systems; *Date: * Wed, Nov 4, 2015 01:33 AM *To: * "devel"devel@sel4.systems; *Subject: * Devel Digest, Vol 18, Issue 4
Send Devel mailing list submissions to devel@sel4.systems
To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, via email, send a message with subject or body 'help' to devel-request@sel4.systems
You can reach the person managing the list at devel-owner@sel4.systems
When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..."
Today's Topics:
- Re: How is network stack implemented in sel4 (Tim Newsham)
- Re: How is network stack implemented in sel4 (Raymond Jennings)
- Re: How is network stack implemented in sel4 (Gernot Heiser)
- Re: How is network stack implemented in sel4 (Raymond Jennings)
- Re: How is network stack implemented in sel4 (Gernot Heiser)
- Re: How is network stack implemented in sel4 (Yuxin Ren)
Message: 1 Date: Mon, 2 Nov 2015 15:48:02 -1000 From: Tim Newsham tim.newsham+sel4@gmail.com To: Yuxin Ren ryx@gwmail.gwu.edu Cc: "devel@sel4.systems" devel@sel4.systems Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: CAGSRWbhESa8qAwNzWjVKzo7Unh=GeGWNTVTBACXbkMA=TbsVQg@mail.gmail.com Content-Type: text/plain; charset="utf-8"
seL4 does not provide a network stack or even network device drivers. An OS on top of seL4 would have to provide their own drivers and stack and is free to put them in a single server or in different servers and choose how to communicate between them.
On Mon, Nov 2, 2015 at 2:38 PM, Yuxin Ren ryx@gwmail.gwu.edu wrote:
Hi,
I have a few questions about network stack in sel4.
Is network stack implemented in the kernel or user level? If in user level, are different protocols (IP/TCP) implemented in a single server or different servers? If in different servers, how do they communicate with each other?
Is there any example code to show how to use network? How to send and receive TCP or UDP packets? How can I set up the network environment on bare metal machine? Is there documentation or instruction?
Thanks a lot! Yuxin
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
On 4 Nov 2015, at 17:43 , Adrian Danis <Adrian.Danis@nicta.com.aumailto:Adrian.Danis@nicta.com.au> wrote:
The kernel is indeed not reentrant and always runs with interrupts disabled whilst in the kernel. This lock is an old artifact from an experiment where seL4 was ran as a multikernel across multiple CPU nodes.
a proper multicore implementation is on the roadmap and scheduled for release in the near future
Gernot
________________________________
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.
Dear Adrian, Regarding the sel4 multi kernel experience, I have read the paper from Michael von Testing "The clustered multikernel..", is the multi kernel code available somewhere ? Best Regards Mehdi
On Wed, Nov 4, 2015, 10:59 Gernot Heiser gernot@nicta.com.au wrote:
On 4 Nov 2015, at 17:43 , Adrian Danis Adrian.Danis@nicta.com.au wrote:
The kernel is indeed not reentrant and always runs with interrupts disabled whilst in the kernel. This lock is an old artifact from an experiment where seL4 was ran as a multikernel across multiple CPU nodes.
a proper multicore implementation is on the roadmap and scheduled for release in the near future
Gernot
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. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
You can find the seL4 code on github at www.github.com/seL4/seL4, more information about it, as well as how to use it, can be found at http://sel4.systems/
Please note that the current multi-kernel implementation by Michael Von Tessin is only for the x86 architecture, and we do not have any published source code to provide examples on how to use it.
The existing multi-kernel code is more or less considered legacy at this point, and will be removed from the code base at some point in the future. There is a student currently investigating better and more appropriate ways to support a multi-kernel seL4, although it is unclear how long until this leads to an actual implementation.
While we have no examples, here are some links to places in the seL4 kernel code that should give you a place to get started reading and understanding how the implementation works, and then how to use it. https://github.com/seL4/seL4/blob/master/Kconfig#L237 https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/cmdline.c#L162 https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/cmdline.c#L172 https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/bootinfo.h#L51 https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/bootinfo.h#L56
Adrian
On Thu 05-Nov-2015 5:26 AM, Mehdi Amiri wrote:
Dear Adrian, Regarding the sel4 multi kernel experience, I have read the paper from Michael von Testing "The clustered multikernel..", is the multi kernel code available somewhere ? Best Regards Mehdi
On Wed, Nov 4, 2015, 10:59 Gernot Heiser <gernot@nicta.com.au mailto:gernot@nicta.com.au> wrote:
On 4 Nov 2015, at 17:43 , Adrian Danis <Adrian.Danis@nicta.com.au <mailto:Adrian.Danis@nicta.com.au>> wrote:The kernel is indeed not reentrant and always runs with interrupts disabled whilst in the kernel. This lock is an old artifact from an experiment where seL4 was ran as a multikernel across multiple CPU nodes.a proper multicore implementation is on the roadmap and scheduled for release in the near future Gernot ------------------------------------------------------------------------ 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. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
-
Adrian Danis -
Gernot Heiser -
Mehdi Amiri -
ぷ风过无痕??