Re: A Framework for Device Drivers in Microkernel Operating Systems

[Espen Skoglund]

[Jonathan S Shapiro]
> Is there a web page that summarizes this? I would find it very
> useful to be able to check this.

Under each of the architectures on:

   http://l4ka.org/projects/pistachio/

You'll find a list of missing features/bugs for that architecture.  As
I said, these lists don't seem to be complete, so they probably won't
prove very useful to you.

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

The description of the ErrorCode TCR in the "Output Parameters"
section in the specification of the IPC syscall states the outcome.
Maybe I'm overlooking something obvious here, but I don't see how this
state transition diagram would influence the outcome.

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

Yes.  This is true.  I actually thought this was coverd in the
description of "undefined value" in the preamble.  I now see that this
is not the case.

        eSk