Re: [seL4] Kernel lock

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";; *Date: * Wed, Nov 4, 2015 01:33 AM *To: * "devel"; *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 To: Yuxin Ren Cc: "devel@sel4.systems" Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: 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 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