Devel

devel@sel4.systems

9 participants
1390 discussions

Kernel lock
by ぷ风过无痕?? 05 Nov '15

05 Nov '15

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(a)sel4.systems>; Date: Wed, Nov 4, 2015 01:33 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 18, Issue 4 Send Devel mailing list submissions to devel(a)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(a)sel4.systems You can reach the person managing the list at devel-owner(a)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(a)gmail.com> To: Yuxin Ren <ryx(a)gwmail.gwu.edu> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <CAGSRWbhESa8qAwNzWjVKzo7Unh=GeGWNTVTBACXbkMA=TbsVQg(a)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(a)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(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20151102/34f3782d/attachmen…> ------------------------------ Message: 2 Date: Mon, 2 Nov 2015 17:58:11 -0800 From: Raymond Jennings <shentino(a)gmail.com> To: Tim Newsham <tim.newsham+sel4(a)gmail.com> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <CAGDaZ_qNsZd+VcH8wwvPcjcq_mQR=xefgKMaR45-L4SO9VBrLQ(a)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(a)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(a)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(a)sel4.systems >> https://sel4.systems/lists/listinfo/devel >> > > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20151102/24c77488/attachmen…> ------------------------------ Message: 3 Date: Tue, 3 Nov 2015 03:05:37 +0000 From: Gernot Heiser <gernot(a)nicta.com.au> To: Raymond Jennings <shentino(a)gmail.com> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <E4936E28-39AA-44E9-B202-FB37401E22F9(a)nicta.com.au> Content-Type: text/plain; charset="us-ascii" On 3 Nov 2015, at 12:58 , Raymond Jennings <shentino(a)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/attachmen…> ------------------------------ Message: 4 Date: Mon, 2 Nov 2015 19:46:14 -0800 From: Raymond Jennings <shentino(a)gmail.com> To: Gernot Heiser <gernot(a)nicta.com.au> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <CAGDaZ_q=98W1c91dFMNN+zL4P1p3+iE-ETAMbfOc51ybxvFwrg(a)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(a)nicta.com.au> wrote: > On 3 Nov 2015, at 12:58 , Raymond Jennings <shentino(a)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/attachmen…> ------------------------------ Message: 5 Date: Tue, 3 Nov 2015 03:54:58 +0000 From: Gernot Heiser <gernot(a)nicta.com.au> To: Raymond Jennings <shentino(a)gmail.com> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <418AEC27-5994-4EAB-8AEB-2D12A7D031A7(a)nicta.com.au> Content-Type: text/plain; charset="utf-8" > On 3 Nov 2015, at 14:46 , Raymond Jennings <shentino(a)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(a)gwmail.gwu.edu> To: Gernot Heiser <gernot(a)nicta.com.au> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <CAAKbDrdNod7_M8h+ufyZCkdJ9bDmKeXNpRD-PpKMSCYUnwpLQQ(a)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(a)nicta.com.au> wrote: > >> On 3 Nov 2015, at 14:46 , Raymond Jennings <shentino(a)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(a)sel4.systems > https://sel4.systems/lists/listinfo/devel ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 18, Issue 4 ************************************

4 4

How is network stack implemented in sel4
by Yuxin Ren 04 Nov '15

04 Nov '15

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

5 7

Running CAmkES Sample Application on Sabre Lite Board
by Bryan Ching 02 Nov '15

02 Nov '15

I was following the CAmkES "Getting Started" tutorial on the seL4 website and followed all the instructions. Here is the link: https://sel4.systems/Info/CAmkES/GettingStarted.pml I managed to get the sample application to run in QEMU (Quick Emulator) like the instructions said. I tried loading the sample application onto the Sabre Lite Board through tftp booting using minicom. However, once I try to boot the .elf file, it displays the memory address and nothing else happens. Is there any configuration file that I need to change to make the sample application run on my Sabre Lite Board? Or is there something else that I am missing? Thanks, Bryan

3 6

Fwd: FOSDEM 2016 - Microkernel devroom CfP
by Martin Decky 28 Oct '15

28 Oct '15

Dear all, I am forwarding the Call for Participation of the Microkernel devroom at FOSDEM 2016. The original announcement did not pass the mailing list gatekeeper for some reason. Martin Decky -------- Forwarded Message -------- Subject: FOSDEM 2016 - Microkernel devroom CfP From: Jakub Jermar <jakub(a)jermar.eu> FOSDEM 2016 - Microkernel devroom CALL FOR PARTICIPATION The developers of several free and open-source microkernel-based operating systems will meet at FOSDEM 2016 [1] in Brussels, Belgium and will share a developer room. The devroom is currently looking for content in the form of talks and activities related to the area of microkernel-based operating systems. Possible topics include, but are not limited to: * project introductory and status update talks, demos * architecture, subsystem and components' design * hardware and device drivers * tools, languages and toolchains * development, debugging, testing and release engineering * best practices and learning from mistakes * trends and challenges * community and life with a microkernel project Please use the Pentabarf [2] system to submit your proposals. You do not need to create a new account if you already have one. When in doubt, please use the devroom mailing list [3]. The deadline for your CfP submissions is on 2015-12-13. Make sure to include the following in your proposal: * title of your talk * abstract (one or two paragraphs) * your full name * your short bio * a picture of yourself * duration of your talk The official devroom schedule (along with the accepted talks) will be announced on 2015-12-18 in the devroom's mailing list and the speakers will be notified via e-mail. The schedule will also be published on the FOSDEM web and in the FOSDEM booklet. The devroom will take place on Saturday of January 30, 2016 at ULB Solbosch Campus in Brussels, Belgium [4]. About FOSDEM FOSDEM is a two-day event organised by volunteers to promote the widespread use of free and open source software. Taking place in the beautiful city of Brussels (Belgium), FOSDEM is widely recognised as the best such conference in Europe. FOSDEM covers a wide spectrum of free and open source software projects, and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) with network/internet connectivity and projectors where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present latest directions, lightning talks, news and discussions. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, certification exams and project stands. Every year, FOSDEM hosts more than 5000 developers at the ULB Solbosch campus. Participation and attendance is totally free, though the organisers gratefully accept donations and sponsorship. No registration necessary. About the devroom Since its inception in 2012 the Microkernel devroom has been part of each FOSDEM conference. It has become a sort of an institutionalized tradition since then. To this date over a dozen projects have participated in one way or another, delivering forty talks and other contributions in total. The goal of the Microkernel devroom has been to bring the various projects together and let them share ideas, cross-pollinate and socialize. Each year the devroom is organized by one of the projects based on a system of rotating presidency from the pool of projects that opt in. In 2016 it is HelenOS' turn again. Social events It has become a tradition that the microkernel projects dine together somewhere in downtown Brussels after the devroom closes. The year 2016 will not be any different, so there is going to be a microkernel family dinner on Saturday night. The exact location and time will be specified later. Consult the FOSDEM web and other projects for additional social events such as the famous FOSDEM-organized Friday Beer Event and the FOSDEM-arranged free sightseeing tours for spouses. Important dates 2015-10-23 CfP 2015-12-13 CfP deadline 2015-12-18 Devroom schedule published, speakers notified 2016-01-30 Microkernel devroom takes place 2016-01-30 Microkernel family dinner Links [1] http://fosdem.org/2016 [2] https://penta.fosdem.org/submission/FOSDEM16 [3] https://lists.fosdem.org/listinfo/microkernel-devroom [4] https://fosdem.org/2016/practical/transportation/

1 0

Support for multiple levels of derived capabilities?
by Mark Jones 22 Oct '15

22 Oct '15

I have a question about the way that derived capabilities are handled in seL4. I'm posting here in the hope that somebody might be able to share some insights about this part of the design. As I understand it, early versions of seL4's Mint operation allowed multiple derived levels of capabilities. (I'm thinking, in particular, of the description of Capability Derivation Trees, or CDTs, on Pages 36-38 of Dhammika Elkaduwe's thesis.) This, for example, would make it possible to construct a system with multiple threads, A, B, and C, each holding a capability to the same object where the capability in C is a CDT child of the capability in B, which in turn is a CDT child of the capability in A. In this scenario, B would have authority to revoke the capability in C, including any further CDT children that C had created, but it wouldn't typically have authority over other children of the original capability in A. So far as I can tell, this is not possible in the current version of seL4. Specifically, the reference manual (API version 1.3, Page 11) indicates that "Ordinary original capabilities can have one level of derived capabilities" and that "Further copies of these derived capabilities will create siblings". In the scenario above, this suggests that the capabilities in B and C would be siblings and that there would be no easy way for B to track any additional sibling copies that C might have created. Can someone provide background about why this change was made? I've seen that Dhammika had a working implementation of the original design, and although it was still technically limited to 128 levels, this was not found to be an issue in practice. But perhaps there were security concerns or problems with verification? Or maybe people who worked with the original system found that it wasn't useful in practice, or that it was hard to use effectively? Or maybe I've just misunderstood some aspect of the above? Thanks and best wishes, Mark

4 5

imx6 + libethdrivers + lwip
by Andrea Sorbini 10 Oct '15

10 Oct '15

Hello, I have been experimenting on the SabreLite imx6 board and the network driver provided by libethdrivers. I've been successful in getting it to work "out of the box" and, testing with a simple UDP echo client running on Linux, I've verified that I can send and receive small UDP messages as long as they were not fragmented. I immediately noticed that the fragmentation performed by Linux was different than the one performed by lwip on seL4. Lwip was successfully reassembling a message fragmented in two, but it wasn't fragmenting it when sending it back out. The driver reports an MTU of 1536 and this is likely the reason for lwip not to perform output fragmentation. Hacking the driver slightly, I had it report an MTU of 1500 to lwip, while using the 1536 value internally to allocate buffers. This has allowed me to successfully receive and send UDP messages of up to ~2950 bytes (ie. under 3 frames). When size is increased above that amount, lwip starts behaving "suspiciously" and I can only see the two first two fragments going out, while the third one is never sent (causing the linux host to timeout on the IP reassembly). Debugging the driver, it seems the third fragment is never actually written Has anybody had any experience in getting bigger UDP messages across? Any suggestions on how to enable it if not? Thanks, -Andrea tl;dr: Got UDP working on imx6 with libethdrivers+lwip, can only send up to 2950 bytes, would like to send more, help needed. -- Andrea Sorbini Software Engineer asorbini(a)rti.com +1.408.990.7475 www.rti.com RTI - Your systems. Working as one.

1 0

Camkes MMIO Driver Failed to find device frame
by Jeff Hieb 03 Oct '15

03 Oct '15

I am working on a UART device driver in camkes for AM335x. When I load the image on the board I get this error: Creating object frame_drv_group_bin_42 in slot 596, from untyped 1f6... device frame, paddr = 0x48022000, size = 12 bits capDL-loader :: << Error: Failed to find device frame at paddr = 0x48022000 >> I am reasonably confident the address is correct, (https://github.com/seL4/libplatsupport/blob/master/plat_include/am335x/plat…) Looking at the source It seems capDL-Loader wants to find this device frame in bootinfo https://github.com/seL4/capdl-loader-app/blob/master/src/main.c#L731 Any help on how capDL-loader builds bootinfo would be appreciated. Jeff -- Jeffrey L. Hieb Department of Engineering Fundamentals University of Louisville Louisville Kentucky 40292 (502) 852 0465

4 4

We're hiring!
by Gernot Heiser 29 Sep '15

29 Sep '15

Want to be part of the seL4 team and be *paid* for having fun? We’re hiring: - proof engineers: https://ssrg.nicta.com.au/jobs/proof-engineers2015 - OS engineers: https://ssrg.nicta.com.au/jobs/OS-engineers2015 - researchers/postdocs: https://ssrg.nicta.com.au/jobs/OS-researchers2015 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.

1 0

libsel4cspace and IPC
by Will Korteland 27 Sep '15

27 Sep '15

Hi, I'm trying to implement a "create endpoint" syscall as a continuation of my AOS project last year. I'm using the following code to create and endpoint in the current threads's cspace (using libsel4cspace): https://gist.github.com/anonymous/8294aa47ad351e4d4066 When this code runs, seL4 prints the following during the cspace_ut_retype_addr call: <<seL4 [decodeUntypedInvocation/128 Tffeead00 @b330]: Untyped Retype: Invalid destination address.>> This error comes from inside libsel4cspace, specifically where it calls seL4_Untyped_RetypeAtOffset(). I've read the libsel4cspace documentation and enabled CSPACE_DEBUG, but nothing from the output looks amiss (I'm not an expert though, and I can post the relevant debug output). Have I done anything wrong in the code above? Thanks, - Will

1 0

How to modify timer server in refos
by ぷ风过无痕?? 27 Sep '15

27 Sep '15

I want to transplant the Refos into the ZYNQ board,Now everything is ok,except the timer server. Could you give me some advices about how to modify timer server's file device_timer.c . ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Thu, Sep 24, 2015 10:00 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 16, Issue 12 Send Devel mailing list submissions to devel(a)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(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Reminder: Developers Day registration closes Monday (Gernot Heiser) ---------------------------------------------------------------------- Message: 1 Date: Wed, 23 Sep 2015 05:58:01 +0000 From: Gernot Heiser <gernot(a)nicta.com.au> To: seL4 <devel(a)sel4.systems> Subject: [seL4] Reminder: Developers Day registration closes Monday Message-ID: <FD16E4F0-FD7A-494C-9432-AF1C4903E750(a)nicta.com.au> Content-Type: text/plain; charset="us-ascii" Details at https://sel4.systems/Community/Devdays/ 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. ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 16, Issue 12 *************************************

2 1

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel