Re: A comment about changing kernels

[Marcus Brinkmann]

At Thu, 27 Oct 2005 20:36:32 +0200,
ness <address@hidden> wrote:
> Marcus already mentioned that l4.sec is no alternative, as the time of 
> release is too far away.

D'oh, yeah, but if you want something to quote me on, please let me be
a bit more careful ;)

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.  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.  For
example, will it support persistence well enough if we want it?  This
would not necessarily be a defect in L4.sec, but rather an issue with
our engineering resources (however, some of such issues could also be
architectural).

So, there are a couple of uncertainties, number depending on our
goals.

Coyotos is a bit different, because it is more conservative in its
goal, IMO.  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).

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

> But actually we (or at least I) don't know much about coyotos. I can't 
> even say whether it is persistent. And your documentation page isn't 
> that helpful, as the kernel spec is mostly incomplete. (btw, I tried to 
> subscribe to the coyotos lists but I got no mails - has there been 
> traffic this afternoon?)

Yeah, the webpage is getting old before it is even written ;) List is
very low traffic.  It will be persistent.  Shap will surely fill you
in about the rest.

Thanks,
Marcus