Re: A Framework for Device Drivers in Microkernel Operating Systems

[Espen Skoglund]

[Jonathan S Shapiro]
> Espen: let me back up. I wrote in haste, and I did not intend to
> insult the L4 community.

Yes.  I know that.  I just sometimes feel the need to pull the break
when it looks like the comments are running out of control.  My
comments wasn't inteded to sound overly harsh.

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

This is exactly why I'm telling people too look to the reference
manual when they're in doubt.  Of course, sometimes the reference
manual can still be unclear, and we're trying to address this when
such ambiguities occur.  Obviously, this doesn't apply to specs which
are still work-in-progress such as the X3e spec I've been doing---but
then again, I haven't released the implementation for this spec.

As you say, sometimes the confustion comes from an implementation
being more complete than another.  We try to keep a list on the L4Ka
web site about which features are missing in the current
implementation, but I suspect this list is not always as complete as
it should be.

For experimental API features, e.g., the special semantics for the
ExchangeRegisters syscall, we always mark these under a special
"Experimental Features" menu in the kernel configuration, and, if
enabled, flag the feature within the Kernel Interface Page for the
applications to see (note, I'm talking about the L4Ka::Pistachio
kernel here).

Regarding the local names spaces, I said that I had implemented them
in Pistachio.  What I meant wasn't that they had been implemented in
the official Pistachio release.  Rather, they had been implemented in
my own work-in-progress repository.  Sorry for being vague there.  The
implementation is (mostly) consistent with my X3e spec which I also
haven't released (reminder to self: get some few more essential
updates to it and get it released).

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

For work that is in progress it will always be impossible or difficult
to say which feature is *definite*.  This is very much in the nature
of defining something as "work in progress".  For currently official
features you'll have to refer to the reference manual of a particular
API.

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

Call it "partial implementation" then if you like.  The fact that a
release is zero point something should clearly indicate that it is not
feature complete or up to final release standards yet.

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

According to your definition, no.  I should note that adding support
for things like Redirectors isn't really a major hassle, though.  One
reason why some features have not been implemented is because there
have been discussions whether the features as specified really are
what we want to start with, and since nobody have requested them we've
been reluctant to implement them in its current form.

To take one example, the redirectors, nobody actually had any use for
them until the Sydney group started playing around with some of their
systems.  What happened then was that the redirector semantics were
changed slightly before they implemented it in their embedded versions
of the kernel.  These changes are now very likely to make it back into
the X2 specification before they get implemented in the X2 version of
the kernel.

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

Ok.  The spec only says that the behaviour of the faulting thread is
undefined if the pager does not follow the page-fault protocol.

Agreed, it would be better to specify more exactly the behaviour if
the IPC fails altogheter.  And after actually implementing the
protocol we also learned more about how to more natually express the
behaviour if the pager does not conform to the protocl.  AFAIK, there
still hasn't been a complete agreement on the exact behaviour in this
case, so...

> or

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

"Not currently allocated" looks like some implementation artifact that
the user should not care about.  I'd say "non-existing thread" is more
accurate and the "not-existing partner" error is then appropriate.

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

I fully sympathize with you on this one.  As I said, it *is* our
intention that the spec should be as complete as possible.

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

I (kind of) agree with this principle.  You might notice that in some
cases the L4 specs say "undefined behaviour" or "undefined return
value".  This is generally done to allow for certain optimizations to
take place in cases where user input is incorrect or makes no sense.
Whether this is good or bad is of course another matter of discussion.

        eSk