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.pdf),
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