[lkml]   [2005]   [May]   [31]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
Messages in this thread
SubjectRe: RT patch acceptance
>>>>> "Esben" == Esben Nielsen <> 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 for our work.

In addition to our work, there's the Adeos system
( uses a very similar approach.

Dr Peter Chubb peterc AT
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
More majordomo info at
Please read the FAQ at

 \ /
  Last update: 2005-06-01 03:02    [W:0.345 / U:9.020 seconds]
©2003-2018 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site