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.com<mailto: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
************************************

_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel