Re: A comment about changing kernels

[Marcus Brinkmann]

At Thu, 27 Oct 2005 21:39:17 +0200,
Bas Wijnen <address@hidden> wrote:
> 
> On Thu, Oct 27, 2005 at 08:53:43PM +0200, Marcus Brinkmann wrote:
> > The problem with L4.sec is the following: It does currently not have
> > all the operations that we think we need (I am thinking specifically
> > about efficient capability copy and identification).  Note that this
> > is preliminary and not definitive.
> 
> They have said that if we can show that it is something which makes sense in a
> real system, they would look at implementing it (and implement it if it's not
> too hard.  It's also been said that it isn't too hard).

This is true, but they have not provided a metric for what "showing
that it is something that makes sense" means, ie, what we have to
demonstrate to convince them.  The usual response is "if it can't be
done feasibly any other way", which is very hard to do.  And I am not
attacking these problems from a research angle, but from an
engineering angle, which doesn't help to push the argument in the
general case.

Please note that I am not putting any blame here.  Both positions are
reasonable, they just don't work very well together in getting
actual results.

I have actually the opportunity to go to Dresden and make my cause in
front of the L4 group, I just don't know right now if or rather when I
can get everything together to actually present my case thoroughly.
This of course also depends on real life issues etc.

Anyway, that part of the design is actually pretty much covered in
past discussions.  There are still differences, but I am not sure how
much they matter.  There is a totally different corner (memory
management) which we have yet to reassess.  Neal will post something
about this soon.

> > It's design goal is very ambitious, and there is an uncertainty if it will
> > be realized at all.  It's experimental in that it is breaking new ground.
> > And last, it is not clear if all our design goals can be efficiently
> > realized.
> 
> I think this is very important.  We need to know this before we make the
> choice.  It would be very bad if we choose another Mach, of which we will find
> out later that it isn't suitable for what we want.

Bas, I know!

> > Coyotos is a bit different, because it is more conservative in its
> > goal, IMO.
> 
> This is what I understood from Shapiro as well.  L4 changed drastically, while
> EROS changed a bit.

You can read Bernhard Kauer's paper to find out how much L4 changes.
 
> However, what I would really like to hear from Shapiro is what's _wrong_ with
> Coyotos.  If anyone knows, it would be him. :-)

Yes, we have to take a close look at its warts as well.  If you want,
you can start with the following:

http://www.eros-os.org/pipermail/eros-arch/2003-December/004047.html
http://www.eros-os.org/pipermail/eros-arch/2003-December/004048.html
http://www.eros-os.org/pipermail/eros-arch/2003-December/004052.html
http://www.eros-os.org/pipermail/eros-arch/2003-December/004053.html

Note that some of these have been extensively reviewed, and some of
these are addressed in Coyotos.  I don't have a list though.

For example, consider also this email:
http://www.eros-os.org/pipermail/eros-arch/2003-December/004247.html

> Also, if we decide to use Coyotos, will he continue to make it his full-time
> job to hang around on this mailinglist?  Or is that just a PR move to convince
> us? ;-)

We know where he works, though! :) You could just enlist for his
lectures and try to get all the answers there.  Actually, if you
happened to have been in his last few lectures, you would have gotten
the answers there :)

> > There is an orthogonal goal of formal verification, which
> > is somewhat uncertain and can take a long time, but this goal can and
> > will (AFAIK) be realized in parallel to writing a working
> > implementation.  So, Coyotos is also experimental, but not so much in
> > its architecture, but in its application (formal verification).
> 
> I would consider it a nice bonus to have a verified kernel. :-)  But I don't
> think this is very important in this decision.

I agree.
 
Thanks,
Marcus