Hi Andrew Jackman! First of all apologies about my assumptions. In my hasty reading of your question I got the impression you were talking about yourself and not the intended audience for your tutorial material proposal. Like yourself, I too would use a practical, tutorial style guide if it were available. So I would like to give my vote for your idea. Unfortunately, I'm a one-man-show and thus not in a position to make a pledge towards a tutorial effort. Perhaps the good folks who are involved with seL4 could suggest how your proposal could come about. Reading these digests, tit would appear that there are quite a few people who are trying to come to grips with seL4. Yes, I was referring to the material that you linked. Cheers, Tyga
thread in reverse chrono-order:
Andrew Jackman kd7nyq@gmail.com On Sun, Mar 6, 2016 at 11:04 AM, Jackman <kd7nyq@gmail.com> wrote:
Hi Andrew, I don't wish to discourage you, but if you are just starting out programming and have limited knowledge of operating systems, etc ... then seL4 might be a very big undertaking to understand and learn from. There are a lot of topics you would need to come up to speed on. I suggest taking a look Gernot's course material at unsw.edu.au.
da Tyga: Thank you for writing back. I totally agree with your assessment. Permit me to elaborate a bit more on my situation. I am a professional software engineer who is primarily dedicated to writing virtualization automation software for sales demonstrations. Naturally, our department is always interested in ways in which we can improve the efficiency of our virtualization environment(s). After reading 'L4 Virtualization and Beyond' (2008, http://os.inf.tu-dresden.de/papers_ps/haertig08_l4_virtualization_and_beyond... ), I became fascinated with L4. I am here talking to you all because of the amount of press that seL4 has gotten as the proofed L4 kernel and because it appears to have the best, most easily understood documentation. Now, that does not mean that I think seL4 is well documented, just that it's the best documented of the L4 projects. The purpose of my original email was to very gently say that the introductory material to seL4 is so bad, that I'm willing to pay someone to either bring it up to date, assist me with it, or both. For example, there is a thread about RefOS, wherein Kevin wrote, "RefOS was a student project that is now no longer actively maintained." Gapry and HyperNewbie, however, provided at least some fixes, but their fixes don't appear to have gotten any attention from upstream. This was on 11 February. Nevertheless, RefOS appears to be the only seL4 project geared towards newcomers on the 'Getting Started' page ( https://sel4.systems/Info/GettingStarted/). You should note that, on that page, there is no indicator that newcomers should, in fact, stay away from that project because it's no longer maintained. I don't think requesting some attention on documentation is a bad or unjust thing. I would hope that lowering the barriers to entry to the seL4 community would increase the flow of developers, users, and sponsors to the seL4 project. In turn, I hope that would be seen as a good thing. I'm offering part-time, albeit unofficial, company sponsored development in exchange for some paid tutoring. I am not asking for a hand-out. If I didn't have to worry about ramp-up time or coming up with deliverables, I wouldn't be bugging you. Now, if you're worried about my qualifications, I'm a university educated computer scientist. While I've spent most of my career on web programming, I've studied operating systems development both at school and on my own. I began a toy kernel with the help of the osdev.org resources, and I'm happy with my progress. When I take inventory, however, I realize I don't have the desire to (re-)write an L4 kernel, nor do I think I can improve upon it. Finally, I think you're referring to Professor Gernot Heiser's page at https://www.cse.unsw.edu.au/~gernot/, and probably more specifically the CS9242 course at http://www.cse.unsw.edu.au/~cs9242/current/. If you're referring to another course, please be more specific. Thank you. Andrew Jackman kd7nyq@gmail.com
Just a couple quick answers is issues raised. Improved documentation is desirable for all. There is a few challenges here though as seL4 is closer to being a virtual machine than a traditional OS in the sense that the abstractions are very low level. So documentation could: a) Focus on seL4 and its abstractions, however this is mostly useful to somebody embarking on building an OS personality running on seL4. b) Focus in an existing OS personality on seL4, which is most useful to somebody wanting to build an application, assuming the OS personality meets the requirements of the application domain. Our experience with the advanced OS course (AOS) is that option (a) is a substantial learning curve. Unless you plan on embarking on building an OS personality from the ground up, this would be a challenging place to start (effectively bottom up). The AOS material is online if you want to start from the bottom up. For option (b), and most mature environment is CAmkES (an environment for static systems). It is actively maintained and in use by project partners and community. I’ll prod the locally to see if material from the http://sel4.systems/Community/Devdays/ can be made readily available. An immature environment is RefOS, whose goal was/is a simple multiserver POSIX-ish environment on seL4. RefOS is a little too immature to be the poster child for getting started on seL4. We are definitely interested in seeing it progress, but we have limited resources ourselves to invest (unless I get an interested student again, which is always a possibility). Regarding the patches from Hypernewbie, we’re working on them, we expect to get them out RSN (they have non-trivial conflicts with our current release candidate). Regards - Kevin Assoc. Prof. Kevin Elphinstone, Trustworthy Systems DATA61 | CSIRO E kevin.elphinstone@nicta.com.au<mailto:kevin.elphinstone@nicta.com.au> T +61 2 8306 0573 www.data61.csiro.au<http://www.data61.csiro.au/> CSIRO’s Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 [cid:image001.png@01D0EFD9.052ECFC0] ________________________________ 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.
Hi Kevin, Thank you for taking the time to respond. I have been tracking okL4 developments for what seems like a decade or more. The open sourcing of seL4 was exciting news as it opens up the opportunity for a wider group to make contributions. None of the points you raise come as a surprise. My interest is how we could have trustworthy compute nodes in a IoT / WoT world. I have concerns about the current trend to connect everything via "The Cloud". I think a more secure approach is to have local trustworthy nodes connected via well secured channels to the internet at large. I have also looked at Minix, Plan9 and Inferno. The way I see it, uKernels are the only approach that has a chance of satisfying the trustworthiness criteria and AFAIK, seL4 is the only provably trustworthy implementation accessible as open source. I'm aware of okL4, but as yet I have not explored any options with Cog Systems. The key to the IoT / WoT view is that we do not need traditional desktops, etc. Any server that is accessible via web pages / web apps should deliver all the required user interfacing. I would have thought that Minix or even Plan9 could have been ported to run on top of seL4. The Wombat project (para-virtualised Linux running on okL4 (?)) suggests that such an approach could work. Minix project received several grants in Europe to produce a reliable OS, yet AFAIK, the Minix kernel was never proven trustworthy. However, with a greater number of drivers and utilities it might be a better subject to port to seL4 than any of the other alternatives. I'm submitting my PhD thesis (in Model Based Software Engineering) at the end of June. Maybe I'll have some spare bandwidth to delve deeper in the above ideas. Until then, I'm looking out for what others on this mailing list might have to suggest, contribute, etc. Cheers, Tyga On 9 March 2016 at 09:52, Kevin Elphinstone <Kevin.Elphinstone@nicta.com.au> wrote:
Thank you for your responses. I am ambitious about following the paths that you have suggested, and I am very excited. When I asked for tutelage, I assumed that there was -zero- usable material for the newcomer. I apologize for making that assumption. As I review what you've given me, I still anticipate turning what I learn for my own goals into a tutorial for others on similar paths. I hope that you'll let me participate in any plans moving forward with documentation. My ambition about using seL4 as a hypervisor is still uncontested, however. Is a practical VMM for seL4 even available for the x86 platform? Are there even academic projects that I can cannibalize? As suggested by Kevin and Gerwin, I'll review the Dev Days stuff tomorrow, specifically the tutorials project, https://github.com/seL4-projects/sel4-tutorials-manifest. I'll see how far I can get without help. The same goes for the AOS course material. When is the next Developer Days event? Especially if it were held in the USA, I'd be very interested in attending. When you're developing for the AOS project ( http://www.cse.unsw.edu.au/~cs9242/15/project/index.shtml, found via http://sel4.systems/Info/Projects/), is it essential that you target specifically the SABRE boards during development? Is a VM not an option? I see one of the milestones is to develop a timer driver, but on the 'Getting Started' page, I'm reading that QEMU doesn't implement all the timers, but I don't know if that includes the timer in question. Part of this question has to do with the fact that I see a lot of material on the web site that seems to suggest that ARM is the preferred target for development work generally. Are there divisions of people that prefer one architecture over another? Regarding tutorial paths, I see value in both the options that Kevin suggested. I prefer the first option, and, as I mentioned before, I'll happily grind through the AOS and Dev Days stuff to do it.The second option, however, certainly has merit if partners and community are already accepting and using CAmkES. I think the only thing I would contribute is to maintain a clear division between the two paths. TU Dresden, for example, appears to have wanted to maintain distinct development paths, but made option A incredibly hard to find, and then incredibly brief: https://l4re.org/doc/l4re_tutorial.html Thank you, again. I hope that I can make a valuable contribution to the seL4 community. Andrew Jackman kd7nyq@gmail.com On Tue, Mar 8, 2016 at 6:55 PM, da Tyga <cyberfonic@gmail.com> wrote:
1. The tutorials from the dev days already contain a lot of things. Check it and try. The main issue is that sometimes, they are out of date so that you might reach out to the NICTA folks and/or issue a bug report. 2. There are some work you can take. For example rust for sel4 ( https://robigalia.org/ ). Or SMACCM https://github.com/smaccm/ . On our end, we are working on it but have nothing public (<advertisement>we are looking for developers</advertisement>) 3. The page you mentioned about AOS seems to be about SOS, not seL4. SOS is initially a french operating system designed to learn the basics of operating systems. If you can read (or translate) french, the full courses are available online and free at http://sos.enix.org (source code included) and can run with i386 4. ARM is preferred for embedded development but most of the time (modulo minor changes), you can still use i386 and emulate it. Try the sel4 tutorial, you will then see how easy it is to change the architecture. Hope that helps! Julien. On Wed, Mar 9, 2016 at 2:24 AM, Jackman <kd7nyq@gmail.com> wrote:
On 9 Mar 2016, at 18:24 , Jackman <kd7nyq@gmail.com<mailto:kd7nyq@gmail.com>> wrote: My ambition about using seL4 as a hypervisor is still uncontested, however. Is a practical VMM for seL4 even available for the x86 platform? Are there even academic projects that I can cannibalize? That’d exactly what’s flying on the ULB: https://ssrg.nicta.com.au/projects/TS/SMACCM/ 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.
participants (5)
-
da Tyga -
Gernot Heiser -
Jackman -
Julien Delange -
Kevin Elphinstone