Re: RT patch acceptance

[Peter Chubb <peterc@gelato.unsw.edu.au>]

>>>>> "Esben" == Esben Nielsen <simlo@phys.au.dk> writes:

Esben> On Tue, 31 May 2005, James Bruce wrote:
>> 
>> It is only better in that if you need provable hard-RT *right now*,
>> then you have to use a nanokernel.

Esben> What do you mean by "provable"? Security critical? Forget about
Esben> nanokernels then. The WHOLE system has to be validated. 

The whole point of a nanokernel is it's *small*.  The whole thing can
be formally verified.  And its semantics will provide isolation
between the real-time processes and anything else that's running.

We're currently working on a system called Iguana, which will have
provable WCET for real-time scheduled tasks, and a Linux envionrment
(called `wombat') that provides compatibility for 

Esben> I can't see it would be easier prove that a nano-kernel with
Esben> various needed mutex and queuing mechanism works correct than
Esben> it is to prove that the Linux scheduler with mutex and queueing
Esben> mechanisms works correctly.  

Except that the nano-kernel is less than one percent of the size.

Both systems does the same thing
Esben> and is most likely based on the same principles!  If a module
Esben> in Linux disables interrupts for a non-deterministic amount of
Esben> time, it destroys the RT in both scenarious. With the
Esben> nanokernel, the Linux kernel is patched not to disable
Esben> interrupts, but if someone didn't use the official
Esben> local_irq_disable() macro the patch didn't work anyway...  The
Esben> only way you can be absolutely sure Linux doesn't hurt RT is to
Esben> run it in a full blown virtuel machine where it doesn't have
Esben> access to disable interrupts and otherwise interfere with the
Esben> nano-kernel.

This is precisely the approach we (and others) are taking.   A
virtualised Linux to provide interactive and soft realtime (think java
games on your mobile phone), and a nanokernel for your hard realtime
tasks (think the radio controller on your mobile phone).  
See http://www.disy.cse.unsw.edu.au/Software/Iguana/ for our work.

In addition to our work, there's the Adeos system
(http://www.hyades-itea.org/) uses a very similar approach.

-- 
Dr Peter Chubb  http://www.gelato.unsw.edu.au  peterc AT gelato.unsw.edu.au
The technical we do immediately,  the political takes *forever*
-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@vger.kernel.org
More majordomo info at  http://vger.kernel.org/majordomo-info.html
Please read the FAQ at  http://www.tux.org/lkml/