Re: A Framework for Device Drivers in Microkernel Operating Systems

[Jonathan S. Shapiro]

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

Is there a web page that summarizes this? I would find it very useful to
be able to check this.

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

It is difficult to have a rigorous specification where there is no
agreement. :-)

I understand that specifications can be a work in progress. My only
point here is that rigor is important. Every bit and every result that
is "undefined" presents a problem for later compatibility, and also for
verifiability.

> >   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 that "non-existing thread" is what I meant: the slot in the
thread table exists, but is not currently allocated for use by any
actual thread. And yes, I think that the non-existing partner error is
appropriate. However, it appears to me that the specification does not
actually state this outcome (either directly or indirectly) because it
did not address the fact that TCB slots have a state transition diagram,
and that one state is "not currently allocated".

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

Actually, my point was that this is bad. Certainly it has had *horrible*
consequences for processor designers. Specifically: attempts by
instructions to access or modify undefined bits need to signal an error.
In software it is not always possible to implement this check
efficiently.

Concerning undefined return values, it is important to state someplace a
requirement that "undefined return values" will not return any result
whose value depends on the behavior of other processes/tasks. This
statement implies that if a covert channel is discovered to exist in an
undefined result, the undefined result needs to get a little more
defined. :-)


shap