[cap-talk] OKL4 Released - An Object-Capability L4 Derivative

[Toby Murray]

News on the operating systems front:

Open Kernel Labs [1] (the commercialisation arm of the seL4 project [2])
has just released the first (to my knowledge) publicly available open
source Object-Capability L4 derivative, called OKL4 version 2.1 [3].

This is significant for a number of reasons:
 - It appears to be widely supported (both IA32 and ARM)

 - It is well documented (the reference / API manual [4] is around 250
pages long)

 - It has an apparently active developer community [5]

 - They have implemented/ported over a POSIX C library and pthreads
functionality on top of the microkernel

 - It is based on the academic work of the seL4 project, which is the
most deeply verified, open, object-capability microkernel currently in
existence

Disclaimer: I have no affiliation with this stuff and am merely an
interested observer.

Cheers

Toby


[1] www.ok-labs.com
[2] http://www.ertos.nicta.com.au/research/sel4/
[3] http://lists.okl4.org/pipermail/developer/2008-April/000920.html
[4]
http://wiki.ok-labs.com/downloads/release-2.1/okl4-user-manual_2.1.pdf
[5] http://wiki.ok-labs.com/

[If someone would be so kind to pass this on to coyotos-dev, capros-dev
or anywhere else that might be interested, I'd be really appreciative.]