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 _______________________________________________ L4-hurd mailing list [email protected] http://lists.gnu.org/mailman/listinfo/l4-hurd
