lkml.org 
[lkml]   [2005]   [May]   [31]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: 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/

\
 
 \ /
  Last update: 2005-06-01 03:02    [from the cache]
©2003-2014 Jasper Spaans. Advertise on this site