Re: A Framework for Device Drivers in Microkernel Operating Systems

[Espen Skoglund]

[Jonathan S Shapiro]
> On Mon, 2006-05-15 at 20:29 +0200, Espen Skoglund wrote:
>> o L4Ka is a widely defined project that encompasses many
>> sub-projects.  One of these sub-projects is the L4Ka::Pistachio
>> microkernel.  If you want to refer to features such as those above
>> you should really refer to specific microkernel APIs instead.
>> 
>> o Regarding unprotected IPCs.  The IPC mechanism in Version X.2 is
>> not completely unprotected.  You do have the Redirectors that can
>> be used for restricting IPCs, albeit not very efficiently.
>> 
>> o The problems with global name spaces are being addressed in L4Ka
>> and local name spaces have been implemented in L4Ka::Pistachio.

> These three points are all true, but they demonstrate that there is
> no such thing as L4. There are only N different implementations
> sharing not-clearly-defined portions of a specification. Because of
> this, it is difficult to understand which subsystems run on which
> kernel versions.  It is *impossible* to understand (or substantiate)
> security claims for L4 as a whole.

Ok.  Whatever.  If you say that there exists no such thing as L4 then
it must definitely be true, right.

There are a number of implementations of L4, yes.  These
implementations do (or at least should) implement a specific L4 API.
L4Ka::Pistachio currently implements the L4 X2 API, L4Ka::Hazelnut
implements the X0 API, etc.  Sure, some people might implement kernels
with no clearly defined API.  But don't blame this on L4 in general.
Blame it on sloppy kernel designers.

You should know that parts of the L4 community strive very hard to
make the API spec match up to the implementation (actually, it's the
other way around).  Case of point: the X2 specification was worked on
for more than one and a half years before a single line of code in
Pistachio was written (and I'm not counting the time Jochen spent on
the spec here).  The idea is that when in doubt, look at the
specification, not the implementation.

I should also note that, yes, certain parts of the specification are
not not always implemented; or rather, they are implemented on a
as-needed basis.  This simply means that the kernel implementation is
not completely finished.  This is one of the reasons why
L4Ka::Pistachio is still in version 0.5.  As I said above, when
refering to L4 features, refer to a particular L4 API rather than an
specific implementation.

> Meta-comment, not really related to my statement above: it is a flaw
> of the L4 specification that error behavior is underspecified.

Example?

        eSk