Re: A Framework for Device Drivers in Microkernel Operating Systems

[Jonathan S. Shapiro]

On Tue, 2006-05-16 at 13:34 +0200, Espen Skoglund wrote:
> [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.

Espen: let me back up. I wrote in haste, and I did not intend to insult
the L4 community.

There are many times when a question will come up on this list (or
others), and the answer from someone in the L4 community will be "oh,
look at implementation XYZ. That does something a little different that
meets what you want". Sometimes it is simply that one implementation is
more complete. But at other times it is a matter of experimental
features (such as local names for IPC, which you mentioned that one of
the implementations has).

>From the outside, it becomes *very* difficult to tell which features can
be relied on, and also very difficult to know how to discuss which
features are part of L4 and which features are not. I often find that I
want to honestly describe the state of L4 in a paper or a note, but I
cannot do so, because I cannot figure out which set of features is
definitive. The X2 spec is almost never useful for this, because the
features I am trying to write up are almost always post-X2.

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

An implementation that does not fully implement the specification is not
an L4 implementation and should not be *called* an L4 implementation.

I am curious, and I really do not mean this question to be unpleasant:

   According to the definition "implements the specification fully", are
   there *any* implementations of L4.X2?

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

I apologize that the following example is vague. I am pressed for time
and I am working from memory.

During the time that I was trying to edit the L4 spec, I remember
looking at the IPC specification. It gives a very clear statement of
what happens when all goes well, but I remember thinking:

  If there is a page fault I can see that the pager
  gets invoked. So far, so good. But ultimately the pager
  invocation may not complete. At that point I do not see
  anything here that tells me the outcome of the IPC.

or

  What happens if an IPC is addressed to a thread-id for
  a TCB that is not currently allocated?

I think what I am trying to say is that there are many places where I
wanted to understand what happens under exceptional conditions, and I
could not discover the answer from reading the specification. If it were
only one or two examples, then I would think that there was some
subtlety that I failed to understand. It was not just one or two
examples.

One lesson from the S/370 Principles of Operation is that *all* outcomes
need to have specified, well-defined behavior -- even the unlikely
corner cases.


shap