Re: A comment about changing kernels

[Bas Wijnen]

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

> 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.

> 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.

However, what I would really like to hear from Shapiro is what's _wrong_ with
Coyotos.  If anyone knows, it would be him. :-)

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? ;-)

> 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.

> Please note: The above is not a complete list.  It is _not at all_
> intended to be suggest a decision.  I am not going to make a decision
> before understanding as many facts as possible, and I am certainly not
> going to make any decision all alone on a limb ;)

Good idea.

> List is very low traffic.  It will be persistent.

Cool, a persistent list.  What does that mean, exactly? :-)

Thanks,
Bas

-- 
I encourage people to send encrypted e-mail (see http://www.gnupg.org).
If you have problems reading my e-mail, use a better reader.
Please send the central message of e-mails as plain text
   in the message body, not as HTML and definitely not as MS Word.
Please do not use the MS Word format for attachments either.
For more information, see http://129.125.47.90/e-mail.html

signature.asc
Description: Digital signature