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:
Is anyone interested in tutoring on the topic of sel4? I have two objectives:
First, I'm interested in beginning programming, like getting through the Hello World process. I would hope this eventually includes things like basic driver development and practical application development.
Second, I want to understand how virtualization works with sel4 and the infrastructure behind it. My objective is to be able to stand up my own virtualization host and guests.
I'm not sure how payment would work. I'd be interested in turning our experience into tutorials for community consumption, which may be more valuable to some of you than the money.
Thank you.
Andrew Roy Jackman
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