OKL4 (or seL4) Released.

On January 21st, 2011, there was an announcement that Open Kernel Labs released OKL4 Verified for download and prototyping.

http://www.ok-labs.com/releases/release/open-kernel-labs-provides-okl4-verified-for-download-and-prototyping

• OK-labs Developer Wiki : http://wiki.ok-labs.com/
• OK GeekTV http://www.ok-labs.com/community/ok-geektv/
• White papers http://www.ok-labs.com/products/whitepapers-abstract-page
• Blogs http://www.ok-labs.com/community/company-blog
• Book in Amazon : (Open Kernel Labs)

1. What are released

The seL4 ARM binaries both on ARM and IA32 are released. For each architecture, two binaries are available: one for debug mode and the other for release mode.

It provides the source codes for user libraries to make use of the released binary kernels. One can build several examples to pack it with the seL4 kernel to run on a version of Qemu supporting ARM architecture. For this, it provides an Elf loader (ARM boot loader) and a binary file manipulator (Dite).

A para-virtualised Linux, Wombat, is also included as an example. But it can run either on a Qemu supporting IA32 or a real hardware.

Open Kernel Labs released the seL4 Reference manual for API version 1.1 together with an abstract formal specification for the APIs. The specification is written in Isabelle/HOL definitions.

1.1 What are not released

Note that the source code for the seL4 kernel is not opened. As a natural consequence, it provides no concrete formal specification and no proof things. It is unfortunate not to be able to see a high-level prototype, written in Haskell, of the seL4 kernel that matches with the released abstract specification.

2. Playing with the seL4 examples

It seems to be quite straightforward to run the released seL4 examples. I ran them on Ubuntu 10.04. You have only to follow the instructions guided by . 

Some of the released examples run on ARM while the others run on IA32. You had better download two set of Code Sourcery toolchains. (Can we build the IA32 examples with the gcc compiler on the Ubuntu?)

This is just for your reference, I downloaded two Sourcery G++ Lite 2010.09-50 for ARM GNU/Linux and 2010.09-44 for IA32 GNU/Linux to build the released examples.

My quick trials succeeded in building and running the examples in Section 1,2,3,4, but got stuck in Section 5 and 6. (I will continue to explore the reason of the build errors I met.)

3.

(Soon I will try to write a summary of the API reference and the abstract specification.)