- Devel - lists.sel4.systems

vspace_reserve_range_at
by Robert VanVossen 11 Dec '15

11 Dec '15

Hello, I am trying to map a device 1:1 in my root thread. When I try to reserve a range at the specific location, using the vspace_reserve_range_at() function I get the following error: ERROR:sel4utils_reserve_range_at_no_alloc:585: Range not available at 0xf8f00000, size 0x64000. Is there something that the kernel or the root task needs to do before this to make this range available for reservation? BTW, I am still using seL4 1.0. Thanks, Robbie VanVossen DornerWorks

2 1

vspace_reserve_range_at
by Robert VanVossen 11 Dec '15

11 Dec '15

Hello, I am trying to create a 1:1 physical to virtual mapping in my root thread. My first step in attempting this is to reserve the virtual address I need using the vspace_reserve_range_at() function, but I get the following error: ERROR:sel4utils_reserve_range_at_no_alloc:585: Range not available at 0xf8f00000, size 0x64000 Is there something I need to do in the kernel or in the root thread to actually allow this memory to be reserved? BTW, I am still using seL4 1.0. Thanks, Robbie VanVossen DornerWorks

1 0

verifying concurrency
by Gergely Buday 09 Dec '15

09 Dec '15

Hi there, what should I read if I want to understand the verification of concurrent programs related to the sel4 project? I have found https://ssrg.nicta.com.au/publications/papers/Daum-phd.pdf https://ssrg.nicta.com.au/publications/papers/Daum_DSW_08.pdf http://ssrg.nicta.com.au/projects/concurrency/ Are there others? Cheers - Gergely

3 2

Reminder: Microkernel-devroom CfP deadline is on this Sunday
by Jakub Jermar 07 Dec '15

07 Dec '15

Hi folks, the CfP deadline for the Microkernel devroom at FOSDEM 2016 is due this Sunday. See the original CfP [1] for information on what to do if you would like to give a talk about some microkernel-related topic. At the same time, I would like to encourage you to submit a talk proposal. It would be shame not to let the wider microkernel community know about the latest and greatest developments in your project. Lastly, please forward this reminder to whoever you think may want to give a talk in the devroom and is not among the recipients of this message. Thanks, Jakub [1] http://trac.helenos.org/wiki/Devroom2016

1 0

haskell on sel4
by Tim Newsham 05 Dec '15

05 Dec '15

I just noticed the web page says "we have Haskell sort-of running on seL4 (thanks or friends from Galois for their help), should be released in the near future" This is great news. Are you able to share any details such as when any of this will be public, what the porting strategy was (is this similar to HalVM?), what dependencies haskell compiled code requires, if there are sel4 bindings, etc? Tim

3 4

Initial Thread physical to Virtual Mapping
by Robert VanVossen 04 Dec '15

04 Dec '15

Hello, I am attempting to integrate the Xilinx drivers, provided through their SDK, with seL4 on the Zynq7000. In the root thread, I created a virtual mapping for the SD Card peripheral, and I pass that virtual address into the driver, so that it is reading and writing to it. The controller has a built-in DMA that gets used for data transfer. I created a buffer in the root thread's virtual space to pass to the DMA, but it needs a physical address. I calculated the virtual/physical offset from the physical and virtual addresses for the application that are given by the elfloader, but that didn't seem to be the correct mapping. Is there a good way to get that mapping, either from within the application itself or from the kernel before hand? Thanks, Robbie VanVossen DornerWorks

3 2

Assigning GPIO buffer to a new process
by Karl Apsite 02 Dec '15

02 Dec '15

Ahoy there! I'm working on a Zynq 7000 - ZC702 dev board. I've setup a capability associated with the GPIO buffer, and have successfully ran a small test in the root process that could read a button's state via GPIO. The next step is to send the capability to a second process so that it can read the button's state. I'm having some trouble understanding how I should go about using the IPC calls to achieve this transfer. I'll try to give a summary of my efforts, to clear up where I am, and what I've done so far. To start: I borrowed (heavily) from the 4th tutorial that established two separate processes Main: https://github.com/seL4-projects/sel4-tutorials/blob/master/solutions/hello… App: https://github.com/seL4-projects/sel4-tutorials/blob/master/solutions/hello… I felt inclined to inform the second process about the whereabouts of the new endpoint as opposed to making an assumption as to where it was allocated. I crammed the address into the argc/argv constructs as the process starts, and it seems to be able to continue just fine. 1. Is that an OK thing to do? I understand that I shouldn't be too willing to share vital information freely between both processes, and I'm not sure if abusing argc/argv to inform the second process is appropriate here. I left the main thread in seL4_Wait(). My idea is: other processes are expected to send a message representing a command that main can respond to. Main can check the message, badge(s), and privileges as necessary, and respond with the capability if it so desires. With the capability in hand, and a tag with extracaps set to one, I was NOT able to successfully send the cap. The second process would only receive a tag with extra caps set to zero, so it must be failing somewhere along the way. I loaded the cap into the first slot using seL4_SetCap(0, my_cap) and the cap was functioning previously, so I doubt it's erroring when I send. I expect an error on the receiving end somewhere. I have NOT been able to prepare a path for a capability in the second process, and notify seL4 of the location using seL4_GetCapReceivePath(root_node, new_cap, 32). 2. How should the second process obtain a reference to its root cnode? 3. How should the second process allocate a new cnode? I think the new_process_t structure in the main process has the addresses I'm after (to obtain the root cnode at least, and maybe allow me to a new cnode?), but I don't understand the implications of informing the second process about the information in the new_process_t structure. 4. Is the new process expected to know all of that information? 5. Is there an API to establish this sort of information (along with the IPC endpoint that I had to cram into argc/argv earlier?)

2 1

seL4 2.0.0 Release Notes
by Anna Lyons 01 Dec '15

01 Dec '15

Introducing seL4 2.0.0 ====================== Version 2.0.0 introduces more consistent terminology to manual and code, as well as API and performance improvements, including to seL4's formally verified ARMv6 version. We clarified the notion of signals and notifications vs IPC, and added a new feature to the seL4 API that allows user programs to receive notifications while waiting for IPC messages. You can now also poll notification objects. Both of these changes are aimed at simplifying user-level interaction with interrupts. In addition to the new features, seL4 has become even faster than it was before, esp. in scheduling threads. The new features and performance improvements are available on all supported platforms, and are formally verified to full sel4 standards. We have also switched our release process to semantic versioning, so it's easy to tell which seL4 releases are binary-compatible, source-compatible, or will require updates to user-level code. Terminology Changes =================== IPC vs Notifications -------------------- The old terminology of "synchronous IPC" vs "asynchronous IPC" was confusing and misleading. We changed this to reflect the fact that IPC in seL4 is always synchronous and is simply referred to as "IPC", which is enabled by "endpoint" objects. The receive operation is now more appropriately called "receive". What used to be called incorrectly "asynchronous IPC" is now called Notifications, enabled by "notification" objects. Notifications are not a form of message passing, but arrays of binary semaphores, and the new terminology describes this better. The operations on them are consequently called "signal" and "wait" New Features ============ Notification binding -------------------- A notification can be bound to a thread and is referred to as the thread's bound notification object. This is a 1:1 relationship. Whenever a thread waits for an IPC on an endpoint, it will receive any signals sent to its bound notification object, with the signal flags converted into a single-word message. Threads can also explicitly wait for signals by waiting on the notification object itself. For more details, see the 2.0.0 manual Implementation improvements =========================== * introduces the bitfield scheduler: faster scheduler (Was linear in the number of runnable threads, now log n) * improved benchmarking macros: can now specify multiple benchmarking tracepoints at once added CONFIG_RELEASE_PRINTF in addition to CONFIG_DEBUG and CONFIG_RELEASE, which enables printf in a release build API Changes =========== * seL4_Recv replaces seL4_Wait on endpoints * seL4_Wait is now only used on notification objects * Async endpoint -> notification object * sync endpoint -> endpoint * seL4_Recv on an endpoint may now return signals sent to a thread's bound notification object. API Additions ============= * seL4_NotificationObject replaces deprecated seL4_AsyncEndpointObject * seL4_NotificationBits size in bits of a notification object * seL4_IRQHandler_SetNotification replaces deprecated seL4_IRQHandler_SetEndpoint * seL4_Recv replaces seL4_Wait for endpoints * seL4_Wait used on notifications * seL4_NBRecv non-blocking (polling) receive on an endpoint, which fails if there is no message waiting. Opposite of NBSend (which silently fails if there is no receiver waiting) * seL4_Poll collects any signals from a notification objects, returns zero if there are none * seL4_Signal replaces deprecated seL4_Notify * seL4_TCB_BindNotification bind a notification to a tcb * seL4_TCB_UnbindNotification unbind a notification from a tcb Deprecations ============ * seL4_AsyncEndpointObject * seL4_Notify * seL4_IRQHandler_SetEndpoint Note on Syscall names ==================== Logically there are only two operations on capabilities, send and receive, which can take opcodes specifying sup-operations. For example, the Notification operations Signal and Wait are mapped to Send and Receive, respectively. For efficiency reasons, many kernel objects use separate kernel entry points for their operations. You must not rely on either, as this can change at any time. Instead, always use the object-specific wrapper functions. User-level repositories ======================= To simply repository management we have merged many of our user level library repositories. To see the changes please compare 1.0.4.xml and 2.0.x.xml in https://github.com/seL4/seL4test-manifest Upgrade notes ============= Calls to seL4_Wait no longer return a seL4_MessageInfo_t as seL4_Wait is intended to be used on notification objects. Calls to the prior version of seL4_Wait need to be replaced with seL4_Recv. If you don't want to upgrade yet - don't worry. Both the sel4test-manifest and verification manifest repositories have manifests titled 1.0.4.xml which point to the tips of the previously released repositories before today. All library repositories have a branch called '1.0.x-compatible' which are compatible with the 1.0.4 kernel. Note that to use the new merged repositories, you must upgrade to 2.0.0. Full changelog ============== Use git log 1.0.4..2.0.0 in https://github.com/seL4/seL4 More details ============ See the 2.0.0 manual included in the release for detailed descriptions of the new features. Or ask on this mailing list! Enjoy! ________________________________ 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.

3 3

Does seL4 support periodic thread
by ぷ风过无痕?? 27 Nov '15

27 Nov '15

Hi everyone,I have some questions about seL4's timer. I know seL4 is controlling the timer device. In the current release version, scheduling is tick-based, there's a periodic interrupt that feeds into the scheduler. I wanna know if seL4 support periodic thread. I want to implement a periodic process in Refos which is above seL4 kernel.And, if seL4 does not support periodic thread, could I modify the kernel scheduler? Does it influences formal verification? I find that Refos modifies _thread_state_t enumeration-type variables (kernel\include\object\structures.h ). Does it influences formal verification? Thank you so much!!

3 2

CAmkES-vm Configuration
by Bryan Ching 24 Nov '15

24 Nov '15

Hi, I was trying to configure the CAmkES-vm to run the vmware configuration. However, I get the following error. [apps/vm] building... /home/bryan/camkes-vm/tools/camkes/camkes.mk:125: /home/bryan/camkes-vm/build/x86/pc99/vm/camkes-gen.mk: No such file or directory [GEN] camkes-gen.mk While transforming AST: /home/bryan/camkes-vm/apps/vm/vm.camkes:4: unresolved reference to VM make[1]: *** [/home/bryan/camkes-vm/build/x86/pc99/vm/camkes-gen.mk] Error 255 make[1]: *** Deleting file `/home/bryan/camkes-vm/build/x86/pc99/vm/ camkes-gen.mk' make: *** [vm] Error 2 I have seen this error before. This time, I used the "make menuconfig" command. I go to Applications --> VMM Main Application --> Configuration. I type in "vmware" to try and configure it. When I am back on the command line, I type "make vmware_defconfig" and then "make silentoldconfig" and finally "make". Where is the camkes-gen.mk file supposed to be located? Thanks, Bryan

2 4

Destroying the Root Thread
by Robert VanVossen 20 Nov '15

20 Nov '15

Hello, I was wondering if I can safely destroy my application root thread after I have setup the capabilities and memory mappings for all of my other threads in the system? Thanks, Robbie VanVossen DornerWorks

5 8

CAmkES-vm Build Question
by Bryan Ching 16 Nov '15

16 Nov '15

Hi, I was just wondering for the CAmkES-vm, where is the Makefile to build it? Also, to clone the github repository, do I use "repo" or can I use "git clone"? Thanks, Bryan

4 7

timing
by Raymond Jennings 12 Nov '15

12 Nov '15

Where does the seL4 microkernel actually get the timing information it needs to enforce scheduling decisions? I can imagine some sort of interrupt or I/O access is required to get it from the raw hardware. How does it get from the timing hardware to the scheduling code?

4 4

CAmkES Tutorial
by Bryan Ching 12 Nov '15

12 Nov '15

Hi, I am following the tutorial for CAmkES and had a few questions. There is a part in the tutorial that says to "create a dependency entry in apps/helloworld/Kbuild for your application". How exactly do you go about creating a dependency? Do you just add it to the first line of the Kconfig file? Also, for the Makefile, I needed to include the camkes.mk file. However, it was not found in the specified directory. This is the command that I included in the Makefile: include ${SOURCE_DIR}/../../tools/common/camkes.mk Where could I get that file? Or if someone had the contents of that file, I could create it myself. Thanks, Bryan

2 6

Call for Participation: NICTA Software Systems Summer School
by Gernot Heiser 11 Nov '15

11 Nov '15

tl;dr 8–9 Feb, free event, travel subsidies for AU/NZ students CALL FOR PARTICIPATION ===================================== Fourth NICTA Software Systems Summer School http://ssrg.nicta.com.au/Events/summer/16 ===================================== Supported by: ANU and UNSW Over two days, this summer school will feature lectures by international leaders in computer systems from industry and academia, interspersed with short student talks and poster sessions. We will emphasise a friendly and informal setting where students can learn and obtain feedback from experts. Topics include operating systems, hypervisors, virtual machines, databases, compilers, language implementation, memory management and security. Research students may apply for participation by submitting a summary (of no more than half a page) on their research interests, indicating how it overlaps with the topic of the summer school. They may also indicate that they would like to give a short talk, although the organisers will only select a small number of student presentations. All attending students will be able to present a poster, and are strongly encouraged to use this opportunity to get feedback from world leaders!. We will also consider submissions from final-stage undergraduate students, post-docs or academic staff, provided they explain the benefits they expect from attendance.Supervisors of attending students are particularly welcome to attend. All submitted material must fit on a single A4 page. COST Attendance is free, but subject to invitation based on the submitted abstract. We will rarely reject an application from a student. Registration includes free lunches and coffee breaks during the summer school, as well as a dinner on the evening of the first day. A limited amount of travel support will be available for students from outside NSW and the ACT. Students requesting travel support must submit a brief justification with their application. Travel support will only be available for students from Australia and New Zealand, and will not exceed the cheapest airfare from their nearest major airport to Sydney. Funds for this are limited, and we will give priority to students likely to benefit most from the summer school, i.e. students whose research is most aligned with the topic. LOCATION The workshop and associated activities will be held in the Computer Science & Engineering building on the UNSW Kensington (main) campus in Sydney. KEY DATES Abstracts Due: Monday, 23 November, 2015, via the SSSS'16 submission site Notification: Friday, 20 November, 2015 Early applications will be notified earlier to help you with planning. ACCOMMODATION For participants from outside Sydney we are holding a limited number of inexpensive rooms at a college on campus. These must be booked (and deposit paid) by the end of November. Latecomers will have to find their own accommodations (there are other colleges and backpacker hostels nearby). ORGANISERS: Gernot Heiser (NICTA and UNSW) <gernot(a)nicta.com.au> Steve Blackburn (ANU and NICTA) <Steve.Blackburn(a)anu.edu.au> PRESENTERS (tentative): • Dr Andrew Baumann, Microsoft Research, Redmond • Prof Steve Blackburn, ANU • Prof Douglas Carmean, Oregon State University • Prof Luis Ceze, University of Washington, Seattle • Prof Kevin Elphinstone, NICTA and UNSW • Prof Alan Fekete, NICTA and Sydney University • Dr Tim Harris, Oracle Labs, Cambridge • Prof Gernot Heiser FACM, NICTA and UNSW, Sydney, Australia • Prof Tony Hosking, NICTA and ANU • Prof Gabriele Keller, NICTA and UNSW • Prof Eliot Moss FACM, UMass Amherst • Dr Karin Strauss, Microsoft Research, Redmond _______________________________________________ Csprofs mailing list Csprofs(a)core.edu.au http://core.edu.au/mailman/listinfo/csprofs_core.edu.au <a href="http://core.edu.au/mailman/listinfo/csprofs_core.edu.au"> Click here to unsubscribe </a> ________________________________ 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

sel4 for armv5 architecture
by vibi sreenivasan 09 Nov '15

09 Nov '15

Hi, Can any one please let me know whether sel4 is supported on armv5 ? I am specifically looking to run sel4 on arm926ej. Thanks & Best Regards Vibi

4 4

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 27 Oct '15

27 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 09 Oct '15

09 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

Reminder: Developers Day registration closes Monday
by Gernot Heiser 23 Sep '15

23 Sep '15

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.

1 0

Caught cap fault in send phase at address 0x0
by Andrew Shruhan 22 Sep '15

22 Sep '15

Hello, I am attempting to create a simple program opening up a serial port on the Sabrelight. Attached is the source code and below is the console output. On other sel4 blogs with this problem uboot may have been the issue. I have used the u-boot as discribed on the supported hardware->sabrelight page with the same outcome. Any help would be appreciated. Thanks, U-Boot 2009.08-dirty (Sep 17 2015 - 14:58:04) CPU: Freescale i.MX6 family TO1.2 at 792 MHz Temperature: 36 C, calibration data 0x56a4bc7d mx6q pll1: 792MHz mx6q pll2: 528MHz mx6q pll3: 480MHz mx6q pll8: 50MHz ipg clock : 66000000Hz ipg per clock : 66000000Hz uart clock : 80000000Hz cspi clock : 60000000Hz ahb clock : 132000000Hz axi clock : 264000000Hz emi_slow clock: 132000000Hz ddr clock : 528000000Hz usdhc1 clock : 198000000Hz usdhc2 clock : 198000000Hz usdhc3 clock : 198000000Hz usdhc4 clock : 198000000Hz nfc clock : 24000000Hz Board: MX6Q-SABRELITE:[ POR] Boot Device: I2C I2C: ready DRAM: 1 GB MMC: FSL_USDHC: 0,FSL_USDHC: 1 JEDEC ID: 0xbf:0x25:0x41 Reading SPI NOR flash 0xc0000 [0x2000 bytes] -> ram 0x276009b8 SUCCESS *** Warning - bad CRC, using default environment In: serial Out: serial Err: serial Net: got MAC address from IIM: 00:19:b8:01:fd:6d FEC0 [PRIME] Hit any key to stop autoboot: 0 mmc1 is current device -- Trying fat on SD 1, partition 1 reading sel4-image 344564 bytes read ## Starting application at 0x20000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10 paddr=[20000000..2004c01f] ELF-loading image 'kernel' paddr=[10000000..10031fff] vaddr=[e0000000..e0031fff] virt_entry=e0000000 ELF-loading image 'hello-1' paddr=[10032000..1003ffff] vaddr=[8000..15fff] virt_entry=803c Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on data at address 0x0 with status 0x7 in thread 0xffdfd900 "rootserver" at address 0x804 -- -Andrew Andrew P. Shruhan Research and Development Engineer III DocBox, Inc. 320 Nevada St Newton MA, 02460 Work: 857-598-2819 ext. 117 www.docboxmed.com <http://www.docboxinc.com/>

2 1

Question about upstream
by Harish Pillay 9v1hp 20 Sep '15

20 Sep '15

Hi. I came across seL4 yesterday and have not spent too much time on it. I have not found anything specific to my question in the FAQ yet, so I am posing it here: has the work done by seL4 been accepted upstream? If not, any reason why it has not been accepted yet? Thanks. Harish

2 2

Roadmap and Developers Day announcements
by Gernot Heiser 16 Sep '15

16 Sep '15

Dear developers, Those of you who aren’t (yet) subscribed to announce(a)sel4.systems might have missed this: we announced - the seL4 roadmap: https://sel4.systems/pipermail/announce/2015/000007.html - the second Developers Day: https://sel4.systems/pipermail/announce/2015/000008.html 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.

2 1

Mysterious Label Before sysenter
by Corey Richardson 16 Sep '15

16 Sep '15

For example, here: https://github.com/seL4/seL4/blob/master/libsel4/arch_include/x86/sel4/arch… What use is the label? Does it align the instruction or do other ABI-important things? -- /cmr

2 2

x86-64
by Raymond Jennings 13 Sep '15

13 Sep '15

Does seL4 support x86-64 with 64-bit virtual address spaces?

2 2

Adding a Rust kernel interface generator
by Corey Richardson 11 Sep '15

11 Sep '15

Hello, As part of the robigalia [0] project I must create a Rust interface to the kernel. I'm using the XML from kernel/libsel4 and have been creating a "new" generator by copying the existing Python scripts. Should I send a patch upstream once this is suitably complete, or should I maintain this completely externally? [0] - https://github.com/robigalia -- /cmr

2 2

how to detect the number of CPUs in the system
by 杰尔米 01 Sep '15

01 Sep '15

Hi all, i want to get the number of CPUs in the system and how many cores in one CPU. how to do that? Thanks! Jeremy Li

3 2

The pt/pd/as abstraction vs software TLBs
by Raymond Jennings 01 Sep '15

01 Sep '15

Hey, quick question. This is just hypothetical, but would making management of pagetables/pagedirectories a low level literal operation hurt seL4's portability to other architectures that might not even use page tables? I could be mistaken but I think there's some archs out there that only have software TLBs (openrisc IIRC among them) Please forgive me if I'm mistaken but my recent question about memory abstraction reminded me about this.

3 2

sharing memory between processes
by Raymond Jennings 01 Sep '15

01 Sep '15

Is there an easy way for one task to share address space with another task directly or does it have to go through the kernel/os and be emulated? I noticed that support for mapping memory is mostly low level assignment of physical frames to virtual frames via page tables, unlike Mach which uses memory objects.

6 7

virtual memory abstraction
by Raymond Jennings 31 Aug '15

31 Aug '15

I noticed that unlike mach, L4 does not directly manage virtual memory, but instead farms out address space, page directory, and page table capabilities to userspace and lets userspace decide what pages to map and where. Does this imply that virtual memory abstraction is userspace responsibility?

2 1

Port I/O - Permissions Question
by Josef M. 25 Aug '15

25 Aug '15

Hi, I'm experimenting with some x86 code that involves reading from I/O ports. I noticed--much to my surprise--that I don't have to use seL4_IA32_IOPort_In8() to read from a port; my program works just as fine using the "in" assembly statement directly, without any caps. The TSS segment limit is initialized with 0x67 https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/vspace.c#L158 and the "I/O Map base address" is initialized with 0 (zero) https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/vspace.c#L43 I believe the result is that ring 3 programs can access I/O port addresses below 0x388 (0x67 * 8) without triggering a protection violation. So my question is: Shouldn't capabilities be required for all ports? Or what what is the reason or motivation behind this? Thanks, Josef

2 1

Running Linux atop sel4
by Sebastian Lau 24 Aug '15

24 Aug '15

On the sel4.systems website, it says that the site is served by the Apache web server on Linux atop sel4. How does that work and could you operate the Linux middleware just on top of sel4, maybe something like mer?

1 0

Roadmap?
by Raymond Jennings 22 Aug '15

22 Aug '15

I remember awhile ago that someone was going to post the roadmap in response to my accessed/dirty bit suggestion...but I haven't seen it yet.

2 1

Some questions about seL4 operating system
by Qing Wei 22 Aug '15

22 Aug '15

Hi, I am a beginner to seL4 as well as microkernel, and very interested in it. I think it is great in terms of its minimality and formally verified security. However, I have some questions about it, (1) How is its performance compared to other monolithic kernel, say, Linux. Could it make use of multicore, multiprocessor to enjoy the performance scalability? (2) How is its ecosystem, fox example, how to support new hardware, does it need write the driver from scratch or could it make use of Linux driver? And how to write application on it, or, could it run Linux application without modification? (3) How is its virtualization support, could it run Linux vm, and does it need any modification to the guest os? Cheers, Qing Wei

3 4

Some comments.
by Mehdi Amiri 17 Aug '15

17 Aug '15

Hi, Thank you for all your efforts and time. I believe the user community is the main success key for all open source projects. Many users and researchers, do not have enough time to read, download and evaluate all the source code in order to investigate a system to see if it is suitable for their research or usage. Usually they will go for clean systems which are easy to use, simple to understand, well documented and have a strong community beside the commercial support to ask and get help in case they had a problem. Here are some comments which may help to increase the number of users and developers for seL4: A) I suggest to add some howtos to the website. It's better to be a wiki like system so other individuals, researchers and students can help in writing some titles. Some interesting topics (at least for me as a beginner in micro-kernel) could be: 1- Running Linux/Android on top of seL4. 2- Writing a simple user application with a use case (not just the SOC). 3. Examples on real-time application. 4- Writing a service (could be a device driver, file-system, etc) for seL4. 5- Documents on using possible run-times like Genode. 6- Documents or case studies on porting an opensource software from Linux or POSIX based system to directly run om seL4. B) Providing ready to use download binary images for supported platforms can also accelerate growth of community. C) A research areas page which can suggest researchers some ideas to chose a title and do their research to expand seL4 could also be useful. Ideas like rump-kernels, lib-OS, visualization (x86/ARM), etc seems to be possible research titles on seL4. I have seen the https://sel4.systems/GettingStarted/ page and I think other than CAmkES, ports and Qubes there could be many more titles. D) I know the major development platform of seL4 has been the Arm architecture, but optimizing the code to utilize the x86 architecture including virtualization can also bring a lot of attention to this project to use seL4 as a replacement for Linux-KVM and Xen in the cloud, IoT or real time systems when stability and security is a matter. Also please note, the archive of both development ( https://sel4.systems/pipermail/devel/) and announcements ( https://sel4.systems/pipermail/announce/) mailing lists are not accessible trough the website. I'm an OS researcher and a senior system engineer (mostly Linux) with a limited time, but I can help in some parts if you think it may be useful. Thank you again! Best Regards, Mehdi

2 1

other communications
by Raymond Jennings 17 Aug '15

17 Aug '15

Is there a mailinglist or forum anywhere for people interested in using seL4? I realized this is a dev list and may not be the right place to ask technical supportr questions.

2 1

Detecting dirty/accessed page tables
by Raymond Jennings 15 Aug '15

15 Aug '15

Hey I'm just curious...how do you detect if a memory page mapped by a page table has been written to or accessed? I imagine if you're writing a filesystem task, such information would help you know when to flush data back to disk or which pages to keep around if things get tight. I hope this isn't a stupid question.

5 16

U-boot help sabrelite
by Andrew Shruhan 11 Aug '15

11 Aug '15

Hi, I am attempting to follow the tutorial booting from SPI for the sabrelite https://sel4.systems/Hardware/sabreLite/ when booting I obtain this output and am not able to run "run bootsel4_mmc" U-Boot 2009.08-dirty (Jun 27 2013 - 16:26:46) CPU: Freescale i.MX6 family TO1.2 at 792 MHz Temperature: 36 C, calibration data 0x56a4bc7d mx6q pll1: 792MHz mx6q pll2: 528MHz mx6q pll3: 480MHz mx6q pll8: 50MHz ipg clock : 66000000Hz ipg per clock : 66000000Hz uart clock : 80000000Hz cspi clock : 60000000Hz ahb clock : 132000000Hz axi clock : 264000000Hz emi_slow clock: 132000000Hz ddr clock : 528000000Hz usdhc1 clock : 198000000Hz usdhc2 clock : 198000000Hz usdhc3 clock : 198000000Hz usdhc4 clock : 198000000Hz nfc clock : 24000000Hz Board: MX6Q-SABRELITE:[ POR] Boot Device: I2C I2C: ready DRAM: 1 GB MMC: FSL_USDHC: 0,FSL_USDHC: 1 JEDEC ID: 0xbf:0x25:0x41 Reading SPI NOR flash 0xc0000 [0x2000 bytes] -> ram 0x276009b8 SUCCESS In: serial Out: serial Err: serial Net: got MAC address from IIM: 00:19:b8:01:fd:6d FEC0 Hit any key to stop autoboot: 0 AHCI 0000.0000 1 slots 1 ports ? Gbps 0x0 impl SATA mode flags: No port device detected! Unknown command 'load' - try 'help' SATA device 1: unknown device Unknown command 'load' - try 'help' Card did not respond to voltage select! mmc0(part 0) is current device Unknown command 'load' - try 'help' mmc1 is current device Unknown command 'load' - try 'help' Unknown command 'usb' - try 'help' Unknown command 'usb' - try 'help' Unknown command 'load' - try 'help' Unknown command 'usb' - try 'help' Unknown command 'load' - try 'help' 6x_bootscript not found serial console at 115200, 8N1 details at http://boundarydevices.com/6q_bootscript AHCI 0000.0000 1 slots 1 ports ? Gbps 0x0 impl SATA mode flags: No port device detected! AHCI 0000.0000 1 slots 1 ports ? Gbps 0x0 impl SATA mode flags: No port device detected! Card did not respond to voltage select! mmc0(part 0) is current device expose mmc drive 0 over USB Unknown command 'ums' - try 'help' Card did not respond to voltage select! no block devices found ERTOS MX6Q SABRELITE U-Boot > -- -Andrew Andrew P. Shruhan Research and Development Engineer III DocBox, Inc. 320 Nevada St Newton MA, 02460 Work: 857-598-2819 ext. 117 www.docboxinc.com

2 2

Upstream seL4/RISC-V work?
by Hesham ALMatary 09 Aug '15

09 Aug '15

Hi, The seL4/RISC-V port is now working on Spike (emulator), Rocket Chip (FPGA), and jor1k (online emulator). I've also written a recent blog post how to build/run the port with SOS project [1] from my repos). The code is pretty much like the ARM port, and following the same bootstrapping procedure (more on this on my blog). MMU code provides 4KiB and 4MiB pages (like IA-32). I'd like to ask if there are special requirements to upstream this work: * All libraries that are target-dependant. * seL4 microkernel. * Tools (elf loader, build system). * SOS project? I understand it won't be an easy process because this work is the first "foreign" code that big, of course apart from formal verification. But it wouldn't hurt to ask. [1] http://heshamelmatary.blogspot.co.uk/2015/07/howto-build-and-run-sel4-on-ri… Best, -- Hesham

4 4

Porting Linux driver into Sel4
by Shabnam Engineer 09 Aug '15

09 Aug '15

HiI have a question about porting Linux drivers in Sel4.Can I port Linux drivers into Sel4? I know that DDEKit provides such functionality for L4-based systems and I could find the implementation of that in fiasco.OC microkernel, but I can not find same works for Sel4. I want to implement Sel4 on a board and test some features, At first I want to be sure that if I need a driver for our special tests and the Sel4 does not support that, Could I choose it from Linux drivers and port it to Sel4 microkernel? Thank you for your considering my question.Regards,Shabnam

1 0

Wandboard Port
by Robert Kaiser 29 Jul '15

29 Jul '15

Hello, in an attempt to familiarize myself with the seL4 code, I am trying to "port" it to the Wandboard (see www.wandboard.org) This should be an easy task for a beginner (thought I) since the board is very similar to the SabeLite, and seL4 is already running well on that board. I have access to a SabreLite and a Wandboard Quad, both (according to U-boot) have the same revision of the iMX6 SoC installed. Differences between the Sabre and the Wand I have noticed so far are: - 2GB of RAM from (0x10000000 to 0x90000000) on the Wand (Sabrelite has 1GB) - Wand uses UART1 for debug output, Sabrelite: UART2 I compiled an sel4test project where I adapted the UART port in kernel/include/plat/imx6/plat/machine/devices.h and elfloader/src/arch-arm/plat-imx6/platform.h and the RAM size in kernel src/plat/imx6/machine/hardware.c. When I boot this system, I get: Jumping to kernel-image entry point... Bootstrapping kernel Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on data at address 0x9f11c2e0 with status 0x1c06 in thread 0xffdfad00 at address 0x13294 (Needless to say, "all is well in the universe" on the SabreLite... ) What is not shown here are a ton of other debug messages which I have added to convince myself that kernel initialization completes as expected. The crash seems to happen upon entry into user code. The address 0x13294 is the virtual address of the entry point: $ nm build/arm/imx6/sel4test-driver/sel4test-driver.bin | grep 13294 00013294 T _sel4_start I suspect that this fault happens on opcode fetch, because the user code is not properly mapped when invoked. Does "status 0x1c06" confirm this? If so, *should* the code be mapped at this point or are these mappings expected to be installed "on demand", i.e. through page fault handling? Thanks for any help... Robert -- Robert Kaiser Computer Engineering RheinMain University of Applied Sciences

3 14

Happy Birthday, Developers!
by Gernot Heiser 29 Jul '15

29 Jul '15

Hi everyone, Today is the anniversary of the open-sourcing of seL4. At NICTA we’re celebrating, I hope you’ll virtually join us ;-) Let me add that I quite enjoy this mailing list. Traffic has a high signal-noise ratio (apologies for degrading it with this message ;-) people generally seem to know what they are doing, and the community is clearly growing. Presently there are over 300 addresses on the list. Many thanks from all of us at NICTA, and keep it up! Gernot [cid:1374281D-B193-431C-AA3F-D6EE049C461A@keg.ertos.in.nicta.com.au] ________________________________ 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.

2 1

CMake and seL4
by Wink Saville 29 Jul '15

29 Jul '15

In my opinion the edit/compile/test loop with the standard build system seeed slow, so I thought I'd try to see if CMake might be any better. Here <https://github.com/winksaville/sel4-newlibs-manifest> is repo manifest which uses CMake for building my sel4-newlibs helloworld application and I'm happy to report there is some improvement. For a "clean" build it is about 2x faster, 8 seconds as compared to 14 seconds. And for a small change to apps/helloworld/src/main.c it is 20x faster, 0.3 seconds as compared to 7 seconds. Is there any interest in using CMake or other build system to reduce the builds times for seL4? -- Wink

2 2

seL4 runs on Rocket Chip (RISCV/FPGA)
by Hesham ALMatary 17 Jul '15

17 Jul '15

Hi all, This is a status update of the seL4/RISC-V project. It can run now on Rocket Chip (FPGA) and jor1k (online emulator), for more details have a look at this link [1]. [1] http://heshamelmatary.blogspot.co.uk/2015/07/sel4-runs-on-rocket-chip-riscv… Thanks, -- Hesham

1 0

Some questions about seL4 operating system
by Qing Wei 16 Jul '15

16 Jul '15

Hi, I am a beginner to seL4 as well as microkernel, and very interested in it. I think it is great in terms of its minimality and formally verified security. However, I have some questions about it, (1) How is its performance compared to other monolithic kernel, say, Linux. Could it make use of multicore, multiprocessor to enjoy the performance scalability? (2) How is its ecosystem, fox example, how to support new hardware, does it need write the driver from scratch or could it make use of Linux driver? And how to write application on it, or, could it run Linux application without modification? (3) How is its virtualization support, could it run Linux vm, and does it need any modification to the guest os? Cheers, Qing Wei

1 0

what are these comments meaning
by Pei.XiLong(裴喜龙) 15 Jul '15

15 Jul '15

Hi, In recent seL4 commit https://github.com/seL4/seL4/commit/67d8d041de0c435a1cc59ef8c237be6e39beb1c6 , A lot of comments like these: /** AUXUPD: "(True, ptr_retyps (2 ^ (unat \<acute>userSize)) (Ptr (ptr_val \<acute>regionBase) :: cte_C ptr))" */ /** GHOSTUPD: "(True, gs_new_cnodes (unat \<acute>userSize) (ptr_val \<acute>regionBase) (4 + unat \<acute>userSize))" */ have been added into source code, What is their meaning? I don't know isablle, and just know a little about haskell. thanks! Xilong Pei Tongji University 2015/7/14

2 1

Raspberry Pi version for learning about seL4
by Simon Apperley 13 Jul '15

13 Jul '15

Hi, I wondered if there was any news on the Raspberry Pi 2 port of seL4 which I saw mentioned when I did a search? I am interested in using the Raspberry Pi to learn about seL4 - not as a target for a full system (as I know there is an issue with trusting the boot mechanism). I just thought it would be a nice platform to use to get my head around seL4 and experiment with virtualising Linux and maybe Android? Simon Sent from my iPad

2 1

reply: This checkin cause a build error
by XilongPei(裴喜龙) 13 Jul '15

13 Jul '15

Hi, Adria, I have fix this build error, it is because I use an old version of apps/sel4test-driver/scripts/extract-test-names.sh I am developing an operating system which can support Microsoft COM like component programing module based on seL4, so I have to sync every repository manually. Xilong Pei Tongji University 2015/7/13

1 0

This checkin cause a build error
by XilongPei(裴喜龙) 13 Jul '15

13 Jul '15

Hi, This checkin cause a build error: Drop static qualifier from tests so that C++ compilers will use extern C linkage instead of name mangling https://github.com/seL4/libsel4test/commit/930744eaf43260ceb37ce2793eefbe77c d808ff0 the error information: .../libs/libsel4test/src/test.c:161: undefined reference to `__start__test_case' .../libs/libsel4test/src/test.c:161: undefined reference to `__stop__test_case' Xilong Pei Tongji University 2015/7/13

2 1

Streamline seL4/libsel4 and make it not depend on libc
by Wink Saville 10 Jul '15

10 Jul '15

I've got sel4test running with libsel4 not having a dependency on libc. I've pulled out libsel4assert, libsel4benchmark, libsel4printf and libsel4putchar from libsel4 and they are separate libraries The biggest change is to seL4/libsel4 and sel4/tools/bitfield_gen.py. The changes to bitfield_gen.py allow it to generate the same code as before for the kernel but uses the new names for entities in user space. Please let me know what you think. -- Wink https://github.com/winksaville/seL4/tree/libsel4-no-libc-dependency https://github.com/winksaville/libsel4test/tree/libsel4-no-libc-dependency https://github.com/winksaville/libsel4allocman/tree/libsel4-no-libc-depende… https://github.com/winksaville/libsel4utils/tree/libsel4-no-libc-dependency https://github.com/winksaville/sel4test/tree/libsel4-no-libc-dependency https://github.com/winksaville/libsel4assert https://github.com/winksaville/libsel4benchmark https://github.com/winksaville/libsel4printf https://github.com/winksaville/libsel4putchar

4 11

can IPC be concurrent running?
by Pei.XiLong(裴喜龙) 07 Jul '15

07 Jul '15

Hi, We can get the definition of IPCBuffer from here https://github.com/seL4/seL4/blob/master/libsel4/arch_include/arm/sel4/arch… enum { seL4_GlobalsFrame = 0xffffc000, }; It is fixed in one virtual space, that means the IPC in seL4's thread cann't be concurrent, we can't prepare more than 1 IPC request at the same time, for we call these function: seL4_SetTag, seL4_SetMR, seL4_SetUserData wil use this buffer, but there is no locker to protect the buffer. Is my understanding correct? Xilong Pei Tongji University 2015/7/6

1 0

Where is the definition of seL4_TCB_BindAEP and seL4_TCB_UnbindAEP?
by XilongPei(裴喜龙) 07 Jul '15

07 Jul '15

Hi, In test program binding.c https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/src/tests/b inding.c , there are two functions, seL4_TCB_BindAEP and seL4_TCB_UnbindAEP, where can I get their definitions? Xilong Pei Tongji University 2015/7/6

2 1

Try two for libsel4 not having a dependency on libc
by Wink Saville 04 Jul '15

04 Jul '15

Here <https://github.com/winksaville/sel4-min-sel4/tree/new-libs> is a different approach for removing the libc dependency, it seemed like people thought libsel4 was to big and that as part of the effort of breaking the dependency it should be made smaller. Basically libsel4 does nothing expect satisfy dependency needed for the kernel for some xml files. And I've broken libsel4 into basically 8 other libraries. see here <https://github.com/winksaville/sel4-min-sel4/tree/new-libs/libs>. This maybe taking things to far, but it does mean people can use only what they need, which I like. The smallest example is app/min-hw which only uses libsel4_gen, libsel4_startup. libsel4_bootinfo and libsel4_putchar. At the other extreme apps/test-newlibs uses everything. Anyway other organizations are certainly possible. Currently there is at least one known problem, I modified bitfield_gen.py so types_gen.h has no asserts since at the moment the kernel uses assert and userspace is libsel4_assert. We could either do something like I've done and remove them or change the kernel to use libsel4_assert or something else. Anyway, before creating a pull request I'd like to know what people think. -- Wink

4 12

Who can give me a sample program using sel4platsupport_new_io_ops
by XilongPei(裴喜龙) 01 Jul '15

01 Jul '15

Hi, sel4platsupport_new_io_ops is defined in libsel4platsupport/include/sel4platsupport/io.h , it creates a new implementation of the platsupport io_ops interface using a provided simple, vspace and vka, Here is its protocol: /* * @param simple Simple interface for getting the physical frames * @param vspace VSpace interface to use for mapping * @param vka VKA interface for allocating any extra objects or cslots * @param io_ops Interface to fill in * * @return returns 0 on success */ int sel4platsupport_new_io_ops(simple_t simple, vspace_t vspace, vka_t vka, ps_io_ops_t *io_ops); Who can give me a sample program using this function? I guess it will be used in I/O DMA program, but I don't know much about DMA program. Xilong Pei Tongji University 2015/7/1

1 0

Make seL4/libsel4 not depend upon libc
by Wink Saville 29 Jun '15

29 Jun '15

I noticed that seL4/libsel4 was dependent upon libc and so I created a patch ( https://github.com/winksaville/seL4/commit/fc91a1f68c054fdb41aaa42a7b56a80f…) which removes the dependency. If there is interest I can submit a pull request, and of course will make any changes deemed necessary to make it suitable for acceptance. Please advise, Wink

6 11

How to edit RefOS libs c file
by ぷ风过无痕?? 22 Jun '15

22 Jun '15

Hi, I am using RefOS to develop a small applicaiton(interprocess comunicaion).I need to edit some c files in RefOS/libs/librefos directory,But comments say that do not edit these files,these files were generated by CIDL.CIDL is a simple C IDL compiler which is made to save the trouble of manually implementing RPC interface stubs to marshal C style arguments and return value. It uses a simple XML-based IDL language. I search on the google，but just got some introduction. So where can I got some useful infomation about CIDL? Can you recommend some books or websites? ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Sun, Jun 21, 2015 10:00 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 13, Issue 11 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: Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC (da Tyga) ---------------------------------------------------------------------- Message: 1 Date: Sat, 20 Jun 2015 16:26:46 +1000 From: da Tyga <cyberfonic(a)gmail.com> To: devel(a)sel4.systems Subject: Re: [seL4] Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC Message-ID: <CALj3Nd3+CFFQF41BOwW+-bwFNOEZS9HyVLHDwVssTyMAcsU3ig(a)mail.gmail.com> Content-Type: text/plain; charset="utf-8" > > > Hi Yuxin, I don't think you need to modify GCC, it is the compiler that you can use to generate required executables. Making changes to it is a massive undertaking. Instead of trying to reinvent stuff that has already been done, you really should read the Genode documentation and download and read the source code referenced by Norman Feske's suggestions. >From my reading of the Genode documents and source code, I would expect that you would find a considerable amount of code that you could you re-purpose for your specific requirements. Cheers, Tyga > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 19 Jun 2015 22:46:40 +0800 > From: Yuxin Ren <ryx(a)gwmail.gwu.edu> > To: Norman Feske <norman.feske(a)genode-labs.com> > Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] Does sel4 support c++ > Message-ID: > <CAAKbDrcbyh0YV+nHzhziiiXavn-= > P_tW5bS2LUfPzHcBF-iMKg(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Thank you all! > > If modifying the tool chain is the easiest way, I want to try it. > But I definitely want to avoid creating the tool chain from "bare metal". > I still prefer to reuse the existing tool chain like gcc > with minimal modification. > > Could you give me some guidance how to create a custom tool chain, which > part I need to modify? > I am not familiar with gcc. So if I have to modify gcc, where can I get > more information or documentation? > > Thanks a lot!! > Yuxin > > On Thu, Jun 18, 2015 at 9:50 PM, Norman Feske < > norman.feske(a)genode-labs.com> > wrote: > > > Hello, > > > > > The easiest approach is possibly to create a custom tool chain, and > port > > > the GCC C++ library that way. I know the people behind Genode did some > > > of this (http://genode.org/download/tool-chain) although I'm not sure > > > how much of the C++ standard library they actually support. > > > > more in-depth information about Genode's tool chain are provided by > > Section 7.2 of the documentation [1]. In short, the tool chain is a > > "bare metal" tool chain that does not depend on a C library, yet it > > still supports C++ (including exceptions and runtime type information). > > > > On Genode, the libc and STL (aka stdcxx) can be used optionally whereas > > the STL depends on the libc. The libc is based on FreeBSD's libc. The > > STL is GCC's version. Both libraries are available via Genode's ports > > mechanism. > > > > That said, as both the libc and stdcxx are shared libraries, they cannot > > be used on the seL4 version of Genode as of now. Shared libraries don't > > work on seL4 (at least on x86_32) because the system-call bindings > > cannot be compiled with -fPIC. > > > > [1] http://genode.org/documentation/genode-foundations-15-05.pdf > > > > Best regards > > Norman > > > > -- > > Dr.-Ing. Norman Feske > > Genode Labs > > > > http://www.genode-labs.com ? http://genode.org > > > > Genode Labs GmbH ? Amtsgericht Dresden ? HRB 28424 ? Sitz Dresden > > Gesch?ftsf?hrer: Dr.-Ing. Norman Feske, Christian Helmuth > > > > _______________________________________________ > > 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/20150619/5b4ce704/attachmen… > > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > ------------------------------ > > End of Devel Digest, Vol 13, Issue 10 > ************************************* > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20150620/c72cfc07/attachmen…> ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 13, Issue 11 *************************************

4 3

Re: [seL4] Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC
by da Tyga 22 Jun '15

22 Jun '15

> > > Hi Yuxin, I don't think you need to modify GCC, it is the compiler that you can use to generate required executables. Making changes to it is a massive undertaking. Instead of trying to reinvent stuff that has already been done, you really should read the Genode documentation and download and read the source code referenced by Norman Feske's suggestions. >From my reading of the Genode documents and source code, I would expect that you would find a considerable amount of code that you could you re-purpose for your specific requirements. Cheers, Tyga > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 19 Jun 2015 22:46:40 +0800 > From: Yuxin Ren <ryx(a)gwmail.gwu.edu> > To: Norman Feske <norman.feske(a)genode-labs.com> > Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] Does sel4 support c++ > Message-ID: > <CAAKbDrcbyh0YV+nHzhziiiXavn-= > P_tW5bS2LUfPzHcBF-iMKg(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Thank you all! > > If modifying the tool chain is the easiest way, I want to try it. > But I definitely want to avoid creating the tool chain from "bare metal". > I still prefer to reuse the existing tool chain like gcc > with minimal modification. > > Could you give me some guidance how to create a custom tool chain, which > part I need to modify? > I am not familiar with gcc. So if I have to modify gcc, where can I get > more information or documentation? > > Thanks a lot!! > Yuxin > > On Thu, Jun 18, 2015 at 9:50 PM, Norman Feske < > norman.feske(a)genode-labs.com> > wrote: > > > Hello, > > > > > The easiest approach is possibly to create a custom tool chain, and > port > > > the GCC C++ library that way. I know the people behind Genode did some > > > of this (http://genode.org/download/tool-chain) although I'm not sure > > > how much of the C++ standard library they actually support. > > > > more in-depth information about Genode's tool chain are provided by > > Section 7.2 of the documentation [1]. In short, the tool chain is a > > "bare metal" tool chain that does not depend on a C library, yet it > > still supports C++ (including exceptions and runtime type information). > > > > On Genode, the libc and STL (aka stdcxx) can be used optionally whereas > > the STL depends on the libc. The libc is based on FreeBSD's libc. The > > STL is GCC's version. Both libraries are available via Genode's ports > > mechanism. > > > > That said, as both the libc and stdcxx are shared libraries, they cannot > > be used on the seL4 version of Genode as of now. Shared libraries don't > > work on seL4 (at least on x86_32) because the system-call bindings > > cannot be compiled with -fPIC. > > > > [1] http://genode.org/documentation/genode-foundations-15-05.pdf > > > > Best regards > > Norman > > > > -- > > Dr.-Ing. Norman Feske > > Genode Labs > > > > http://www.genode-labs.com ? http://genode.org > > > > Genode Labs GmbH ? Amtsgericht Dresden ? HRB 28424 ? Sitz Dresden > > Gesch?ftsf?hrer: Dr.-Ing. Norman Feske, Christian Helmuth > > > > _______________________________________________ > > Devel mailing list > > Devel(a)sel4.systems > > https://sel4.systems/lists/listinfo/devel > > >

2 1

Does sel4 support c++
by Yuxin Ren 19 Jun '15

19 Jun '15

Hi, Can I run C++ programs on sel4? I am not familiar with programming language. I do not know the relationship between the OS and the C++ language. In order to run C++, does the OS need to provide some support or what user level library are needed? Thanks a lot. Yuxin

4 6

Virtualization extensions
by Nick Betteridge 15 Jun '15

15 Jun '15

Hi I'm very interested in working with the virtualization extensions on sel4 - is there any rough timeline for when these will be available. Thanks Nick

1 0

high-availability system should have these software services
by XilongPei(裴喜龙) 15 Jun '15

15 Jun '15

Hi, In general, a high-availability system should have the following software services http://electronicdesign.com/boards/high-availability-rtoss-deliver-five-nine s-reliability : - Heartbeat support for each server and each application. - Event management capability for change notification. - Alarm management for error handling. - Transactions capability for check-pointing and rollback/restart. - Clustering for server management and applications links. - Reliable storage support for RAIDs and for journaling file systems. I want to develop a high-availability system on seL4, can anyone give me some suggestions? QNX has high availability support http://www.qnx.com/developers/docs/6.3.0SP3/neutrino/sys_arch/ham.html , can we learn something from them? Xilong Pei Tongji University 2015/6/11

6 7

[sel4] seL4 on RISC-V is running SOS (Simple Operating System)
by Hesham ALMatary 09 Jun '15

09 Jun '15

Hi all, This is the second status update of the project (Porting seL4 to RISC-V). Please have a look at the blog post [1] for more details, and feel free to ask and/or comment. You feedback would be appreciated. [1] http://heshamelmatary.blogspot.co.uk/2015/06/sel4-on-risc-v-is-running-sos-… Thanks, -- Hesham

2 1

Sel4 and Network
by Haselauer Lukas - S1410304006 03 Jun '15

03 Jun '15

Hello, My name is Lukas and I am currently studying in Austria. I am currently using sel4 in a student's project. We are using CAmkES to develop a small application (on the imx6-platform), and some things already work fine :-) But when it comes to networking, we are totally without results. We tried using some of the excisting libraries (libethdrivers + libplatsupport + liblwip) - but without success. My question is: Which way can I go if I want my CAmkES Apps to communicate via ethernet? Do I have to implement a driver as part of the App? As an additional library? Or somewhere else? I really couldn't figure out how to do it properly... Is there some sort of documentation or example on how to get a IP-stack up and running on sel4? Thank you for reading and helping! Lukas

2 1

Hello world - simple example thread creation
by Piotr 30 May '15

30 May '15

I would like to start from scratch - simple thread or process creation helloworld in seL4. I saw there are some examples in "sel4test/app" of seL4 application, but I am looking for something smaller. I have found here on page 39 "Creating a Thread in Own AS and cspace_t" http://www.cse.unsw.edu.au/~cs9242/14/lectures/01-intro.pdf example of thread creation. Unfortunetly I cannot find header file with " cspace_ut_retype_addr" or "ut_alloc". Are they obsolete, any replacements? Are there any small and simple hello-world tutorials or examples avaliable?

1 0

why do there are some differences between camkes branch and master branch in lib seL4/libsel4muslcsys
by Pei.XiLong(裴喜龙) 29 May '15

29 May '15

Hi, Siwei Zhuang, Why do there are some differences between camkes branch and master branch in lib seL4/libsel4muslcsys? The lib seL4/libsel4muslcsys is the foundation of libmuslc, it shoud be a libc for any seL4 program, and there should be no diference among any branches. https://github.com/seL4/libsel4muslcsys/commits/camkes Xilong Pei Tongji University 2015/5/29

3 3

[sel4] Porting seL4 to RISC-V - Status Report 1
by Hesham ALMatary 26 May '15

26 May '15

Hi all, As a warm up, I've written a blog entry [1] of the project giving some introductory details for both RISC-V and seL4 microkernel and what has been done so far. Open to questions/suggestions. [1] http://heshamelmatary.blogspot.co.uk/2015/05/porting-sel4-to-risc-v-status-… Thanks, -- Hesham

2 3

Progress of bringing Genode to seL4
by Norman Feske 26 May '15

26 May '15

Hello, I have written up the first of a series of articles about using seL4 as base platform for the Genode OS framework: http://genode.org/documentation/articles/sel4_part_1 I hope that it contains useful bits of information for novices of seL4 and Genode alike. Even though the article outlines a few hurdles, the overall experience of using the kernel had been overly positive so far. For those of you interested in tracking the progress of the ongoing work, here is the corresponding topic branch: https://github.com/nfeske/genode/commits/sel4 Cheers Norman -- Dr.-Ing. Norman Feske Genode Labs http://www.genode-labs.com · http://genode.org Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

4 7

Virtual address space (kernelBase) restriction
by Hesham ALMatary 22 May '15

22 May '15

Hi all, Is it a must that every platform/architecture mapped to virtual addresses higher than 0xF0000000? Thanks -- Hesham

1 0

lowRISC Google Summer of Code
by Stefan Wallentowitz 18 May '15

18 May '15

Hi all, I just wanted to take the chance to introduce Hesham ALMatary and myself. Hesham participates in Google's Summer of Code in the lowRISC organization and I am his mentor. During summer, Hesham will port seL4 to the RISC-V architecture, specifically for the lowRISC project. Please find more details here: http://www.lowrisc.org/blog/2015/05/summer-of-code-students-for-lowrisc/ Hesham and I will keep you updated about the progress, I believe he will also give updates in his blog: http://heshamelmatary.blogspot.it/. Best Regards, Stefan

2 1

sel4 example compilation - cygwin
by Piotr 12 May '15

12 May '15

Hi, I am trying to compile example from 'Download' tutorial under Cygwin. http://sel4.systems/Download/ What I get is: [KERNEL] [BF_GEN] arch/object/structures_gen.h [BF_GEN] plat/machine/hardware_gen.h [BF_GEN] api/types_gen.h [CPP] src/arch/ia32/machine_asm.s [AS] src/arch/ia32/machine_asm.o /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S: Assembler messages: /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:15: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:15: Error: junk at end of line, first unrecognized character is `o' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:20: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:20: Error: junk at end of line, first unrecognized character is `o' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:22: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:22: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:26: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:26: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:30: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:30: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:34: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:34: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:36: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:36: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:41: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:41: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:43: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:43: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:49: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:49: Error: junk at end of line, first unrecognized character is `i' .......... What to do with it?

4 3

CSpace: resolveAddressBits
by Norman Feske 04 May '15

04 May '15

Hello, I am trying to construct a custom CSpace for my root task using seL4's guarded page-table concept. At the 1st level, there is a CNode with a radix of 12 and a guard of 0. At the 2nd level, there is a CNode with a radix of 14 and a guard of 6. After copying the initial capabilities to the 2nd-level CNode, switching to this CSpace, and invoking a system call that takes a capability as argument (seL4_TCB_Suspend), the kernel tells me: <<seL4 [decodeInvocation/609 Te3ffa880 @10245c2]: Attempted to invoke a null cap #1.>> The problem seems to be a failed 'lookupCapAndSlot', which internally calls 'resolveAddressBits': https://github.com/seL4/seL4/blob/experimental/src/kernel/cspace.c#L138 While inspecting the function, it does not appeared to me why it does not consider any guard bits within the while loop. The 'levelBits' variable is simply set to 'radixBits'. Interestingly, the same function in the master branch looks different. Here, the 'guardBits' are taken into account, which is consistent with the documentation. I wonder, why differs the experimental branch to the master branch in this respect? Is there a way to construct the scenario above with the experimental branch? The only work-around I see is to allocate an intermediate CNode with a size of 2^6 that sits between the 1st and 2nd level. Or is there a better way? Best regards Norman -- Dr.-Ing. Norman Feske Genode Labs http://www.genode-labs.com · http://genode.org Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

2 2

Does sel4 support pthread?
by 小健 24 Apr '15

24 Apr '15

I am using sel4 to develop a multi-thread program on ARM platform. I know that sel4 support musl libc. But when I call __pthread_create the program returns an error. Does sel4 support pthread on ARM platform? By the way, I get the libmuslc from seL4test. So if there is a musl libc which has pthread inside that can be used by sel4, please tell me where I can get it. Thank you.

2 1

Port seL4 to allwinnerA20
by Jensen Zhang 20 Apr '15

20 Apr '15

Hello everyone, We have ported seL4 to allwinnerA20, although the cache cannot still work well. All tests passed, except for CACHEFLUSH0001 and CACHEFLUSH0002. A git clone can be gotten from here [1]. And the 'zener' directory in this project has a similar structure to sel4test. But there is a problem about TIMER API. For allwinnerA20, there are several registers (Timer IRQ Enable/Status Register) used by all timers. Both kernel and libsel4platsupport will use timers, and they have to use different timers. But some registers can be accessed by both kernel and libsel4platsupport. That's very dangerous! Because libsel4platsupport can disable the timer of kernel by modifying the register. How to solve this problem? [1] git clone http://elastos.org/review/HD-Elastos -- Jensen Zhang Tongji University

2 1

am335x patches - refos working
by Tim Newsham 13 Apr '15

13 Apr '15

RefOS is now working fine on am335x / beaglebone black. Patches attached. Tim

4 3

How to get a helper thread's TCB?
by Kun Cheng 11 Apr '15

11 Apr '15

Hi guys, Currently I'm working on something that requires threads can be moving between domains. I can run two domains now (trying to run more) and I'm trying to understand the content of domain.cxx in sel4-test. Each thread has TCB which contains the domain id of it. But after running through *struct helper_thread* and relevant data structures, I'm curious about how to retrieve a helper thread's domain id, which could help me verify that they're indeed moved to another domain. Best regards, Kun Cheng

1 0

Regarding Bootstrapping the Kernel
by Sebastian Lau 08 Apr '15

08 Apr '15

On the http://sel4.systems website, it says that like qnx, sel4 expects to be elf-loaded. Could you please explain what that means?

2 1

SeL4 As Hypervisor
by CACook＠quantum-sci.com 02 Apr '15

02 Apr '15

After weeks trying to make Xen pass through an Intel IGP to the VM, I've finally found that it simply doesn't work. That's enough time spent on that.... My goal is to use a microkernel for hypervisor, which supports up to 10 VMs that perform various functions. The most challenging one is a VM which plays video using hardware accel of the integrated graphics processor, and sends and receives commands over a USB device. All my VMs will be CentOS. >From the FAQ I infer that it requires coding skills to do anything more than install base seL4. True? If not, have others set up an seL4 machine with multiple VMs and written how they did it and how it went? I should note that I am not a coder, although I am well experienced with Linux admin and scripting.

3 3

libsel4cspace?
by Ted Cooper 27 Mar '15

27 Mar '15

I'm adapting the aos-2014 exercises from http://www.cse.unsw.edu.au/~cs9242/14/project/index.shtml so I can run them under IA32 qemu. Milestone 0's sos project depends on stuff from libsel4space, e.g. cspace_root_task_bootstrap(). From a cursory search, it seems like this library isn't on the seL4 github account. Is this because its functionality has been rolled into one of the other libsel4*, or because it's a course-specific library not intended to see the light of day?

2 1

Cannot run on more than 1 domian?
by Kun Cheng 26 Mar '15

26 Mar '15

Hey guys, It seems that sel4test can only run on 1 domian (with CONFIG_NUM_DOMAINS=1 in .config), I tried to set it to 4 or a larger one (<=16) but when I ran the image with qemu it gave me an error "seL4 failed assertion '_ndks_end - _ndks_start <= NDKS_SIZE' at /home/kenneth/sel4/sel4current/kernel/src/arch/ia32/kernel/boot_sys.c:447 in function try_boot_sys". Is there any other configurations or code that I have to change? PS: I've been suffering a problem that I can only receive devel digests recently but none of your emails could reach me. This is weird because I set no filter in gmail. Best regards, Kun Cheng

1 0

Getting Started
by Fred 24 Mar '15

24 Mar '15

>From the main page. "If you would like to learn how to build a system on seL4, you might want to follow the lectures and especially the seL4-based project of UNSW's Advanced Operating Systems course <http://cs9242.web.cse.unsw.edu.au/>." Request: Is it possible to obtain access to the recorded lectures as well as the notes? Also assignment templates appear to be only available to enrolled students. I understand that publicly posting solutions to the assignments may be a problem. e.g. git clone ssh:// YOURLOGIN@login.cse.unsw.edu.au//home/cs9242/public_html/current/project/files/aos-2014 Background: Our project is in the internally funded phase of an open-source platform for medical simulation and training (similar to SimMan). The system consists of intercommunicating modules where each module runs a minimal OS. Thanks

4 5

beagle bone docs on page?
by Tim Newsham 21 Mar '15

21 Mar '15

Now that sel4, sel4test and refos work on beaglebone, perhaps it could be mentioned on the sel4 web page? If there's anything I can do to help make that happen, please let me know. Tim

2 1

seL4 + Qubes OS Project
by WhonixQubes 20 Mar '15

20 Mar '15

Hello, I am the maintainer of the Qubes + Whonix project... https://www.whonix.org/wiki/Qubes Which is the port of Whonix OS (think a more secure Tor proxied VM) to Qubes OS, which has upstream integration into the Qubes codebase now. I am very interested in secure minimal kernels and hypervisors, and have been discussing these topics publicly and privately with other interested developers and investors recently. And I am also positioning to bring development resources to low-level projects that can achieve a more optimal (and verifiable) secure TCB than bloated Linux-based systems, as Qubes Dom0 is currently based upon. Actually being able to read through and know all the code that is running on a mission critical machine, a novel thought, huh. ;) I am most interested in this Qubes blurb on the seL4 website... https://sel4.systems/GettingStarted "Qubes is an open source operating system designed to provide strong security for desktop computing using virtualisation to provide isolation. Qubes is based on Xen. seL4 is a much better fit for Qubes. The project is to port Qubes to seL4 (or develop an alternative Qubes-like system for seL4)." I absolutely agree with this and would like to know more about what Qubes development project might already underway be in the seL4 community in order to consider the opportunity of providing some real assistance in the future. What's the status of this seL4 Qubes port project and who can I get in touch with to talk more about accomplishing it? Thanks! :) WhonixQubes

7 7

Emit debugging info
by Hesham ALMatary 18 Mar '15

18 Mar '15

Hi all, This is most likely a straight forward question: how can I get debugging symbols for the final image (if possible)? I am configuring/compiling seL4tests for example with "make kzm_simulation_debug_xml_defconfig", etc. And when I try to dump the generated "sel4test-driver-image-arm-imx31" content with "arm-none-eabi-objdump" command, I can't find any debugging symbols (function/variable names) although debugging flags are set. If the previous question is not valid, then how can I debug the generated image using QEMU/gdb if possible? and trace the program execution beginning from _start? Other solutions for debugging are appreciated. Thanks in advance. -- Hesham

2 2

About the latest commit of seL4 kernel
by Jensen Zhang 15 Mar '15

15 Mar '15

Hello, I found there are several little changes on the latest commit of seL4 kernel [1]. And you just changed the define of function "map_it_frame_cap" for arm, but not for ia32. I just wonder whether there are any further considerations, or it's just a mistake :) Thanks, [1] https://github.com/seL4/seL4/commit/4f12acd2703183c9f44fe097589b53eb53c599eb -- Jensen Zhang Tongji University

2 1

refos and sel4-test questions
by Tim Newsham 15 Mar '15

15 Mar '15

Is it possible to build and run sel4-test against the "experimental" kernel tree? if so, whats the process? On RefOS for my port, I'm seeing a weird problem with the timer code. It is mapping in the right phys addr for my timer device, and I can read the right ID register out, so it appears to be mapping the right memory, but the code to do a timer reset, which sets a reset bit then polls for the bit to return to zero, is getting stuck in an infinite loop. I verified that the loop isn't being altered by the compiler, and I verified that the same code runs fine in sel4 test. At this point I suspect one of two things 1) refos is allowing the mapping to happen with caching on (even though I asked it not to) or 2) something is wrong elsewhere with the "experimental" kernel (sel4-test is running on the "master" tree, and refos is using the kernel from the "experimental" tree). is there anything else I could be missing? any thoughts? -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com

3 2

Porting seL4 to RISC-V
by Hesham ALMatary 14 Mar '15

14 Mar '15

Hi all, I'm Hesham ALMatary a computer science research student at the University of York. I am considering porting L4 microkernel variants to RISC-V [2] (for both my research and Google Summer of Code), and Fiasco.OC is one of these variants, but I want to extend the options here by asking about seL4. Is this project would be: first applicable, and second of interest to you? And if yes, would you offer some help (guidance)? I am sending this message as suggested here [1] that I should contact you if I'm willing to port seL4 to a new platform. [1] http://sel4.systems/GettingStarted/ [2] http://riscv.org/ Thanks, -- Hesham

4 4

seL4 on Raspberry Pi
by da Tyga 10 Mar '15

10 Mar '15

> > IMHO, the biggest problem with the Raspberry Pi is that most of its I/O > (even the NIC) is connected through USB. A serial port is available > (albeit without level shifters). So, running the seL4test should be > possible without a USB stack, but as soon as you want to access a > keyboard, network or filesystem, you'll need one. You should keep in mind that seL4 is a microkernel. So the USB stack and drivers that depend on that stack should all be implemented as processes/tasks running on top of seL4. I know it is not cool to mention Minix here, but it and Plan9 suggest ideas as to how the layers above seL4 could be structured. As far as I can understand, seL4 is not an operating system, it is a microkernel upon which one or more operating systems could be built. The key reason to use seL4 would be due to it providing capabilities based isolation between the layers that run on top of it and thus preventing rogue processes from interfering with other processes.

3 2

A port to the Raspberry Pi 2?
by Sebastian Lau 10 Mar '15

10 Mar '15

Would a port of seL4 to the raspberry pi 2 be welcome because I'm interested in buying a raspberry pi 2 and building sel4 for it?

5 9

docker compatible? (was Re: MySQL - seL4)
by Raoul Duke 07 Mar '15

07 Mar '15

> wouldn't provide you much. What sel4 could buy > you is isolation between mysql and other applications > if you chose to run several processes on the same > machine. The processes themselves, including mysql, > would still be vulnerable to any internal vulnerabilities > they might have (sel4 is not a magic bullet). There's a lot of noise around Docker. I find it annoying for many reasons, including security -- although I do understand some of the attraction. It would be super keen in my mind if seL4 could offer something in that vein, could present itself as a nice alternative.

5 6

MySQL - seL4
by André Bispo 06 Mar '15

06 Mar '15

Hello guys,Do you think it is feasible to have MySQL running on top of seL4 and take advantage of the isolation mechanisms?I was looking into the microkernel, the CamKES project and the mailinglist, to find some answers but i think it would be very difficult, if not impossible to run MySQL on seL4.I'm trying to explore this possibility and i want to know your opinion before continue. Best regards,André Bispo.

3 2

USB booting problem
by André Bispo 04 Mar '15

04 Mar '15

Hello guys, i'm building myself a system for my thesis and i'm currently testing out the seL4.I was trying to boot the sel4test by USB following the tutorial described in another question on this mailing list.But syslinux seems to load the kernel and the test but nothing appears afterwards.This is the message shown: MBRLoading sel4kernel... okLoading rootserver... ok _ If anyone could help me out i'd be very grateful. Best regards,André Bispo.

3 3

am335x - configs and refos
by Tim Newsham 04 Mar '15

04 Mar '15

Attached are some patches for am335x support. I've started to play with refos, and can build it for am335x and run some of the startup (with release mode) but it hangs at some point.. still a work in progress. Also there's a few minor proofread tweaks on the refos doc. By the way, sel4test runs pretty well now in debug and release modes. Instructions are pretty straightforward: - build the project using the debug or release config - use objcopy to extract a raw binary from the ELF image - load the binary with uboot (I use "tftp", it defaults to the proper load address) - run it in uboot with "go 82000000" Tim

2 1

Joint a formally verified C compiler with seL4?
by Grissiom 02 Mar '15

02 Mar '15

Hi all, I've heard a formally verified optimizing C compiler: CompCert recently: http://www.absint.com/compcert/ HN: https://news.ycombinator.com/item?id=9130934 . So what benefit will there be if some one use CompCert as the compiler for seL4? -- Cheers, Grissiom

3 2

Re: [seL4] How are capabilities assigned
by Sebastian Lau 02 Mar '15

02 Mar '15

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?

2 2