Messages in this thread | | | Date | Wed, 1 Jun 2005 10:26:28 +1000 | From | Peter Chubb <> | Subject | Re: RT patch acceptance |
| |
>>>>> "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/
| |