[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: A Framework for Device Drivers in Microkernel Operating Systems
From: |
Jonathan S. Shapiro |
Subject: |
Re: A Framework for Device Drivers in Microkernel Operating Systems |
Date: |
Tue, 16 May 2006 10:29:05 -0400 |
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
- A Framework for Device Drivers in Microkernel Operating Systems, William Grim, 2006/05/12
- Re: A Framework for Device Drivers in Microkernel Operating Systems, Tom Bachmann, 2006/05/12
- Re: A Framework for Device Drivers in Microkernel Operating Systems, Espen Skoglund, 2006/05/15
- Re: A Framework for Device Drivers in Microkernel Operating Systems, Tom Bachmann, 2006/05/15
- Re: A Framework for Device Drivers in Microkernel Operating Systems, Jonathan S. Shapiro, 2006/05/15
- Re: A Framework for Device Drivers in Microkernel Operating Systems, Espen Skoglund, 2006/05/16
- Re: A Framework for Device Drivers in Microkernel Operating Systems,
Jonathan S. Shapiro <=
- Re: A Framework for Device Drivers in Microkernel Operating Systems, Espen Skoglund, 2006/05/16
- Re: A Framework for Device Drivers in Microkernel Operating Systems, Jonathan S. Shapiro, 2006/05/16
- Re: A Framework for Device Drivers in Microkernel Operating Systems, Espen Skoglund, 2006/05/16
- Re: A Framework for Device Drivers in Microkernel Operating Systems, Jonathan S. Shapiro, 2006/05/15
- Re: A Framework for Device Drivers in Microkernel Operating Systems, William Grim, 2006/05/15
- Re: A Framework for Device Drivers in Microkernel Operating Systems, Tom Bachmann, 2006/05/16
- Re: A Framework for Device Drivers in Microkernel Operating Systems, Espen Skoglund, 2006/05/16
- Re: A Framework for Device Drivers in Microkernel Operating Systems, Jonathan S. Shapiro, 2006/05/16
- Re: A Framework for Device Drivers in Microkernel Operating Systems, Espen Skoglund, 2006/05/16