[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: L4.sec
|
From: |
Marcus Brinkmann |
|
Subject: |
Re: L4.sec |
|
Date: |
Fri, 08 Jun 2007 00:12:26 +0200 |
|
User-agent: |
Wanderlust/2.14.0 (Africa) SEMI/1.14.6 (Maruoka) FLIM/1.14.8 (Shijō) APEL/10.6 Emacs/23.0.0 (i486-pc-linux-gnu) MULE/6.0 (HANACHIRUSATO) |
At Wed, 6 Jun 2007 18:24:33 +1200,
"Shams" <address@hidden> wrote:
>
> Hi,
>
> Has anyone reviewed OKL4 for usage with Hurd?
> http://www.ok-labs.com/technology/
As far as I know this project is based on the seL4 work from NICTA[1].
seL4 is a cross-over between EROS and the previous L4 generations: The
mapping paradigm of L4 is preserved, while kernel object semantics
resemble EROS in some details.
[1] http://ertos.nicta.com.au/research/sel4/
It's an interesting mix, with some things good and some things
uncertain. Definitely a relevant project, but practical value of the
implementation to us is unclear to me. The focus is also very
different (formal verification, embedded systems).
Thanks,
Marcus